Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Types for Proofs and Programs

International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers

  • Conference proceedings
  • © 2002

Overview

Editors:
  1. Paul Callaghan

    1. Department of Computer Science, University of Durham, Durham, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Zhaohui Luo

    1. Department of Computer Science, University of Durham, Durham, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. James McKinna

    1. Department of Computer Science, University of Durham, Durham, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  4. Robert Pollack

    1. Department of Computer Science, University of Durham, Durham, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  5. Robert Pollack

    1. Division of Informatics Laboratory for Foundations of Computer Science, The University of Edinburgh, Edinburgh, Scotland, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 2277)

Included in the following conference series:

Conference proceedings info: TYPES 2000.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (15 papers)

  1. Front Matter

    Pages I-VIII
    Download chapter PDF

  2. Collection Principles in Dependent Type Theory

    • Peter Aczel, Nicola Gambino
    Pages 1-23

  3. Executing Higher Order Logic

    • Stefan Berghofer, Tobias Nipkow
    Pages 24-40

  4. A Tour with Constructive Real Numbers

    • Alberto Ciaffaglione, Pietro Di Gianantonio
    Pages 41-52

  5. An Implementation of Type:Type

    • Thierry Coquand, Makoto Takeyama
    Pages 53-62

  6. On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem

    • Matt Fairtlough, Michael Mendler
    Pages 63-78

  7. Constructive Reals in Coq: Axioms and Categoricity

    • Herman Geuvers, Milad Niqui
    Pages 79-95

  8. A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals

    • Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
    Pages 96-111

  9. A Kripke-Style Model for the Admissibility of Structural Rules

    • Healfdene Goguen
    Pages 112-124

  10. Towards Limit Computable Mathematics

    • Susumu Hayashi, Masahiro Nakata
    Pages 125-144

  11. Formalizing the Halting Problem in a Constructive Type Theory

    • Kristofer Johannisson
    Pages 145-159

  12. On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory

    • Giuseppe Longo
    Pages 160-180

  13. Changing Data Structures in Type Theory: A Study of Natural Numbers

    • Nicolas Magaud, Yves Bertot
    Pages 181-196

  14. Elimination with a Motive

    • Conor McBride
    Pages 197-216

  15. Generalization in Type Theory Based Proof Assistants

    • Olivier Pons
    Pages 217-232

  16. An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma

    • Monika Seisenberger
    Pages 233-242

  17. Back Matter

    Pages 243-243
    Download chapter PDF
Back to top

Other volumes

  1. Types for Proofs and Programs

Keywords

Editors and Affiliations

  • Department of Computer Science, University of Durham, Durham, UK

    Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack

  • Division of Informatics Laboratory for Foundations of Computer Science, The University of Edinburgh, Edinburgh, Scotland, UK

    Robert Pollack

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation