2-Dimensional Directed Type Theory

DOI10.1016/j.entcs.2011.09.026zbMath1343.03051OpenAlexW1987700231WikidataQ113318219 ScholiaQ113318219MaRDI QIDQ5739362

Robert Harper, Daniel R. Licata

Publication date: 15 July 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2011.09.026

zbMATH Keywords

category theorytype theorydependent typeshomotopy type theory

Mathematics Subject Classification ID

Related Items (7)

Towards a directed homotopy type theory ⋮ Homotopical patch theory ⋮ Higher Structures in Homotopy Type Theory ⋮ Bicategorical type theory: semantics and syntax ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A type theory for synthetic $\infty$-categories

Uses Software

• Coq
• Twelf
• MiniAgda

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The identity type weak factorisation system
• Substitution: A formal methods case study using monads and transformations
• A universe of binding and computation
• Typed compilation of inclusive subtyping
• Types are weak ω -groupoids
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Two-dimensional models of type theory
• Homotopy theoretic models of identity types
• Weak ω-Categories from Intensional Type Theory
• Coercive subtyping
• Functorial ML
• de Bruijn notation as a nested datatype
• Implicit coercions in type systems
• Indexed containers
• Practical Programming with Higher-Order Encodings and Dependent Types
• Types for Proofs and Programs

This page was built for publication: 2-Dimensional Directed Type Theory