Aaron Stump
2018-09-14 19:38:13 UTC
Dear Agda community,
We are pleased to announce the public release of Cedille 1.0.0. Cedille
implements an extrinsic pure type theory, in which datatypes with their
induction principles can be derived as lambda encodings. The details of
how this works are explained in several papers you can find on my web
page (a good starting one is "From Realizability to Induction via
Dependent Intersection"). Cedille is implemented in an Emacs mode
communicating with a backend. The backend is written in around 10kloc
of Agda -- and hence we feel justified advertising on this list. :-)
We have a Debian package for quick installation, or you can build from
sources following some instructions (INSTALL.txt in the repo).
Cedille's web page is https://cedille.github.io.
The 1.0.0 release is tagged on github here:
https://github.com/cedille/cedille/releases/tag/v1.0.0
Master is for development and could be broken, but the maintenance
branch for this release (and the one you might want to checkout) is:
https://github.com/cedille/cedille/tree/release-1.0
Sincerely, and gratefully to Agda on which this tool is based,
Aaron, for the Cedille development team
PS We welcome issues on the github issue tracker for installation
problems or other questions.
We are pleased to announce the public release of Cedille 1.0.0. Cedille
implements an extrinsic pure type theory, in which datatypes with their
induction principles can be derived as lambda encodings. The details of
how this works are explained in several papers you can find on my web
page (a good starting one is "From Realizability to Induction via
Dependent Intersection"). Cedille is implemented in an Emacs mode
communicating with a backend. The backend is written in around 10kloc
of Agda -- and hence we feel justified advertising on this list. :-)
We have a Debian package for quick installation, or you can build from
sources following some instructions (INSTALL.txt in the repo).
Cedille's web page is https://cedille.github.io.
The 1.0.0 release is tagged on github here:
https://github.com/cedille/cedille/releases/tag/v1.0.0
Master is for development and could be broken, but the maintenance
branch for this release (and the one you might want to checkout) is:
https://github.com/cedille/cedille/tree/release-1.0
Sincerely, and gratefully to Agda on which this tool is based,
Aaron, for the Cedille development team
PS We welcome issues on the github issue tracker for installation
problems or other questions.