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.
Generating Mutually Recursive Definitions
Currently MetaOCaml can only build recursive groups whose size is hard-coded in the generating program. The general case requires something other than quotation, and seemingly weakens static guarantees on the resulting code. We describe the challenges and propose a new language construct for assuredly generating binding groups of arbitrary size – illustrating with a collection of examples for mutual, n-ary, heterogeneous, value and polymorphic recursion.
Let(rec) Insertion Without Effects, Lights or Magic
We show how one can understand let insertion, and hence implement it in plain OCaml. We give the first denotational semantics of let(rec)-insertion, which does not rely on any effects at all. The formalization has guided the implementation of let(rec) insertion in the current version of MetaOCaml.
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
Minimal implementations for dependent type checking and elaboration
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specifications serve directly as implementations, being programs in the language Lambda Prolog
General Recursion via Coinductive Types
To every type A we associate a type of partial elements Aᵛ, coinductively generated by two constructors: the first, ⸢α⸣ just returns an element α: A; the second, ▷x, adds a computation step to a recursive element x: Aᵛ. We show how this simple device is sufficient to formalize all recursive functions between two given types.
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.