Michael Norrish
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
43
Venues
21
Active years
1999–2025
Best venue rank
A*
Where they publish
Papers
43 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | ITP | Mechanising Bhm Trees and λη-Completeness. | Chun Tian, Michael Norrish |
| 2024 | AAAI | BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. | Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague |
| 2023 | ITP | Dependently Sorted Theorem Proving for Mathematical Foundations. | Yiming Xu, Michael Norrish |
| 2023 | PLOS | 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 |
| 2022 | ITP | Kalas: A Verified, End-To-End Compiler for a Choreographic Language. | Johannes man Pohjola, Alejandro Gmez-Londoo, James Shaker, Michael Norrish |
| 2022 | ITP | Mechanizing Soundness of Off-Policy Evaluation. | Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas |
| 2021 | CPP | On the formalisation of Kolmogorov complexity. | Elliot Catt, Michael Norrish |
| 2021 | ISSTA | Seed selection for successful fuzzing. | Adrian Herrera, Hendra Gunadi, Shane Magrath, Michael Norrish, Mathias Payer, Antony L. Hosking |
| 2020 | CADE | Mechanised Modal Model Theory. | Yiming Xu, Michael Norrish |
| 2019 | ICSE | Modular synthesis of verified verifiers of computation with STV algorithms. | Milad K. Ghale, Dirk Pattinson, Michael Norrish |
| 2019 | ITP | A Verified Compositional Algorithm for AI Planning. | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
| 2019 | OOPSLA | Designing a low-level virtual machine for implementing real-time managed languages. | Javad Ebrahimian Amiri, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish |
| 2019 | PLDI | Verified compilation on a verified processor. | Andreas Lw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox |
| 2018 | CADE | 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 |
| 2018 | ITP | Verifying the LTL to Bchi Automata Translation via Very Weak Alternating Automata. | Simon Jantsch, Michael Norrish |
| 2018 | VEE | Hop, Skip, & Jump: Practical On-Stack Replacement for a Cross-Platform Language-Neutral VM. | Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish |
| 2017 | ESOP | Verified Characteristic Formulae for CakeML. | Armal Guneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish |
| 2016 | ICFP | A new verified compiler backend for CakeML. | Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish |
| 2016 | ITP | Proof Pearl: Bounding Least Common Multiples with Triangles. | Hing-Lun Chan, Michael Norrish |
| 2015 | IJCAI | Exploiting Symmetries by Planning for a Descriptive Quotient. | Mohammad Abdulaziz, Michael Norrish, Charles Gretton |
| 2015 | ITP | Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. | Mohammad Abdulaziz, Charles Gretton, Michael Norrish |
| 2015 | ITP | Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. | Hing-Lun Chan, Michael Norrish |
| 2014 | CADE | Beagle as a HOL4 external ATP method. | Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish |
| 2014 | POPL | CakeML: a verified implementation of ML. | Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens |
| 2013 | ITP | Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. | Michael Norrish, Brian Huffman |
| 2013 | TABLEAUX | Tableaux for Verification of Data-Centric Processes. | Andreas Bauer, Peter Baumgartner, Martin Diller, Michael Norrish |
| 2012 | CPP | A String of Pearls: Proofs of Fermat's Little Theorem. | Hing-Lun Chan, Michael Norrish |
| 2011 | ITP | Mechanised Computability Theory. | Michael Norrish |
| 2010 | CSL | A Formalisation of the Normal Forms of Context-Free Grammars in HOL4. | Aditi Barthwal, Michael Norrish |
| 2010 | ITP | (Nominal) Unification by Recursive Descent with Triangular Substitutions. | Ramana Kumar, Michael Norrish |
| 2010 | WoLLIC | Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. | Aditi Barthwal, Michael Norrish |
| 2009 | ESOP | Verified, Executable Parsing. | Aditi Barthwal, Michael Norrish |
| 2009 | SOSP | 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, Simon Winwood |
| 2008 | FM | A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. | Tom Ridge, Michael Norrish, Peter Sewell |
| 2007 | CADE | Barendregt's Variable Convention in Rule Inductions. | Christian Urban, Stefan Berghofer, Michael Norrish |
| 2007 | POPL | Types, bytes, and separation logic. | Harvey Tuch, Gerwin Klein, Michael Norrish |
| 2006 | POPL | Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. | Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough |
| 2005 | ICFP | A formal treatment of the barendregt variable convention in rule inductions. | Christian Urban, Michael Norrish |
| 2005 | SIGCOMM | 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, Keith Wansbrough |
| 2003 | ICFP | Mechanising Hankin and Barendregt using the Gordon-Melham axioms. | Michael Norrish |
| 2002 | ESOP | Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. | Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov |
| 2000 | TACAS | The PROSPER Toolkit. | Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham |
| 1999 | ESOP | Deterministic Expressions in C. | Michael Norrish |