| 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 |
図書
