Bi-Intuitionistic Logics: A New Instance of an Old Problem. - Rajeev Goré; Ian Shillito (AiML, 2020)

A multi-labelled sequent calculus for Topo-Logic. - Ian Shillito (J. Log. Comput., 2020)

Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq. - Rajeev Goré; Revantha Ramanayake; Ian Shillito (TABLEAUX, 2021)

Direct elimination of additive-cuts in GL4ip: verified and extracted. - Ian Shillito; Rajeev Goré (AiML, 2022)

A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised. - Ian Shillito; Iris van der Giessen; Rajeev Goré; Rosalie Iemhoff (TABLEAUX, 2023)

A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. - Ian Shillito; Dominik Kirst (CPP, 2024)

Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. - Hugo Férée; Iris van der Giessen; Sam van Gool; Ian Shillito (IJCAR (2), 2024)

Semantical Analysis of Intuitionistic Modal Logics between CK and IK. - Jim de Groot; Ian Shillito; Ranald Clouston (CoRR, 2024)

Completeness of First-Order Bi-Intuitionistic Logic. - Dominik Kirst; Ian Shillito (CSL, 2025)

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. - Tim S. Lyon; Ian Shillito; Alwen Tiu (CSL, 2025)