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

Agdalogical relationshomotopy type theorymetaprogramminghigher inductive types

Mathematics Subject Classification ID

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

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

(38)

• Constructing infinitary quotient-inductive types
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• The \textsc{MetaCoq} project
• Transpension: the right adjoint to the Pi-type
• Two-level type theory and applications
• Constructing a universe for the setoid model
• A class of higher inductive types in Zermelo‐Fraenkel set theory
• Formalizing type operations using the ``image type constructor
• scientific article; zbMATH DE number 7168146 (Why is no real title available?)
• Towards a cubical type theory without an interval
• From realizability to induction via dependent intersection
• Large and infinitary quotient inductive-inductive types
• Semantics of higher inductive types
• Quotients, inductive types, and quotient inductive types
• Quotient inductive-inductive types
• Constructing higher inductive types as groupoid quotients
• Quotients over Minimal Type Theory
• The construction of set-truncated higher inductive types
• Towards formalizing categorical models of type theory in type theory
• Partiality, Revisited
• Normalization by Evaluation for Typed Weak lambda-Reduction
• scientific article; zbMATH DE number 2185663 (Why is no real title available?)
• Higher Structures in Homotopy Type Theory
• Finitary type theories with and without contexts
• Quotients by idempotent functions in Cedille
• Normalization for multimodal type theory
• Normalization by evaluation for modal dependent type theory
• POPLMark reloaded: mechanizing proofs by logical relations
• scientific article; zbMATH DE number 7559297 (Why is no real title available?)
• scientific article; zbMATH DE number 7559298 (Why is no real title available?)
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• Big step normalisation for type theory
• A syntax for higher inductive-inductive types
• scientific article; zbMATH DE number 1927427 (Why is no real title available?)
• On generalized algebraic theories and categories with families
• For Finitary Induction-Induction, Induction is Enough
• Pointers in Recursion: Exploring the Tropics

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)