|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910456015503321 |
|
|
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 |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Oxford, : Clarendon Press |
|
New York, : Oxford University Press, 1998 |
|
|
|
|
|
|
|
|
|
ISBN |
|
0-19-191654-4 |
1-280-81972-3 |
9786610819720 |
0-19-158903-9 |
|
|
|
|
|
|
|
|
Descrizione fisica |
|
1 online resource (292 p.) |
|
|
|
|
|
|
Collana |
|
Oxford logic guides ; ; 36 |
Oxford science publications |
|
|
|
|
|
|
|
|
Altri autori (Persone) |
|
SambinGiovanni |
SmithJan M |
|
|
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Type theory |
Logic, Symbolic and mathematical |
Electronic books. |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
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-LoÌf type theory is an important and practical formalisation of |
|
|
|
|