This is a list of prior art that have influenced Peridot's design and implementation in major ways.
Two-Level Type Theory and Applications
We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories.
Experimental staged language with dependent types
MetaML: Multi-Stage Programming with Explicit Annotations
We introduce MetaML, a practically-motivated, statically typed multi-stage programming language. MetaML allows the programmer to construct, combine, and execute code fragments in a type-safe manner.
Moebius: Metaprogramming using Contextual Types
We describe the foundation of the metaprogramming language, Moebius, which supports the generation of polymorphic code and, more importantly the analysis of polymorphic code via pattern matching.
Contextual modal type theory provides an elegant, uniform foundation for understanding meta-variables and explicit substitutions. We sketch some applications in functional programming and logical frameworks
Elaborating dependent (co)pattern matching
We present an algorithm elaborating definitions by dependent copattern matching to a core language with inductive datatypes, coinductive record types, an identity type, and constants defined by well-typed case trees.
Minimal implementations for dependent type checking and elaboration
Projects exploring a similar design space - leveraging the compile time vs runtime separation - but from perspectives other than that of two level type theory.
Lisp dialect featuring highly flexible syntax, arbitrary compile-time evaluation, and static types!
Functional language with intensional polymorphism and first-class staging.