KI-Beratung Beta
Vor Ort
Merkzettel Warenkorb
  • Produktbild: Extensional Constructs in Intensional Type Theory
  • Produktbild: Extensional Constructs in Intensional Type Theory
- 13%

Extensional Constructs in Intensional Type Theory

Aus der Reihe Distinguished Dissertations
13% sparen

129,99 € UVP 149,79 €

inkl. gesetzl. MwSt., Versandkostenfrei

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

22.09.2011

Abbildungen

XII, 216 p.

Verlag

Springer London

Seitenzahl

216

Maße (L/B/H)

23,5/15,5/1,3 cm

Gewicht

359 g

Auflage

Softcover reprint of the original 1st ed. 1997

Sprache

Englisch

ISBN

978-1-4471-1243-3

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

22.09.2011

Abbildungen

XII, 216 p.

Verlag

Springer London

Seitenzahl

216

Maße (L/B/H)

23,5/15,5/1,3 cm

Gewicht

359 g

Auflage

Softcover reprint of the original 1st ed. 1997

Sprache

Englisch

ISBN

978-1-4471-1243-3

Herstelleradresse

Springer-Verlag GmbH
Tiergartenstr. 17
69121 Heidelberg
DE

Email: ProductSafety@springernature.com

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)
  • Produktbild: Extensional Constructs in Intensional Type Theory
  • Produktbild: Extensional Constructs in Intensional Type Theory
  • 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.