A Classical Realizability Model for a Semantical Value Restriction

DOI10.1007/978-3-662-49498-1_19MaRDI QIDQ2802494zbMATH OpenOpenAlexFDO

Authors Rodolphe Lepigre

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.07484

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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

Recommendations

• A constructive valuation semantics for classical logic
• scientific article; zbMATH DE number 5851813
• scientific article; zbMATH DE number 6841178
• A semantics of realisability for the classical propositional natural deduction
• Realizability of three-valued semantics for abstract dialectical frameworks
• Realizability models refuting Ishihara's boundedness principle
• Restricted Classical Modal Logics
• scientific article; zbMATH DE number 65751
• scientific article; zbMATH DE number 4212000
• Classical and relative realizability

Cites work

• scientific article; zbMATH DE number 4180818 (Why is no real title available?)
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• A Classical Realizability Model for a Semantical Value Restriction
• A call-by-name lambda-calculus machine
• A syntactic approach to type soundness
• AURA
• Combining proofs and programs in a dependently typed language
• Dependently typed programming in Agda
• Focalisation and Classical Realisability
• Functional and Logic Programming
• Secure distributed programming with value-dependent types
• The calculus of constructions
• The size-change termination principle for constructor based languages
• Type inference for polymorphic references
• Types for Proofs and Programs

Cited in

(4)

• PML2: integrated program verification in ML
• A classical sequent calculus with dependent types
• A Classical Realizability Model for a Semantical Value Restriction
• No value restriction is needed for algebraic effects and handlers

Describes a project that uses

Uses Software

• F*
• AURA
• Agda
• Nuprl
• PVS
• Coq

This page was built for publication: A Classical Realizability Model for a Semantical Value Restriction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802494)