TYPES 2000: Durham, UK

Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers. Lecture Notes in Computer Science 2277 Springer 2002, ISBN 3-540-43287-6 BibTeX

@proceedings{DBLP:conf/types/2000,
  editor    = {Paul Callaghan and
               Zhaohui Luo and
               James McKinna and
               Robert Pollack},
  title     = {Types for Proofs and Programs, International Workshop, TYPES
               2000, Durham, UK, December 8-12, 2000, Selected Papers},
  booktitle = {TYPES},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2277},
  year      = {2002},
  isbn      = {3-540-43287-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Peter Aczel, Nicola Gambino:
Collection Principles in Dependent Type Theory. 1-23
Electronic Edition (Springer LINK) BibTeX
Stefan Berghofer, Tobias Nipkow:
Executing Higher Order Logic. 24-40
Electronic Edition (Springer LINK) BibTeX
Alberto Ciaffaglione, Pietro Di Gianantonio:
A Tour with Constructive Real Numbers. 41-52
Electronic Edition (Springer LINK) BibTeX
Thierry Coquand, Makoto Takeyama:
An Implementation of Type: Type. 53-62
Electronic Edition (Springer LINK) BibTeX
Matt Fairtlough, Michael Mendler:
On the Logical Content of Computational Type Theory: A Solution to Curry's Problem. 63-78
Electronic Edition (Springer LINK) BibTeX
Herman Geuvers, Milad Niqui:
Constructive Reals in Coq: Axioms and Categoricity. 79-95
Electronic Edition (Springer LINK) BibTeX
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. 96-111
Electronic Edition (Springer LINK) BibTeX
Healfdene Goguen:
A Kripke-Style Model for the Admissibility of Structural Rules. 112-124
Electronic Edition (Springer LINK) BibTeX
Susumu Hayashi, Masahiro Nakata:
Towards Limit Computable Mathematics. 125-144
Electronic Edition (Springer LINK) BibTeX
Kristofer Johannisson:
Formalizing the Halting Problem in a Constructive Type Theory. 145-159
Electronic Edition (Springer LINK) BibTeX
Giuseppe Longo:
On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory. 160-180
Electronic Edition (Springer LINK) BibTeX
Nicolas Magaud, Yves Bertot:
Changing Data Structures in Type Theory: A Study of Natural Numbers. 181-196
Electronic Edition (Springer LINK) BibTeX
Conor McBride:
Elimination with a Motive. 197-216
Electronic Edition (Springer LINK) BibTeX
Olivier Pons:
Generalization in Type Theory Based Proof Assistants. 217-232
Electronic Edition (Springer LINK) BibTeX
Monika Seisenberger:
An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma. 233-242
Electronic Edition (Springer LINK) BibTeX