README
Cicada Language
A nascent programming language as formal deduction system for the foundations of mathematics.
Contents
- partech: Parsing Techniques, DSL for CFG, General CFG parsers.
- lang0: Untyped lambda calculus.
- lang1: Simply typed lambda calculus, Natural number, Primitve recursive combinator.
- lang2: The Little Typer, Type in Type, No recursion.
- lang3: Dependent type, Nominal algebraic datatype, Structural record type, Fulfilling type, Type in Type, Arbitrary recursion.
References
- Parsing:
- Lambda calculus:
- Pie:
- Racket implementation: https://davidchristiansen.dk/tutorials/nbe
- Haskell implementation: https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf
- Foundations of mathematics:
- How I became interested in foundations of mathematics
- by Vladimir Voevodsky, at the 9th Asian Science Camp, Thailand, 2015
- Lecture about Univalent Foundations at the Institut Henri Poincaré
- by Vladimir Voevodsky, at the Institut Henri Poincaré, 2014
- How I became interested in foundations of mathematics
Community
Contributions are welcome, see current TODO list for tasks.
(Please add yourself to the AUTHORS list if you made any contributions.)
- We enforce C4 as collaboration protocol.
- Style Guide
- Observe the style of existing code and respect it.
- Code of Conduct