A Classical Realizability Model for a Semantical Value Restriction

Rodolphe Lepigre 1, *
Abstract : We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01107429
Contributeur : Rodolphe Lepigre <>
Soumis le : jeudi 24 mars 2016 - 11:56:09
Dernière modification le : jeudi 11 janvier 2018 - 06:12:26
Document(s) archivé(s) le : samedi 25 juin 2016 - 14:13:21

Fichiers

esop2016.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Rodolphe Lepigre. A Classical Realizability Model for a Semantical Value Restriction. 2015. 〈hal-01107429v3〉

Partager

Métriques

Consultations de la notice

67

Téléchargements de fichiers

55