README.md

Cicada Instars

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, Recursion is not an option.
• lang3: Dependent type, Nominal algebraic datatype, Structural record type, Type in Type, Arbitrary recursion.
• lang4: Simply typed jojo, Sequent calculus.
• lang5: Untyped jojo, A theory of equivalence for untyped jojo (by placeholder value & application trace).

References

• 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

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.
  • The C4 RFC
• Style Guide
  • Observe the style of existing code and respect it.
• Code of Conduct

License

• GPLv3