Coq Interpreter Playground

Multiple examples of interpreters (with fuel), written in Coq.

CPS transformer(CPS.v)

A CPS transformer and evaluator of a functional language featuring raise and handle operations.

λ-calculus with modules

• Without recursion, using options (ShadowInterpOption.v)
• Without recursion, using lists (ShadowInterpList.v)
• With recursion, using lists (ShadowInterpRec.v)
• With recursion, add Peano naturals, using lists (ShadowInterpMatchList.v)
• With recursion, add Peano naturals, remember constraints (ShadowInterpMatchLazy.v)
• With recursion, add Peano naturals, remember constraints, use destructor (ShadowInterpMatchEager.v)
• With recursion, add general constructors, remember constraints (ShadowInterpMatchGuard.v)