Type theory in type theory using quotient inductive types

DOI10.1145/2837614.2837638zbMath1347.68045OpenAlexW2274485505WikidataQ61583695 ScholiaQ61583695MaRDI QIDQ2828239

Thorsten Altenkirch, Ambrus Kaposi

Publication date: 24 October 2016

Published in: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: http://eprints.nottingham.ac.uk/31169/

zbMATH Keywords

homotopy type theoryAgdalogical relationsmetaprogramminghigher inductive types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (27)

The construction of set-truncated higher inductive types ⋮ From realizability to induction via dependent intersection ⋮ Unnamed Item ⋮ On generalized algebraic theories and categories with families ⋮ Unnamed Item ⋮ Quotients by Idempotent Functions in Cedille ⋮ Finitary type theories with and without contexts ⋮ Normalization by evaluation for modal dependent type theory ⋮ Higher Structures in Homotopy Type Theory ⋮ A class of higher inductive types in Zermelo‐Fraenkel set theory ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Two-level type theory and applications ⋮ The \textsc{MetaCoq} project ⋮ Unnamed Item ⋮ Partiality, Revisited ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Constructing a universe for the setoid model ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Semantics of higher inductive types ⋮ Unnamed Item ⋮ Pointers in Recursion: Exploring the Tropics ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Towards a Cubical Type Theory without an Interval

This page was built for publication: Type theory in type theory using quotient inductive types