Program Testing and the Meaning Explanations of Intuitionistic Type Theory

DOI10.1007/978-94-007-4435-6_11zbMath1314.03032OpenAlexW100593489MaRDI QIDQ5253930

Peter Dybjer

Publication date: 5 June 2015

Published in: Epistemology versus Ontology (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-94-007-4435-6_11

Mathematics Subject Classification ID

Related Items (3)

Type Theory Should Eat Itself ⋮ A meaning explanation for HoTT ⋮ Predicativity and constructive mathematics

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The calculus of constructions
• Extending Martin-Löf type theory by one Mahlo-universe
• Indexed induction-recursion
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Recursive models for constructive set theories
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Meaning and proofs: on the conflict between classical and intuitionistic logic
• A coherence theorem for Martin-Löf's type theory
• A general formulation of simultaneous inductive-recursive definitions in type theory
• A semantics of evidence for classical arithmetic
• Truth and Proof in Intuitionism
• Towards the animation of proofs -- testing proofs by examples
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Program Testing and the Meaning Explanations of Intuitionistic Type Theory