A Classical Realizability Model for a Semantical Value Restriction

TL;DR

This paper introduces a new type system for call-by-value languages with control operators, using a classical realizability model to handle value restrictions and dependent types.

Contribution

It proposes a novel semantic model for a type system supporting proofs and dependent products in a call-by-value setting with relaxed restrictions.

Findings

Semantic model ensures system consistency.

Supports proofs of program properties.

Handles dependent products with relaxed restrictions.

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).