Homotopy type theory is an interpretation of Martin-Lo ̈f’s constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for inten- sional 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 homotopi- cal 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.

Awodey, S., Gambino, N., Sojakova, K. (2012). Inductive types in homotopy type theory. In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2012) [10.1109/LICS.2012.21].

Inductive types in homotopy type theory

GAMBINO, Nicola;
2012-01-01

Abstract

Homotopy type theory is an interpretation of Martin-Lo ̈f’s constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for inten- sional 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 homotopi- cal 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.
Settore MAT/01 - Logica Matematica
27th Annual ACM/IEEE Symposium on Logic in Computer Science
2012
9
Awodey, S., Gambino, N., Sojakova, K. (2012). Inductive types in homotopy type theory. In Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2012) [10.1109/LICS.2012.21].
Proceedings (atti dei congressi)
Awodey, S; Gambino, N; Sojakova, K
File in questo prodotto:
File Dimensione Formato  
InductiveTypesInHomotopyTypeTheory.pdf

Solo gestori archvio

Descrizione: Main article
Dimensione 273.68 kB
Formato Adobe PDF
273.68 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10447/74875
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 25
  • ???jsp.display-item.citation.isi??? 18
social impact