Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8--12, 2000. Selected papers (Q1601174)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Aczel, Peter; Gambino, Nicola}, Collection principles in dependent type theory, 1-23 [Zbl 1054.03036] \textit{Berghofer, Stefan; Nipkow, Tobias}, Executing higher order logic, 24-40 [Zbl 1054.68133] \textit{Ciaffaglione, Alberto; Di Gianantonio, Pietro}, A tour with constructive real numbers, 41-52 [Zbl 1054.03038] \textit{Coquand, Thierry; Takeyama, Makoto}, An implementation of Type:Type, 53-62 [Zbl 1054.68087] \textit{Fairtlough, Matt; Mendler, Michael}, On the logical content of computational type theory: A solution to Curry's problem, 63-78 [Zbl 1054.03027] \textit{Geuvers, Herman; Niqui, Milad}, Constructive reals in Coq: Axioms and categoricity, 79-95 [Zbl 1054.03039] \textit{Geuvers, Herman; Wiedijk, Freek; Zwanenburg, Jan}, A constructive proof of the fundamental theorem of algebra without using the rationals, 96-111 [Zbl 1054.03041] \textit{Goguen, Healfdene}, A Kripke-style model for the admissibility of structural rules (extended abstract), 112-124 [Zbl 1054.03508] \textit{Hayashi, Susumu; Nakata, Masahiro}, Towards limit computable mathematics, 125-144 [Zbl 1054.03037] \textit{Johannisson, Kristofer}, Formalizing the halting problem in a constructive type theory, 145-159 [Zbl 1054.03032] \textit{Longo, Giuseppe}, On the proofs of some formally unprovable propositions and prototype proofs in type theory, 160-180 [Zbl 1062.03056] \textit{Magaud, Nicolas; Bertot, Yves}, Changing data structures in type theory: A study of natural numbers, 181-196 [Zbl 1054.03500] \textit{McBride, Conor}, Elimination with a motive, 197-216 [Zbl 1054.03501] \textit{Pons, Olivier}, Generalization in type theory based proof assistants, 217-232 [Zbl 1054.03502] \textit{Seisenberger, Monika}, An inductive version of Nash-Williams' minimal-bad-sequence argument for Higman's lemma, 233-242 [Zbl 1054.03042]