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