Deterministic Expressions in C. - Michael Norrish (ESOP, 1999)

C formalised in HOL - Michael Norrish (1999)

The PROSPER Toolkit. - Louise A. Dennis; Graham Collins; Michael Norrish; Richard J. Boulton; Konrad Slind; Graham Robinson; Michael J. C. Gordon; Thomas F. Melham (TACAS, 2000)

Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. - Keith Wansbrough; Michael Norrish; Peter Sewell; Andrei Serjantov (ESOP, 2002)

Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets. - Michael Norrish; Peter Sewell; Keith Wansbrough (ACM SIGOPS European Workshop, 2002)

A Thread of HOL Development. - Michael Norrish; Konrad Slind (Comput. J., 2002)

Mechanising Hankin and Barendregt using the Gordon-Melham axioms. - Michael Norrish (MERLIN, 2003)

Complete Integer Decision Procedures as Derived Rules in HOL. - Michael Norrish (TPHOLs, 2003)

The PROSPER toolkit. - Louise A. Dennis; Graham Collins; Michael Norrish; Richard J. Boulton; Konrad Slind; Thomas F. Melham (Int. J. Softw. Tools Technol. Transf., 2003)

Recursive Function Definition for Types with Binders. - Michael Norrish (TPHOLs, 2004)

A formal treatment of the barendregt variable convention in rule inductions. - Christian Urban; Michael Norrish (MERLIN, 2005)

Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets. - Steve Bishop; Matthew Fairbairn; Michael Norrish; Peter Sewell; Michael Smith 008; Keith Wansbrough (SIGCOMM, 2005)

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. - Michael Norrish; Konrad Slind (TPHOLs, 2005)

Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. - Steve Bishop; Matthew Fairbairn; Michael Norrish; Peter Sewell; Michael Smith 008; Keith Wansbrough (POPL, 2006)

Mechanising lambda-calculus using a classical first order theory of terms with permutations. - Michael Norrish (High. Order Symb. Comput., 2006)

Barendregt's Variable Convention in Rule Inductions. - Christian Urban; Stefan Berghofer; Michael Norrish (CADE, 2007)

Types, bytes, and separation logic. - Harvey Tuch; Gerwin Klein; Michael Norrish (POPL, 2007)

Proof Pearl: De Bruijn Terms Really Do Work. - Michael Norrish; René Vestergaard (TPHOLs, 2007)

A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. - Tom Ridge; Michael Norrish; Peter Sewell (FM, 2008)

A Brief Overview of HOL4. - Konrad Slind; Michael Norrish (TPHOLs, 2008)

Verified, Executable Parsing. - Aditi Barthwal; Michael Norrish (ESOP, 2009)

seL4: formal verification of an OS kernel. - Gerwin Klein; Kevin Elphinstone; Gernot Heiser; June Andronick; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (SOSP, 2009)

Mind the Gap. - Simon Winwood; Gerwin Klein; Thomas Sewell; June Andronick; David A. Cock; Michael Norrish (TPHOLs, 2009)

Rewriting Conversions Implemented with Continuations. - Michael Norrish (J. Autom. Reason., 2009)

A Formalisation of the Normal Forms of Context-Free Grammars in HOL4. - Aditi Barthwal; Michael Norrish (CSL, 2010)

(Nominal) Unification by Recursive Descent with Triangular Substitutions. - Ramana Kumar; Michael Norrish (ITP, 2010)

Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. - Aditi Barthwal; Michael Norrish (WoLLIC, 2010)

seL4: formal verification of an operating-system kernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (Commun. ACM, 2010)

Mechanised Computability Theory. - Michael Norrish (ITP, 2011)

Reasoning with Data-Centric Business Processes - Andreas Klaus Bauer; Peter Baumgartner 001; Michael Norrish (CoRR, 2012)

Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax. - James Cheney; Michael Norrish; René Vestergaard (J. Autom. Reason., 2012)

Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. - Michael Norrish; Brian Huffman (ITP, 2013)

Tableaux for Verification of Data-Centric Processes. - Andreas Bauer 002; Peter Baumgartner 001; Martin Diller; Michael Norrish (TABLEAUX, 2013)

A String of Pearls: Proofs of Fermat's Little Theorem. - Hing-Lun Chan; Michael Norrish (J. Formaliz. Reason., 2013)

