The Lambda Calculus is a model of computation first formalised by Alonzo Church in the 1930s. It is a basis for all computation, (just like Turing Machines), yet unlike Turing Machines, presentations of the Lambda Calculus tend to be abstract. As far as we know, they tend to be either purely on pen-and-paper, or written within a programming language themselves. We hope to be able to break that trend, by making a physical evaluator for the lambda calculus. Some inspirations are listed below -

• Alligator Eggs
• Dynamic Labyrinths
• Lambda Calculus in 383 Bytes

This is primarily a learning project, where we want to build a language server protocol to figure out how one works. Currently, we plan to do it for the Pyret programming language.

HAX is a verification toolchain for Rust programs. It works by taking Rust programs, and trying to translate them into formal languages such as F*, LEAN4, and Rocq. The project title is self explanatory.

The HAX toolchain isn't all encompassing, and there are many libraries of Rust code that are not just Rust code. For example, they may use FFI to call C or LLVM code. The documentation within these projects can be very hard to follow, and sometimes just wrong. Thus, by writing formal specifications in the form of clean, functional, Rust code that mirrors their behaviour, allowing tools like HAX to reason about them.

CSLib is a very new library for formalised computer science in LEAN4, inspired by the success of Mathlib for formalised mathematics. We want to contribute to it.

Software Foundations is a phenomenal resource for getting familiar with the Rocq theorem prover, and we want to write a LEAN4 translation in a manner that respects the specific differences between Rocq and LEAN4, while also considering the current trends of best practices within the LEAN community.