Einzeltreffer — DigiBib

Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.

Comment: 19 pages; v2: added references and acknowledgements, removed appendix with Coq README file, updated URL for Coq files. To appear in the proceedings of LICS 2012

Titel:	Inductive types in homotopy type theory
Autor/in / Beteiligte Person:	Gambino, Nicola ; Sojakova, Kristina ; Awodey, Steve ; Awodey, S ; Gambino, N ; Sojakova, K
Link:	View record in OpenAIRE (Volltext) Volltext
Quelle:	LICS; (2012)
Veröffentlichung:	2012
Medientyp:	unknown
Schlagwort:	FOS: Computer and information sciences Computer Science - Logic in Computer Science 03B15, 03B70, 03F50 0102 computer and information sciences 01 natural sciences Computer Science::Logic in Computer Science FOS: Mathematics A¹ homotopy theory Category Theory (math.CT) 0101 mathematics Mathematics Homotopy lifting property Type theory, inductive types, homotopy-initial algebra Homotopy 010102 general mathematics Mathematics - Category Theory Intuitionistic type theory Mathematics - Logic Settore MAT/01 - Logica Matematica Logic in Computer Science (cs.LO) Algebra n-connected Type theory TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Proof theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Homotopy type theory Computer Science::Programming Languages Logic (math.LO)
Sonstiges:	Nachgewiesen in: OpenAIRE Sprachen: English Language: English Rights: OPEN

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.

Inductive types in homotopy type theory