Beagle as a HOL4 external ATP method. - Thibault Gauthier; Cezary Kaliszyk; Chantal Keller; Michael Norrish (PAAR@IJCAR, 2014)

An Approach for Proving the Correctness of Inspector/Executor Transformations. - Michael Norrish; Michelle Mills Strout (LCPC, 2014)

CakeML: a verified implementation of ML. - Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens (POPL, 2014)

A mechanisation of some context-free language theory in HOL4. - Aditi Barthwal; Michael Norrish (J. Comput. Syst. Sci., 2014)

Exploiting Symmetries by Planning for a Descriptive Quotient. - Mohammad Abdulaziz; Michael Norrish; Charles Gretton (IJCAI, 2015)

Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. - Mohammad Abdulaziz; Charles Gretton; Michael Norrish (ITP, 2015)

Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. - Hing-Lun Chan; Michael Norrish (ITP, 2015)

Stop and go: understanding yieldpoint behavior. - Yi Lin; Kunshan Wang; Stephen M. Blackburn; Antony L. Hosking; Michael Norrish (ISMM, 2015)

Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development. - Kunshan Wang; Yi Lin; Stephen M. Blackburn; Michael Norrish; Antony L. Hosking (SNAPL, 2015)

A new verified compiler backend for CakeML. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (ICFP, 2016)

Rust as a language for high performance GC implementation. - Yi Lin; Stephen M. Blackburn; Antony L. Hosking; Michael Norrish (ISMM, 2016)

A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds. - Mohammad Abdulaziz; Charles Gretton; Michael Norrish (ICAPS, 2017)

Verified Characteristic Formulae for CakeML. - Armaël Guéneau; Magnus O. Myreen; Ramana Kumar; Michael Norrish (ESOP, 2017)

Verifying efficient function calls in CakeML. - Scott Owens; Michael Norrish; Ramana Kumar; Magnus O. Myreen; Yong Kiam Tan (Proc. ACM Program. Lang., 2017)

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. - Son Ho; Oskar Abrahamsson; Ramana Kumar; Magnus O. Myreen; Yong Kiam Tan; Michael Norrish (IJCAR, 2018)

Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. - Simon Jantsch; Michael Norrish (ITP, 2018)

Hop, Skip, & Jump: Practical On-Stack Replacement for a Cross-Platform Language-Neutral VM. - Kunshan Wang; Stephen M. Blackburn; Antony L. Hosking; Michael Norrish (VEE, 2018)

Verified Certificate Checking for Counting Votes. - Milad K. Ghale; Dirk Pattinson; Ramana Kumar; Michael Norrish (VSTTE, 2018)

Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (CoRR, 2018)

Formally Verified Algorithms for Upper-Bounding State Space Diameters. - Mohammad Abdulaziz; Michael Norrish; Charles Gretton (J. Autom. Reason., 2018)

Modular synthesis of verified verifiers of computation with STV algorithms. - Milad K. Ghale; Dirk Pattinson; Michael Norrish (FormaliSE@ICSE, 2019)

A Verified Compositional Algorithm for AI Planning. - Mohammad Abdulaziz; Charles Gretton; Michael Norrish (ITP, 2019)

Designing a low-level virtual machine for implementing real-time managed languages. - Javad Ebrahimian Amiri; Stephen M. Blackburn; Antony L. Hosking; Michael Norrish (VMIL@SPLASH, 2019)

Verified compilation on a verified processor. - Andreas Lööw; Ramana Kumar; Yong Kiam Tan; Magnus O. Myreen; Michael Norrish; Oskar Abrahamsson; Anthony C. J. Fox (PLDI, 2019)

MoonLight: Effective Fuzzing with Near-Optimal Corpus Distillation. - Liam Hayes; Hendra Gunadi; Adrian Herrera; Jonathon Milford; Shane Magrath; Maggi Sebastian; Michael Norrish; Antony L. Hosking (CoRR, 2019)

Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. - Steve Bishop; Matthew Fairbairn; Hannes Mehnert; Michael Norrish; Tom Ridge; Peter Sewell; Michael Smith 008; Keith Wansbrough (J. ACM, 2019)

Proof Pearl: Bounding Least Common Multiples with Triangles. - Hing-Lun Chan; Michael Norrish (J. Autom. Reason., 2019)

