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.
- 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)