molikto/ChihuahuaLang

PLT & structural editor playground

this is my

Programming Language Theory Playground

code here may not be complete or working at all

main stuff

• a structural editor

  

• dependent type theory type checker and compiled (JIT'ed) normalization by evaluation

  • it also implements subtyping for dependent records, and inductive types, but the soundness is not verified yet
  • code sample, you can run it in Parser.scala
  • tests
  • references
    • Full reduction at full throttle
    • A simple type-theoretic language: Mini-TT

smaller stuff

• eval for untyped lambda calculus and compiled (JIT'ed) normalization by evaluation (Full reduction at full throttle)