Zero-Cost Coercions for Program and Proof Reuse

Cedille code accompanying the paper draft (available on arXiv) authored by Larry Diehl and Aaron Stump.

We have also developed a generic version of this development, where identity functions are defined via propositional equality, rather than definitional equality.

Code from the paper

• Datatype Definitions
  • Nat
  • List
  • Vec
  • VecL
• Coercion Functions
  • Identity Coercions
  • Nested Identity Coercions
• Vector Examples
  • Definitions
  • Reuse
• List Examples
  • Definitions (including nested)
  • Reuse
  • Nested Reuse

Cedille Language

Download and unpack the Cedille prerelease, then follow INSTALL.txt in cedille-prerelease for installation instructions.