Lean is a modern, functional, dependently-typed programming language that allows both to write efficient code (with a foreign function interface to C), but at the same time can serve as a proof assistant, via the proofs-are-programs principle.
In this project, you will implement the semantics (e.g. interpreter or operational semantics) and type systems of very simple languages and prove properties about them.
For this, you will use Lean, which is both a programming language and a theorem prover.
The book Formal Reasoning about Programs would serve as an inspiration for potential formalizations.
In particular, you could explore the “mixed embeddings” (see References) technique, which claims to simplify the formalization of languages considerably.
Links: