Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers /
Types for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers /
Paul Callaghan [and others].
- Berlin ; New York : Springer, ©2002.
- 1 online resource (viii, 242 pages) : illustrations
- Lecture notes in computer science ; 2277 .
- Lecture notes in computer science ; 2277. .
Includes bibliographical references and index.
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.
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.
English.
9783540458425 3540458425
10.1007/3-540-45842-5. doi
GBA220709 bnb
963684981 DE-101
Automatic theorem proving--Congresses.
Computer programming--Congresses.
Théorèmes--Démonstration automatique--Congrès.
Programmation (Informatique)--Congrès.
Automatic theorem proving
Computer programming
FACinfotech Computer science ER Internet Book Full text
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
QA76.9.A96 / T96 2000
006.3/33
Includes bibliographical references and index.
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.
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.
English.
9783540458425 3540458425
10.1007/3-540-45842-5. doi
GBA220709 bnb
963684981 DE-101
Automatic theorem proving--Congresses.
Computer programming--Congresses.
Théorèmes--Démonstration automatique--Congrès.
Programmation (Informatique)--Congrès.
Automatic theorem proving
Computer programming
FACinfotech Computer science ER Internet Book Full text
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
QA76.9.A96 / T96 2000
006.3/33