Quotients by idempotent functions in Cedille

DOI10.1007/978-3-030-47147-7_1MaRDI QIDQ5098733zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

type theoryquotientsCedillequotient types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

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

Cites work

• scientific article; zbMATH DE number 1722663 (Why is no real title available?)
• scientific article; zbMATH DE number 2185663 (Why is no real title available?)
• scientific article; zbMATH DE number 2003152 (Why is no real title available?)
• scientific article; zbMATH DE number 1927427 (Why is no real title available?)
• scientific article; zbMATH DE number 2085175 (Why is no real title available?)
• scientific article; zbMATH DE number 1841843 (Why is no real title available?)
• scientific article; zbMATH DE number 1420793 (Why is no real title available?)
• Codifying guarded definitions with recursive schemes
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Efficient Mendler-style lambda-encodings in Cedille
• Packaging Mathematical Structures
• Pragmatic quotient types in Coq
• The calculus of constructions
• The calculus of dependent lambda eliminations
• The construction of set-truncated higher inductive types
• Theorem Proving in Higher Order Logics
• Type theory in type theory using quotient inductive types

Cited in

(3)

• scientific article; zbMATH DE number 1281943 (Why is no real title available?)
• Quotients of Bounded Natural Functors
• Impredicative encodings of inductive-inductive data in Cedille

Describes a project that uses

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)