Twenty-five years of constructive type theory [[electronic resource] ] : proceedings of a congress held in Venice, October 1995 / / edited by Giovanni Sambin and Jan M. Smith
(Visualizza in formato marc)
(Visualizza in BIBFRAME)
| Titolo: |
Twenty-five years of constructive type theory [[electronic resource] ] : proceedings of a congress held in Venice, October 1995 / / edited by Giovanni Sambin and Jan M. Smith
|
| Pubblicazione: | Oxford, : Clarendon Press |
| New York, : Oxford University Press, 1998 | |
| Descrizione fisica: | 1 online resource (292 p.) |
| Disciplina: | 511.3 |
| Soggetto topico: | Type theory |
| Logic, Symbolic and mathematical | |
| Soggetto genere / forma: | Electronic books. |
| Altri autori: |
SambinGiovanni
SmithJan M
|
| Note generali: | Previously issued in print: Oxford: Clarendon Press, 1998. |
| Nota di bibliografia: | Includes bibliographical references. |
| Nota di contenuto: | 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 | |
| Sommario/riassunto: | 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. |
| Titolo autorizzato: | Twenty-five years of constructive type theory |
| ISBN: | 0-19-191654-4 |
| 1-280-81972-3 | |
| 9786610819720 | |
| 0-19-158903-9 | |
| Formato: | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione: | Inglese |
| Record Nr.: | 9910456015503321 |
| Lo trovi qui: | Univ. Federico II |
| Opac: | Controlla la disponibilità qui |
Serie:
Oxford logic guides ; ; 36.
Oxford science publications.