A Classical Realizability Model for a Semantical Value Restriction

DOI10.1007/978-3-662-49498-1_19zbMATH Open1335.68059arXiv1603.07484OpenAlexW2336116580MaRDI QIDQ2802494FDOQ2802494

Authors: Rodolphe Lepigre 

Publication date: 26 April 2016

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

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

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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

Uses Software

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

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)