Extensional Constructs in Intensional Type Theory presents a novel approach to the treatment of equality in Martin-Loef type theory (a basis for important work in mechanised mathematics and program verification). Martin Hofmann attempts to reconcile the two different ways that type theories deal with identity types. The book will be of interest particularly to researchers with mainly theoretical interests and implementors of type theory based proof assistants, and also fourth year undergraduates who will find it useful as part of an advanced course on type theory.
Extensional Constructs in Intensional Type Theory presents a novel approach to the treatment of equality in Martin-Loef type theory (a basis for important work in mechanised mathematics and program verification). Martin Hofmann attempts to reconcile the two different ways that type theories deal with identity types. The book will be of interest particularly to researchers with mainly theoretical interests and implementors of type theory based proof assistants, and also fourth year undergraduates who will find it useful as part of an advanced course on type theory.
Die Herstellerinformationen sind derzeit nicht verfügbar.
Autorenporträt
Prof. Dr. Martin Hofmann, lehrt an der Ludwig-Maximilians-Universität München, Institut für Informatik, Theoretische Informatik, Germany.
Inhaltsangabe
1. Introduction.- 1.1 Definitional and propositional equality.- 1.2 Extensional constructs.- 1.3 Method.- 1.4 Applications.- 1.5 Overview.- 2. Syntax and semantics of dependent types.- 2.1 Syntax for a core calculus.- 2.2 High-level syntax.- 2.3 Further type formers.- 2.4 Abstract semantics of type theory.- 2.5 Interpreting the syntax.- 2.6 Discussion and related work.- 3. Syntactic properties of propositional equality.- 3.1 Intensional type theory.- 3.2 Extensional type theory.- 3.3 Related work.- 4. Proof irrelevance and subset types.- 4.1 The refinement approach.- 4.2 The deliverables approach.- 4.3 The deliverables model.- 4.4 Model checking with Lego.- 4.5 Type formers in the model D.- 4.6 Subset types.- 4.7 Reinterpretation of the equality judgement.- 4.8 Related work.- 5. Extensionality and quotient types.- 5.1 The setoid model.- 5.2 The groupoid model.- 5.3 A dependent setoid model.- 5.4 Discussion and related work.- 6. Applications.- 6.1 Tarski's fixpoint theorem.- 6.2 Streams in type theory.- 6.3 Category theory in type theory.- 6.4 Encoding of the coproduct type.- 6.5 Some basic constructions with quotient types.- 6.6 ? is co-continuous-intensionally.- 7. Conclusions and further work.- A.1 Extensionality axioms.- A.2 Quotient types.- A.3 Further axioms.- Appendix B. Syntax.- Appendix C. A glossary of type theories.- Appendix D. Index of symbols.
1. Introduction.- 1.1 Definitional and propositional equality.- 1.2 Extensional constructs.- 1.3 Method.- 1.4 Applications.- 1.5 Overview.- 2. Syntax and semantics of dependent types.- 2.1 Syntax for a core calculus.- 2.2 High-level syntax.- 2.3 Further type formers.- 2.4 Abstract semantics of type theory.- 2.5 Interpreting the syntax.- 2.6 Discussion and related work.- 3. Syntactic properties of propositional equality.- 3.1 Intensional type theory.- 3.2 Extensional type theory.- 3.3 Related work.- 4. Proof irrelevance and subset types.- 4.1 The refinement approach.- 4.2 The deliverables approach.- 4.3 The deliverables model.- 4.4 Model checking with Lego.- 4.5 Type formers in the model D.- 4.6 Subset types.- 4.7 Reinterpretation of the equality judgement.- 4.8 Related work.- 5. Extensionality and quotient types.- 5.1 The setoid model.- 5.2 The groupoid model.- 5.3 A dependent setoid model.- 5.4 Discussion and related work.- 6. Applications.- 6.1 Tarski's fixpoint theorem.- 6.2 Streams in type theory.- 6.3 Category theory in type theory.- 6.4 Encoding of the coproduct type.- 6.5 Some basic constructions with quotient types.- 6.6 ? is co-continuous-intensionally.- 7. Conclusions and further work.- A.1 Extensionality axioms.- A.2 Quotient types.- A.3 Further axioms.- Appendix B. Syntax.- Appendix C. A glossary of type theories.- Appendix D. Index of symbols.
Es gelten unsere Allgemeinen Geschäftsbedingungen: www.buecher.de/agb
Impressum
www.buecher.de ist ein Internetauftritt der buecher.de internetstores GmbH
Geschäftsführung: Monica Sawhney | Roland Kölbl | Günter Hilger
Sitz der Gesellschaft: Batheyer Straße 115 - 117, 58099 Hagen
Postanschrift: Bürgermeister-Wegele-Str. 12, 86167 Augsburg
Amtsgericht Hagen HRB 13257
Steuernummer: 321/5800/1497
USt-IdNr: DE450055826
