Skip to content

Latest commit

 

History

History

recursive-representation-of-data

Monotone Recursive Types and Recursive Data Representation in Cedille

Under consideration for the Journal of Mathematical Structures in Computer Science

All code can be checked from everything.ced.

Utilities

  • cast.ced: type coercions
  • recType.ced: monotone recursive types in Cedille
  • functor.ced: functors and the associated identity and composition laws
  • functorThms.ced: some useful lemmas about functors, including the relation between functorality and positivity
  • utils.ced: useful datatypes (dependent products, unit) and signature functors (lists)

Main files

TODO