Inductive types in homotopy type theory

Nicola Gambino, Kristina Sojakova, Steve Awodey

Risultato della ricerca: Otherpeer review

18 Citazioni (Scopus)

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.
Lingua originaleEnglish
Numero di pagine9
Stato di pubblicazionePublished - 2012

All Science Journal Classification (ASJC) codes

  • Computer Science (miscellaneous)
  • Logic

Fingerprint Entra nei temi di ricerca di 'Inductive types in homotopy type theory'. Insieme formano una fingerprint unica.

Cita questo