Amazon cover image
Image from Amazon.com

Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers / Paul Callaghan [and others].

By: Contributor(s): Material type: TextTextSeries: Lecture notes in computer science ; 2277.Publication details: Berlin ; New York : Springer, ©2002.Description: 1 online resource (viii, 242 pages) : illustrationsContent type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9783540458425
  • 3540458425
Subject(s): Genre/Form: Additional physical formats: Print version:TYPES 2000 (2000 : Durham, England): Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers.DDC classification:
  • 006.3/33 21
LOC classification:
  • QA76.9.A96 T96 2000
Other classification:
  • 54.10
  • SS 4800
Online resources:
Contents:
Collection Principles in Dependent Type Theory / Peter Aczel and Nicola Gambino -- Executing Higher Order Logic / Stefan Berghofer and Tobias Nipkow -- A Tour with Constructive Real Numbers / Alberto Ciaffaglione and Pietro Di Gianantonio -- An Implementation of Type:Type / Thierry Coquand and Makoto Takeyama -- On the Logical Content of Computational Type Theory: A Solution to Curry's Problem / Matt Fairtlough and Michael Mendler -- Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers and Milad Niqui -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Herman Geuvers, Freck Wiedijk and Jan Zwanenburg -- A Kripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen -- Towards Limit Computable Mathematics / Susumu Hayashi and 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: A Study of Natural Numbers / Nicolas Magaud and 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.
Summary: This book constitutes the thoroughly refereed post-proceedings of the International Workshop of the TYPES Working Group, TYPES 2000, held in Durham, UK in December 2000. The 15 revised full papers presented were carefully reviewed and selected during two rounds of refereeing and revision. All current issues on type theory and type systems and their applications to programming, systems design, and proof theory are addressed.
Holdings
Item type Current library Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library eBook LNCS Available
Total holds: 0

Includes bibliographical references and index.

This book constitutes the thoroughly refereed post-proceedings of the International Workshop of the TYPES Working Group, TYPES 2000, held in Durham, UK in December 2000. The 15 revised full papers presented were carefully reviewed and selected during two rounds of refereeing and revision. All current issues on type theory and type systems and their applications to programming, systems design, and proof theory are addressed.

Collection Principles in Dependent Type Theory / Peter Aczel and Nicola Gambino -- Executing Higher Order Logic / Stefan Berghofer and Tobias Nipkow -- A Tour with Constructive Real Numbers / Alberto Ciaffaglione and Pietro Di Gianantonio -- An Implementation of Type:Type / Thierry Coquand and Makoto Takeyama -- On the Logical Content of Computational Type Theory: A Solution to Curry's Problem / Matt Fairtlough and Michael Mendler -- Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers and Milad Niqui -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Herman Geuvers, Freck Wiedijk and Jan Zwanenburg -- A Kripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen -- Towards Limit Computable Mathematics / Susumu Hayashi and 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: A Study of Natural Numbers / Nicolas Magaud and 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.

English.

Powered by Koha