Welcome to TypeSig!

This is a dedicated space for people to nerd out about semantics, type theory, programming languages, logic, and everything inbetween! We’re a brand new special interest group (SIG) within CompSoc, and we’re planning to run frequent events for you to learn about various different topics within the field.

We have weekly hacking sessions where you can learn to use the Lean theorem prover, and (roughly) monthly TypeSig Talks, where academics will give introductory talks on their research (both of these events have free pizza 🍕). Everything is designed to be beginner-friendly, so don’t worry if you haven’t got any experience - this is the perfect place to learn!

We also have a Discord server for announcements and general discussion. This is the best way to keep up with us, so do join and say hello!

The image above is a subset of our current committee with Phil Wadler, who’s very excited about our existence.