Quotients by idempotent functions in Cedille

DOI10.1007/978-3-030-47147-7_1zbMATH Open1503.68038OpenAlexW3023913990MaRDI QIDQ5098733FDOQ5098733

Andrew Marmaduke, Christopher Jenkins, Aaron Stump

Publication date: 30 August 2022

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

Full work available at URL: https://doi.org/10.1007/978-3-030-47147-7_1

Recommendations

• Defining functions on equivalence classes
• scientific article; zbMATH DE number 2003152
• scientific article; zbMATH DE number 2185663
• scientific article; zbMATH DE number 1841843
• Quotients, inductive types, and quotient inductive types

zbMATH Keywords

type theoryquotientsCedillequotient types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• The calculus of constructions
• Packaging Mathematical Structures
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• Codifying guarded definitions with recursive schemes
• Title not available (Why is that?)
• The construction of set-truncated higher inductive types
• Pragmatic Quotient Types in Coq
• The calculus of dependent lambda eliminations
• Efficient Mendler-style lambda-encodings in Cedille
• Title not available (Why is that?)
• Type theory in type theory using quotient inductive types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Cited In (3)

• Title not available (Why is that?)
• Quotients of Bounded Natural Functors
• Impredicative encodings of inductive-inductive data in Cedille

Uses Software

• Cubical agda

This page was built for publication: Quotients by idempotent functions in Cedille

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