by Mathews George
16 April 2024
I am Mathews George, a first year Computer Science PhD student at Heriot-Watt University, Edinburgh. With the help of SICSA, I was able to attend the Midlands Graduate School (MGS) 2024 which took place at the University of Leicester from 8th-12th April 2024.
About MGS
MGS is a programme aimed primarily at PhD students for providing a sound basis for research in the Foundations of Computing. It happens once a year and is organized by universities of Leicester, Birmingham, Nottingham, and Sheffield. This year was the 25th anniversary of MGS. The topics discussed in MGS primarily revolves around type theory, category theory and proof-theory. There are also exercise sessions associated each of the courses in MGS.
Highlights of my MGS participation
This year there were 7 courses in MGS. Out of which 3 were introductory ones, and 4 were advanced courses. I focused on 4 courses, namely: Category theory, Proof-theory, Type-theory and Synthetic Homotopy theory with HoTT. I attended exercises sessions for Category-theory and Synthetic Homotopy theory.
My work revolves around proving things in the proof-assistant Coq which is based on a type-theory known as Calculus of Inductive Constructions. However, all the above-mentioned subjects are related by a beautiful principle known as Curry-Howard Isomorphism. As a relative beginner to this field, I was not aware of how all these fields are connected, in other words, I could not see the bigger picture. The most important thing that I gained from MGS is that now I’m able to see where all these different but highly related sub-fields fit in the bigger picture. Also, now I’m really interested in Homotopy Type Theory (HoTT) which can be considered as an alternative (to set-theory) foundation for Mathematics.
I was able to meet many awesome researchers including one who is an active advocate of proof-assistants in formalizing Mathematics. We also had a trip to St Marys de Castro church and had dinner together. During dinner we had discussions on some interesting topics, and about the connections between Category theory and Functional Programming. This was really enlightening.