Encoding Featherweight Java with assignment and immutability using the Coq proof assistant. - Julian Mackay; Hannes Mehnert; Alex Potanin; Lindsay Groves; Nicholas Cameron 001 (FTfJP@ECOOP, 2012)

The Billion-Dollar Fix - Safe Modular Circular Initialisation with Placeholders and Placeholder Types. - Marco Servetto; Julian Mackay; Alex Potanin; James Noble 001 (ECOOP, 2013)

Syntactically Restricting Bounded Polymorphism for Decidable Subtyping. - Julian Mackay; Alex Potanin; Jonathan Aldrich; Lindsay Groves (APLAS, 2020)

Holistic Specifications for Robust Programs. - Sophia Drossopoulou; James Noble 001; Julian Mackay; Susan Eisenbach (FASE, 2020)

Decidable subtyping for path dependent types. - Julian Mackay; Alex Potanin; Jonathan Aldrich; Lindsay Groves (Proc. ACM Program. Lang., 2020)

Holisitic Specifications for Robust Programs - Coq Model. - Sophia Drossopoulou; James Noble 001; Julian Mackay; Susan Eisenbach (Zenodo, 2020)

Rusty Links in Local Chains✱. - James Noble 001; Julian Mackay; Tobias Wrigstad (FTfJP@ECOOP, 2022)

Necessity Specifications for Robustness. - Julian Mackay; Sophia Drossopoulou; James Noble 001; Susan Eisenbach (CoRR, 2022)

Necessity specifications for robustness. - Julian Mackay; Susan Eisenbach; James Noble 001; Sophia Drossopoulou (Proc. ACM Program. Lang., 2022)

Necessity Specifications for Robustness. - Julian Mackay; Sophia Drossopoulou; James Noble 001; Susan Eisenbach (Zenodo, 2022)

Dafny vs. Dala: Experience with Mechanising Language Design. - James Noble 001; Julian Mackay; Tobias Wrigstad; Andrew Fawcet; Michael Homer (FTfJP@ECOOP, 2024)

Reasoning about External Calls. - Sophia Drossopoulou; Julian Mackay; Susan Eisenbach; James Noble 001 (CoRR, 2025)

Semantically Separating Nominal Wyvern for Usability and Decidability. - Yu Xiang Zhu; Amos Robinson; Sophia Roshal; Timothy Mou; Julian Mackay; Jonathan Aldrich; Alex Potanin (CoRR, 2025)