Logic, proofs & formalisation

Ian Shillito · Research Fellow

I am a Research Fellow at the University of Melbourne, working with Cezary Kaliszyk since July 2026. I study the mathematical and computational foundations of non-classical logics, with a focus on proof theory and computer-checked mathematics.

My research brings together proof theory, semantics and formalisation in Rocq. I investigate intuitionistic, bi-intuitionistic and modal logics: how to design calculi, prove cut-elimination and completeness, and compute uniform interpolants. Alongside syntactic methods, I work with Kripke, algebraic and topological semantics. I aim to formalise my results in the interactive theorem prover Rocq, formerly Coq.

Explore publications Curriculum vitae

Recent research

All publications and extended abstracts →

Background

Before moving to Melbourne, I was a Research Fellow at the University of Birmingham (2025–June 2026), working with Anupam Das on the UKRI-funded StrIP project, and at the Australian National University (2022–2024), working with Peter Höfner. I completed my PhD at ANU under the supervision of Rajeev Goré, following studies in philosophy and logic in Paris and the Logic Year in Amsterdam.

Recognition

• IJCAR 2024 best paper award — Mechanised uniform interpolation for modal logics K, GL and iSL.
• TABLEAUX 2023 best paper award — A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised.

Get in touch

You can reach me at ian.shillito@unimelb.edu.au. My papers are also listed on Google Scholar, and my formalisation projects are on GitHub.