Failure is not an option. An exceptional type theory

DOI10.1007/978-3-319-89884-1_9zbMATH Open1418.68062OpenAlexW2798115558MaRDI QIDQ2323976FDOQ2323976

Pierre-Marie Pédrot, Nicolas Tabareau

Publication date: 13 September 2019

Full work available at URL: https://doi.org/10.1007/978-3-319-89884-1_9

Recommendations

• The independence of Markov's principle in type theory
• The independence of Markov's principle in type theory
• A New Elimination Rule for the Calculus of Inductive Constructions
• Extending type theory with forcing
• The definitional side of the forcing

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cited In (1)

• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules

Uses Software

• Coq

This page was built for publication: Failure is not an option. An exceptional type theory

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