Proofs and Programs Club @ RHUL

What do we do?

Weekly meetups

We meet every week to learn about logic, proof assistants, certified programs, and programming language theory. We are currently using the Agda proof assistant, and we are following tutorials derived from various resources including:

Programming Language Foundations in Agda
2024 Agda course at the University of Padova
The Natural Number Game - this is for Lean rather than Agda

We have used the Isabelle proof assistant and we followed the Programming and Proving in Isabelle/HOL book. We have used the Coq 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):

Mechanisation of Subtyping for Go 1.18
Correct and Certified Regular Expressions
Coq Formalisation of Recursive Adaptive Grammars

Who are we?

Organisers

Felix Bradley
Francisco Ferreira
Angeliki Koutsoukou-Argyraki
Julien Lange (coordinator)
Chris Purdy

Reuben Rowe

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.