Deciding equivalence with sums and the empty type

Gabriel Scherer 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : The logical technique of focusing can be applied to the λ-calculus; in a simple type system with atomic types and negative type form-ers (functions, products, the unit type), its normal forms coincide with βη-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidabil-ity of βη-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and a finite model property.
Type de document :
Communication dans un congrès
POPL 2017, Jan 2017, Paris, France. POPL 2017- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 〈10.01213〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01646064
Contributeur : Scherer Gabriel <>
Soumis le : jeudi 23 novembre 2017 - 15:33:25
Dernière modification le : jeudi 10 mai 2018 - 02:06:27

Fichier

finite-sums.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Gabriel Scherer. Deciding equivalence with sums and the empty type. POPL 2017, Jan 2017, Paris, France. POPL 2017- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 〈10.01213〉. 〈hal-01646064〉

Partager

Métriques

Consultations de la notice

89

Téléchargements de fichiers

19