Mini MLTT Machine

Mini MLTT Machine (mmm) is a Agda-like, dependently typed toy language.

Features

• inductive data type and pattern matching
• holes and implicit arguments
• dependent pattern matching

References

Indentation Sensitive Lexical Analysis:

• Agda

Bidirectional Type Inference:

• Bidirectional Typing Rules: A Tutorial, Christiansen.
• Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell Version), Christiansen.
• Elaboration with first-class implicit function types, Kovács.
• Towards a practical programming language based on dependent type theory, Norell.
• Bidirectional Elaboration of Dependently Typed Programs, Ferreira and Pientka.
• Local Type Inference, Pierce.
• Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types, Dunfield et al.
• A quick look at impredicativity, Serrano et al.
• Bidirectional Typing, Dunfield and Krishnaswami.

Row Polymorphism:

• Extensible records with scoped labels, Leijen.
• Polymorphic Records for Dynamic Languages, Castagna and Peyrot.

Dependent Pattern Matching:

• Eliminating Dependent Pattern Matching, Goguen et al.
• Elaborating dependent (co)pattern matching, Cockx and Abel.
• Pattern matching without K, Cockx et al.
• A simpler encoding of indexed types, Zhang.

Codebases:

• blott, Gratzer and Sterling.
• minimal MLTT implementation step-by-step, Guest0x0.
• elaboration-zoon, Kovács.
• ShiTT, KonjacSource.
• Mini Moonbit Machine, waterlens and flaotshadow.