fun-with-types
This is a toy project for the construction of a lisp-like programming language using the Extended Calculus of Constructions. While the full thing is impossible (since the calculus does not support eval or recursive functions), hopefully it'll be possible to at least give the language a lispy feel.
planned features
- Implementation of the ECC core - dependent products, strong sums and their canonical objects and operations.
- Inductive schemata for defining new data types.
- syntactic sugar for abstract theories, function argument destructuring, struct creation, etc.
- support for macros