Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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).
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-01107429
Contributor : Rodolphe Lepigre <>
Submitted on : Thursday, March 24, 2016 - 11:56:09 AM
Last modification on : Thursday, January 11, 2018 - 6:12:26 AM
Document(s) archivé(s) le : Saturday, June 25, 2016 - 2:13:21 PM

Files

esop2016.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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

Share

Metrics

Record views

161

Files downloads

282