Tech Stack
Python
Java
Linux
Git
Description
Three-part academic project covering grammars, natural semantics (SN), syntactic analyzers, and formal verification in Rocq.
- OCaml parsers and executors for WHILEb-- and WHILEb with whitespace-tolerant parsing.
- Natural semantics rules and operational semantics (SOS) with proofs in TD6et7.v.
- Optional extensions: lazy lists, memory management, step counters, and interactive execution.
Page Info
Syntax, semantics & proofs
OCaml interpreters for WHILE variants plus Coq proofs for natural and operational semantics.