Quotients by Idempotent Functions in Cedille

DOI10.1007/978-3-030-47147-7_1zbMath1503.68038OpenAlexW3023913990MaRDI QIDQ5098733

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)

Related Items (1)

Quotients of Bounded Natural Functors

Uses Software

• Cubical agda

Cites Work

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

This page was built for publication: Quotients by Idempotent Functions in Cedille