Types for proofs and programs : international workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999 : selected papers / Thierry Coquand ... [and others] (eds.).

Format:

• Book
• Conference/Event

Contributor:

• Coquand, Thierry, 1961-

Conference Name:

• TYPES'99 (1999 : Lökeberg, Sweden)

Series:

• Lecture notes in computer science ; 1956.
• Lecture notes in computer science

Language:

English

Subjects (All):

• Automatic theorem proving--Congresses.
• Automatic theorem proving.
• Computer programming--Congresses.
• Computer programming.
• Type theory--Congresses.
• Type theory.

Genre:

• Conference papers and proceedings.

Physical Description:

193 pages : illustrations ; 24 cm.

Place of Publication:

Berlin ; New York : Springer, [2000]

Summary:

This book constitutes the thoroughly refereed post-workshop proceedings of the Third International Workshop, TYPES'99, organized by the ESPRIT Working Group 21900, in L keberg, Sweden, in June 1999.The 11 revised full papers presented in the volume were carefully reviewed and selected during two rounds of refereeing. All current issues on type theory and type systems and their applications to programming and proof theory are addressed.

Contents:

• Specification and verification of a formal system for structurally recursive functions / Andreas Abel
• A predicative strong normalisation proof for a [lambda]-calculus with interleaving inductive types / Andreas Abel and Thorsten Altenkirch
• Polymorphic intersection type assignment for rewrite systems with abstraction and [beta]-rule / Steffen van Bakel, Franco Barbanera, and Maribel Fernández
• Computer-assisted mathematics at work (the Hahn-Banach theorem in Isabelle/Isar) / Gertrud Bauer and Markus Wenzel
• Specification of a smart card operating system / Gustavo Betarte ... [et al.]
• Implementation techniques for inductive types in plastic / Paul Callaghan and Zhaohui Luo
• A co-inductive approach to real numbers / Alberto Ciaffaglione and Pietro Di Gianantonio
• Information retrieval in a Coq proof library using type isomorphisms / David Delahaye
• Memory management : an abstract formulation of incremental tracing / Healfdene Goguen, Richard Brooksby, and Rod Burstall
• The three gap theorem (Steinhaus conjecture) / Micaela Mayero
• Formalising formulas-as-types-as-objects / Qiao Haiyan.

Notes:

Includes bibliographical references and index.

ISBN:

3540415173

OCLC:

50418389