Combinatorial realizability models of type theory

DOI10.1016/j.apal.2013.05.002zbMath1323.03013arXiv1205.5527OpenAlexW2096221521MaRDI QIDQ385804

Michael A. Warren, Pieter J. W. Hofstra

Publication date: 11 December 2013

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1205.5527

zbMATH Keywords

realizabilityMartin-Löf type theoryhomotopy type theorygluinglogical relationsgroupoid semantics

Mathematics Subject Classification ID

Related Items (5)

Homotopy type theory and Voevodsky’s univalent foundations ⋮ Martin-Löf complexes ⋮ Models of HoTT and the Constructive View of Theories ⋮ Univalence for inverse diagrams and homotopy canonicity ⋮ Monoidal computer III: a coalgebraic view of computability and complexity (extended abstract)

Cites Work

• Unnamed Item
• Unnamed Item
• Martin-Löf complexes
• The identity type weak factorisation system
• Internal type theory
• Type Theory and Homotopy
• Intensional interpretations of functionals of finite type I

This page was built for publication: Combinatorial realizability models of type theory