Twenty-five years of constructive type theory : proceedings of a congress held in Venice, October 1995 / edited by Giovanni Sambin and Jan M. Smith.

Format:

Book

Contributor:

Sambin, Giovanni.

Smith, Jan M.

Series:

Oxford logic guides ; 36.

Oxford science publications.

Oxford logic guides ; 36

Oxford science publications

Language:

English

Subjects (All):

Type theory--Congresses.

Type theory.

Logic, Symbolic and mathematical--Congresses.

Logic, Symbolic and mathematical.

Physical Description:

1 online resource (292 p.)

Edition:

1st ed.

Other Title:

25 years of constructive type theory

Place of Publication:

Oxford : Clarendon Press ; New York : Oxford University Press, 1998.

Language Note:

English

Summary:

Martin-Löf type theory is an important and practical formalisation of the foundations of mathematics. This volume celebrates the 25th anniversary of the birth of the subject, and is a record of areas of activity and of its early development.

Contents:

Cover; Contents; 1. Yet another constructivization of classical logic; 2. Extension of Martin-Löf's type theory with record types and subtyping; 3. Type-theoretical checking and philosophy of mathematics; 4. The Hahn-Banach theorem in type theory; 5. A realizability interpretation of Martin-Löf's type theory; 6. The groupoid interpretation of type theory; 7. Analytic program derivation in type theory; 8. An intuitionistic theory of types; 9. On storage operators; 10. On universes in type theory; 11. How to believe a machine-checked proof

12. Building up a toolbox for Martin-Löf's type theory: subset theory13. An introduction to well-ordering proofs in Martin-Löf's type theory; 14. Variable-free formalization of the Curry-Howard theory; 15. The forget-restore principle: a paradigmatic example

Notes:

Previously issued in print: Oxford: Clarendon Press, 1998.

Includes bibliographical references.

ISBN:

0-19-191654-4

1-280-81972-3

9786610819720

0-19-158903-9

OCLC:

714569778