A Mechanized Theory of Quoted Code Patterns

2020
Projet étudiant

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.

Source officielle

https://infoscience.epfl.ch/record/278147?ln=fr

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

A Mechanized Theory of Quoted Code Patterns

Revisiting the General Identifiability Problem

Proof of Multi-Stage Programming with Generative and Analytical Macros

Integral Convexity And Parabolic Systems

Proof of Multi-Stage Programming with Generative and Analytical Macros

Integral Convexity And Parabolic Systems

Revisiting the General Identifiability Problem