A Classical Realizability Model for a Semantical Value Restriction

DOI10.1007/978-3-662-49498-1_19zbMath1335.68059arXiv1603.07484OpenAlexW2336116580MaRDI QIDQ2802494

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)

Related Items

No value restriction is needed for algebraic effects and handlers, Unnamed Item, A Classical Sequent Calculus with Dependent Types, A Classical Realizability Model for a Semantical Value Restriction

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Type inference for polymorphic references
• The calculus of constructions
• A syntactic approach to type soundness
• A call-by-name lambda-calculus machine
• A Classical Realizability Model for a Semantical Value Restriction
• Focalisation and Classical Realisability
• Dependently Typed Programming in Agda
• Secure distributed programming with value-dependent types
• AURA
• Functional and Logic Programming
• The Size-Change Termination Principle for Constructor Based Languages
• Combining proofs and programs in a dependently typed language
• Types for Proofs and Programs