Type theory in type theory using quotient inductive types

DOI10.1145/2837614.2837638MaRDI QIDQ2828239zbMATH OpenOpenAlexWikidataFDO

Authors 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

Agdahigher inductive typeshomotopy type theorylogical relationsmetaprogramming

Mathematics Subject Classification ID

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

Recommendations

• Quotient inductive-inductive types
• Quotients, inductive types, and quotient inductive types
• Constructing infinitary quotient-inductive types
• Inductive types in homotopy type theory
• Type theory based on dependent inductive and coinductive types
• Equational theories for inductive types
• scientific article; zbMATH DE number 1302061
• scientific article; zbMATH DE number 2061701
• scientific article; zbMATH DE number 2182487
• scientific article; zbMATH DE number 1420793

Cited in

(43)

• Quotient inductive-inductive types
• The construction of set-truncated higher inductive types
• Constructing infinitary quotient-inductive types
• The \textsc{MetaCoq} project
• Constructing a universe for the setoid model
• From realizability to induction via dependent intersection
• Towards formalizing categorical models of type theory in type theory
• Partiality, Revisited
• scientific article; zbMATH DE number 2185663 (Why is no real title available?)
• scientific article; zbMATH DE number 1927427 (Why is no real title available?)
• Towards a cubical type theory without an interval
• Formalizing type operations using the ``image type constructor
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• Semantics of higher inductive types
• Constructing higher inductive types as groupoid quotients
• A syntax for higher inductive-inductive types
• On generalized algebraic theories and categories with families
• Pointers in Recursion: Exploring the Tropics
• Cubical syntax for reflection-free extensional equality
• Guarded recursion in Agda via sized types
• Normalization by Evaluation for Typed Weak lambda-Reduction
• A cubical language for Bishop sets
• Quotients, inductive types, and quotient inductive types
• Quotients by idempotent functions in Cedille
• POPLMark reloaded: mechanizing proofs by logical relations
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• Large and infinitary quotient inductive-inductive types
• Signatures and induction principles for higher inductive-inductive types
• Quotients over Minimal Type Theory
• Finitary type theories with and without contexts
• Normalization by evaluation for modal dependent type theory
• Higher Structures in Homotopy Type Theory
• Big step normalisation for type theory
• For Finitary Induction-Induction, Induction is Enough
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Two-level type theory and applications
• Transpension: the right adjoint to the Pi-type
• Normalization for multimodal type theory
• A syntax for mutual inductive families
• Quotients in dependent type theory (invited talk)
• A sound and complete substitution algorithm for multimode type theory
• Second-order generalised algebraic theories: signatures and first-order semantics
• The category of iterative sets in homotopy type theory and univalent foundations

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2828239)