Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
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.