Failure is not an option. An exceptional type theory

DOI10.1007/978-3-319-89884-1_9MaRDI QIDQ2323976zbMATHOpenAlexFDO

Authors 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

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)

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

Cited in

(3)

• Russian constructivism in a prefascist theory
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
• An effectful way to eliminate addiction to dependence

Describes a project that uses

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)