Cedille Developments

A showcase of interesting code and proof developments in Cedille.

Generic derivation of induction for impredicative encodings in Cedille

• Authors: Denis Firsov and Aaron Stump
• Venue: CPP'18
• Paper: http://firsov.ee/impred-ind/impred-ind.pdf

Efficient Mendler-Style Lambda-Encodings in Cedille

• Authors: Denis Firsov, Richard Blair, and Aaron Stump
• Venue: ITP'18
• Paper: https://arxiv.org/abs/1803.02473

Generic Zero-Cost Reuse for Dependent Types

• Authors: Larry Diehl, Denis Firsov, and Aaron Stump
• Venue: ICFP'18
• Paper: https://arxiv.org/abs/1803.08150

Monotone Recursive Types and Recursive Data Representations in Cedille

• Authors: Christopher Jenkins and Aaron Stump
• Venue: Under consideration for publication in the journal of Mathematical Structures in Computer Science
• Paper: https://arxiv.org/abs/2001.02828

Efficient Mendler Prime

• Authors: Larry Diehl, Denis Firsov, Richard Blair, and Aaron Stump
• Refactored version of the ITP'18 development, see the README

Quotients by Idempotent Functions in Cedille

• Authors: Andrew Marmaduke, Christopher Jenkins, Aaron Stump
• Venue: TFP'19

Efficient Lambda Encodings for Mendler-style Coinductive Types in Cedille

• Authors: Christopher Jenkins, Aaron Stump, Larry Diehl

Zero-Cost Constructor Subtyping

• Authors: Andrew Marmaduke, Christopher Jenkins, Aaron Stump
• Venue: ifl'20
• Paper: https://dl.acm.org/doi/abs/10.1145/3462172.3462194

A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedilled

• Author: Aaron Stump
• Venue: LFMTP'19
• Paper: http://eptcs.web.cse.unsw.edu.au/paper.cgi?LFMTP2019.6

Simulating Large Eliminations in Cedille

• Authors: Christopher Jenkins, Andrew Marmaduke, Aaron Stump
• Venue: TYPES'21
• Paper: https://drops.dagstuhl.de/opus/volltexte/2022/16778/

Impredicative Encodings of Inductive-Inductive Data in Cedille

• Authors: Andrew Marmaduke, Larry Diehl, Aaron Stump