Tech Stack
Python
Java
Linux
Git
Description
Complete framework for implementing and formally verifying a simple programming language. Includes OCaml parser/interpreter and Coq proofs for big-step and small-step semantics.
Project split into 1_Préliminaires (grammars & natural semantics rules), 2_PartiePrincipale (WHILEb-- and WHILEb implementations), and 3_ExtensionsOptionnelles (advanced parsing, lazy lists, memory, step-by-step mode).
- OCaml: WHILEb--.ml, WHILEb.ml, WHILEb_With_Spaces.ml — syntactic analysis + natural semantics execution.
- Rocq (Coq): TD6et7.v — proofs for Part 2.3 (SN) and Part 3.1 (SOS); French answers in 3-1-ANSWERS.txt.
- Extensions: advanced lexical/syntax analysis, lazy lists, memory management, config translation, interactive step debugger.
- Demonstrates rigorous approach to language design — relevant foundation for reliable systems and tooling.
Page Info
Syntax, semantics & proofs
Three-part project: theoretical grammars, OCaml analyzers/executors, and Coq proofs for SN and SOS semantics.
