Publication
The pattern matching on code from the new macro system of Scala 3 is modeled by a calculus called λ half-circle. We present a mechanized proof of soundness of the calculus in Coq and discuss encountered challenges.
Negar Kiyavash, Ehsan Mokhtarian, Yaroslav Kivva, Seyed Jalal Etesami
Martin Odersky, Nicolas Alexander Stucki, Jonathan Immanuel Brachthäuser