Abstract is missing.
- Collection Principles in Dependent Type TheoryPeter Aczel, Nicola Gambino. 1-23 [doi]
- Executing Higher Order LogicStefan Berghofer, Tobias Nipkow. 24-40 [doi]
- A Tour with Constructive Real NumbersAlberto Ciaffaglione, Pietro Di Gianantonio. 41-52 [doi]
- An Implementation of Type: TypeThierry Coquand, Makoto Takeyama. 53-62 [doi]
- On the Logical Content of Computational Type Theory: A Solution to Curry s ProblemMatt Fairtlough, Michael Mendler. 63-78 [doi]
- Constructive Reals in Coq: Axioms and CategoricityHerman Geuvers, Milad Niqui. 79-95 [doi]
- A Constructive Proof of the Fundamental Theorem of Algebra without Using the RationalsHerman Geuvers, Freek Wiedijk, Jan Zwanenburg. 96-111 [doi]
- A Kripke-Style Model for the Admissibility of Structural RulesHealfdene Goguen. 112-124 [doi]
- Towards Limit Computable MathematicsSusumu Hayashi, Masahiro Nakata. 125-144 [doi]
- Formalizing the Halting Problem in a Constructive Type TheoryKristofer Johannisson. 145-159 [doi]
- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type TheoryGiuseppe Longo. 160-180 [doi]
- Changing Data Structures in Type Theory: A Study of Natural NumbersNicolas Magaud, Yves Bertot. 181-196 [doi]
- Elimination with a MotiveConor McBride. 197-216 [doi]
- Generalization in Type Theory Based Proof AssistantsOlivier Pons. 217-232 [doi]
- An Inductive Version of Nash-Williams Minimal-Bad-Sequence Argument for Higman s LemmaMonika Seisenberger. 233-242 [doi]