A Mechanized Theory of Quoted Code Patterns
Radosław, Wasko
2020

Files

Résumé

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.

Détails

Titre A Mechanized Theory of Quoted Code Patterns
Auteur(s) Radosław, Wasko
Directeur(s)
Date 2020-06-18
Laboratoires LAMP
Le document apparaît dans Production scientifique et compétences > I&C - Faculté Informatique & Communications > IINFCOM > LAMP - Laboratoire de méthodes de programmation
Travail produit à l'EPFL
Travaux d'étudiants
Type de travail Semester assignment
Date de création de la notice 2020-06-19

PDF