Classification of Finite Fields with Applications. - Hing-Lun Chan; Michael Norrish (J. Autom. Reason., 2019)

The verified CakeML compiler backend. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (J. Funct. Program., 2019)

Mechanised Modal Model Theory. - Yiming Xu; Michael Norrish (IJCAR (1), 2020)

Proof-Producing Synthesis of CakeML from Monadic HOL Functions. - Oskar Abrahamsson; Son Ho; Hrutvik Kanabar; Ramana Kumar; Magnus O. Myreen; Michael Norrish; Yong Kiam Tan (J. Autom. Reason., 2020)

On the formalisation of Kolmogorov complexity. - Elliot Catt; Michael Norrish (CPP, 2021)

Seed selection for successful fuzzing. - Adrian Herrera; Hendra Gunadi; Shane Magrath; Michael Norrish; Mathias Payer; Antony L. Hosking (ISSTA, 2021)

TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. - Minchao Wu; Michael Norrish; Christian Walder; Amir Dezfouli (NeurIPS, 2021)

Mechanisation of the AKS Algorithm. - Hing-Lun Chan; Michael Norrish (J. Autom. Reason., 2021)

TacticToe: Learning to Prove with Tactics. - Thibault Gauthier; Cezary Kaliszyk; Josef Urban; Ramana Kumar; Michael Norrish (J. Autom. Reason., 2021)

Kalas: A Verified, End-To-End Compiler for a Choreographic Language. - Johannes Åman Pohjola; Alejandro Gómez-Londoño; James Shaker; Michael Norrish (ITP, 2022)

Mechanizing Soundness of Off-Policy Evaluation. - Jared Yeager; J. Eliot B. Moss; Michael Norrish; Philip S. Thomas (ITP, 2022)

Dependently Sorted Theorem Proving for Mathematical Foundations. - Yiming Xu; Michael Norrish (ITP, 2023)

Pancake: Verified Systems Programming Made Sweeter. - Johannes Åman Pohjola; Hira Taqdees Syeda; Miki Tanaka; Krishnan Winter; Tsun Wang Sau; Benjamin Nott; Tiana J. Tsang Ung; Craig McLaughlin; Remy Seassau; Magnus O. Myreen; Michael Norrish; Gernot Heiser (PLOS@SOSP, 2023)

PureCake: A Verified Compiler for a Lazy Functional Language. - Hrutvik Kanabar; Samuel Vivien; Oskar Abrahamsson; Magnus O. Myreen; Michael Norrish; Johannes Åman Pohjola; Riccardo Zanetti (Proc. ACM Program. Lang., 2023)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. - Sean Lamont; Michael Norrish; Amir Dezfouli; Christian Walder; Paul Montague (AAAI, 2024)

Reproducibility Debt: Challenges and Future Pathways. - Zara Hassan; Christoph Treude; Michael Norrish; Graham J. Williams; Alex Potanin (SIGSOFT FSE Companion, 2024)

AutoCorres2. - Matthew Brecknell; David Greenaway; Johannes Hölzl; Fabian Immler; Gerwin Klein; Rafal Kolanski; Japheth Lim; Michael Norrish; Norbert Schirmer; Salomon Sickert; Thomas Sewell; Harvey Tuch; et al. (Arch. Formal Proofs, 2024)

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes. - Sean Lamont; Christian Walder; Amir Dezfouli; Paul Montague; Michael Norrish (CoRR, 2024)

Characterising reproducibility debt in scientific software: A systematic literature review. - Zara Hassan; Christoph Treude; Michael Norrish; Graham J. Williams; Alex Potanin (J. Syst. Softw., 2025)

Verifying Device Drivers with Pancake. - Junming Zhao; Alessandro Legnani; Tiana J. Tsang Ung; H. Truong; Tsun Wang Sau; Miki Tanaka; Johannes Åman Pohjola; Thomas Sewell; Robert Sison; Syeda Hira; Magnus Myreen; Michael Norrish; et al. (CoRR, 2025)

Fast, Verified Computation for HOL ITPs. - Oskar Abrahamsson; Magnus O. Myreen; Michael Norrish; Hrutvik Kanabar; Johannes Åman Pohjola (J. Autom. Reason., 2025)