An intermediate verification language
To view and edit the sources, open this folder with VS Code.
To manage the project from the command line, see the Makefile. For example, to verify the code, run
make verify
To edit the documentation, use Madoko source
About the implementation: B3 syntax, raw AST, and printing
- Parser: input characters -> raw AST -- RawAst.WellFormed says whether or not raw AST is well-formed, but doesn't give good error messages
- Resolver: raw AST -> resolved AST -- generates a good error message if RawAst.WellFormed does not hold -- ensures Ast.WellFormed
- TypeChecker: operates on a well-formed resolved AST -- check if AST is type correct -- ensures TypeCorrect
- Verifier: resolved AST -> calls to Solver.{extend,prove}
- Semantics: gives co-inductive big-step semantics for raw AST (soon: resolved AST)
- Somewhere, should also do macro expansions (before Resolver, operating on raw AST) and closure lifting (probably best done on resolved AST)