Some inspirations for dependent types, MiniTT, Haskell's Bound library, etc.

• Mini-TT
  • the Mini-TT paper
  • Thierry Coquand's semantic type checking
  • the original implementation
  • Arnaud Bailly's implementation
• type checking in terms of Bound: cf. Dan Doel's UPTS, as referred to in a discussion about Bound in Morte
• David Christiansen's tiny dependent types (in F#)
• for Haskell's repline cf. Stephen Diehl's Write You a Haskell
• a series of blog posts by Andrej Bauer: How to implement dependent type theory I, and parts II, and III
• Olle Fredriksson's Sixty compiler:
  • Speeding up the Sixty compiler
  • https://github.com/ollef/sixten
  • https://github.com/ollef/sixty
• András Kovács' smalltt
• Ermine as a larger example of Haskell-Bound usage (expressions are terms there: in src/Ermine/Syntax/Term.hs)
  • https://github.com/ermine-language/ermine
  • https://github.com/ermine-language
  • https://ermine-language.github.io