Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino |
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow |
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio |
An Implementation of Type: Type / Thierry Coquand ; Makoto Takeyama |
On the Logical Content of Computational Type Theory: A Solution to CurryÆs Problem / Matt Fairtlough ; Michael Mendler |
Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers ; Milad Niqui |
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Freek Wiedijk ; Jan Zwanenburg |
AKripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen |
Towards Limit Computable Mathematics / Susumu Hayashi ; Masahiro Nakata |
Formalizing the Halting Problem in a Constructive Type Theory / Kristofer Johannisson |
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory / Giuseppe Longo |
Changing Data Structures in Type Theory: AStudy of Natural Numbers / Nicolas Magaud ; Yves Bertot |
Elimination with a Motive / Conor McBride |
Generalization in Type Theory Based Proof Assistants / Olivier Pons |
An Inductive Version of Nash-WilliamsÆ Minimal-Bad-Sequence Argument for HigmanÆs Lemma / Monika Seisenberger |
Author Index |
Collection Principles in Dependent Type Theory / Peter Aczel ; Nicola Gambino |
Executing Higher Order Logic / Stefan Berghofer ; Tobias Nipkow |
ATour with Constructive Real Numbers / Alberto Ciaffaglione ; Pietro Di Gianantonio |
An Implementation of Type: Type / Thierry Coquand ; Makoto Takeyama |
On the Logical Content of Computational Type Theory: A Solution to CurryÆs Problem / Matt Fairtlough ; Michael Mendler |
Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers ; Milad Niqui |