This is a dedicated space for people to nerd out about semantics, programming languages, type theory, concurrency and any other field of theoretical CS! We’re a special interest group (SIG) within CompSoc, and we run frequent events for you to learn about various different topics within these fields.

We have weekly workshops where you can learn to use the Lean theorem prover, and learn to make your own programming language; ~monthly TypeSig Talks, where academics give introductory talks on their research; and we organise the world’s largest undergrad PL conference every year in reading week of semester two! 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! Oh, and all events come with free pizza 🍕.

To complement our Lean workshops, we run Advent of Proof every December, testing you with a range of theorem proving challenges released daily.

We also have regular pub socials at the Dagda Bar (nominative determinism?) every Sunday at 7pm, and an annual barbecue at the end of each academic year.

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

TypeSig ❤️ you!

Contact

If you want to get in touch with us, please ping the @committee role on our Discord server. We can also be reached via Instagram DM, but this may have a slower response time. For inquiries, please contact us at typesig@comp-soc.com.