Type theory in type theory using quotient inductive types
DOI10.1145/2837614.2837638zbMATH Open1347.68045OpenAlexW2274485505WikidataQ61583695 ScholiaQ61583695MaRDI QIDQ2828239FDOQ2828239
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/
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
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)
Cited In (33)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Transpension: the right adjoint to the Pi-type
- The \textsc{MetaCoq} project
- Two-level type theory and applications
- A class of higher inductive types in Zermelo‐Fraenkel set theory
- Quotients by Idempotent Functions in Cedille
- Constructing a universe for the setoid model
- Title not available (Why is that?)
- From realizability to induction via dependent intersection
- Semantics of higher inductive types
- POPLMark reloaded: Mechanizing proofs by logical relations
- A Syntax for Higher Inductive-Inductive Types
- Title not available (Why is that?)
- Quotients over Minimal Type Theory
- The construction of set-truncated higher inductive types
- Partiality, Revisited
- Normalization by Evaluation for Typed Weak lambda-Reduction
- Title not available (Why is that?)
- Higher Structures in Homotopy Type Theory
- Finitary type theories with and without contexts
- Normalization for multimodal type theory
- Normalization by evaluation for modal dependent type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Towards a Cubical Type Theory without an Interval
- Title not available (Why is that?)
- 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)
