A nascent programming language as formal deduction system for the foundations of mathematics.
npm install @xieyuheng/cicadaA nascent programming language as formal deduction system for the foundations of mathematics.
- 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.
- Parsing:
- CFG: https://en.wikipedia.org/wiki/Context-free_grammar
- Earley parser: https://en.wikipedia.org/wiki/Earley_parser
- IXML: https://homepages.cwi.nl/~steven/ixml
- Lambda calculus:
- https://en.wikipedia.org/wiki/Lambda_calculus
- https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
- System T: https://en.wikipedia.org/wiki/Dialectica_interpretation
- 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
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.
- The C4 RFC
- Style Guide
- Observe the style of existing code and respect it.
- Code of Conduct
- GPLv3