Extensional Constructs in Intensional Type Theory: Distinguished Dissertations
Autor Martin Hofmannen Limba Engleză Paperback – 22 sep 2011
Din seria Distinguished Dissertations
- 20% Preț: 290.51 lei
- 15% Preț: 633.68 lei
- 15% Preț: 645.47 lei
- 20% Preț: 654.05 lei
- 20% Preț: 647.79 lei
- 20% Preț: 994.92 lei
- 20% Preț: 648.26 lei
- 20% Preț: 328.60 lei
- 20% Preț: 641.34 lei
- 20% Preț: 328.09 lei
- 20% Preț: 325.30 lei
- 20% Preț: 639.52 lei
- 20% Preț: 640.69 lei
- 20% Preț: 603.37 lei
- 20% Preț: 637.56 lei
- 20% Preț: 643.30 lei
- 20% Preț: 640.51 lei
- 20% Preț: 640.19 lei
- 20% Preț: 325.63 lei
Preț: 926.94 lei
Preț vechi: 1158.68 lei
-20% Nou
Puncte Express: 1390
Preț estimativ în valută:
177.39€ • 184.52$ • 146.45£
177.39€ • 184.52$ • 146.45£
Carte tipărită la comandă
Livrare economică 15-29 aprilie
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9781447112433
ISBN-10: 1447112431
Pagini: 232
Ilustrații: XII, 216 p.
Dimensiuni: 155 x 235 x 12 mm
Greutate: 0.33 kg
Ediția:Softcover reprint of the original 1st ed. 1997
Editura: SPRINGER LONDON
Colecția Springer
Seria Distinguished Dissertations
Locul publicării:London, United Kingdom
ISBN-10: 1447112431
Pagini: 232
Ilustrații: XII, 216 p.
Dimensiuni: 155 x 235 x 12 mm
Greutate: 0.33 kg
Ediția:Softcover reprint of the original 1st ed. 1997
Editura: SPRINGER LONDON
Colecția Springer
Seria Distinguished Dissertations
Locul publicării:London, United Kingdom
Public țintă
ResearchCuprins
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.