Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma
Rattachement africain : de. Niveau de preuve : code pays fourni par la source.
Le résumé fourni par la source
Intrinsically typed syntax is an important and popular method for mechanized reasoning about programming languages. We explore the limits of this method in the setting of finitely-stratified System F using the Agda proof assistant. This system supports elegant definitions of denotational semantics as well as big-step operational semantics based on intrinsically typed syntax. While its syntactic metatheory (i.e., type soundness) works well, we demonstrate that its semantic metatheory poses technical challenges, by defining a logical relation and proving its fundamental lemma. Our logical relation connects a denotational semantics with an operational one, which exposes issues with transfer lemmas as well as minor issues with universe polymorphism.
Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.
Le contrôle bibliographique ouvert
DOI retrouvé dans Crossref DOI retrouvé ; titre concordant.
- Titre Crossref
- Intrinsically Typed Syntax, a Logical Relation, and the Scourge of the Transfer Lemma
- Date Crossref
- 28/08/2024
- Éditeur
- ACM
- Type
- proceedings-article
Ce recoupement confirme des métadonnées liées au DOI. Il ne confirme ni la méthode ni les conclusions de l’étude, et il ne compte pas comme une seconde source scientifique indépendante.
Où se fait cette recherche
-
University of Freiburg pays non établi dans la noticeUniversité ou école supérieure
University of Freiburg.
Une affiliation ne permet pas de déduire la nationalité d’un auteur.