The Proofs and Programs Club @ RHUL
What do we do?
Weekly meetups
(Thursdays, starting Oct 29th, in the Bedford Labs)
We meet every week to learn about logic, proof
assistants, certified programs, and programming language theory.
We are currently using the Lean
language/proof assistant, and we are following the Functional Programming in Lean (FPIL) book.
The Lean Game Server has a gamiefied way of learning (but it is best to start with the FPIL book).
In the past, we have used the Isabelle proof assistant and we followed the
Programming and Proving in
Isabelle/HOL book.
We have used the ROCQ proof assistant and we learned it using
the
Software Foundations books.
Research projects
We are currently investigating the following topics (available as UROP projects to RHUL students):
Who are we?
Organisers
Past Students
- Ben Collins (UROP 2022, UROP 2023)
- Isaac Joseph (UROP 2022, UROP 2023)
Contact us
Find us on Discord, contact any of the organisers for an invitation.