Michael Norrish

Publication Activity (10 Years)

Years Active: 1999-2024
Publications (10 Years): 38

Top Topics

Kolmogorov Complexity

Policy Evaluation

Virtual Machine

Top Venues

J. Autom. Reason.

Proc. ACM Program. Lang.

Publications

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, Simon Wimmer
AutoCorres2. Arch. Formal Proofs 2024 (2024)
Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. AAAI (2024)
Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. CoRR (2024)
Zara Hassan, Christoph Treude, Michael Norrish, Graham Williams, Alex Potanin
Reproducibility Debt: Challenges and Future Pathways. SIGSOFT FSE Companion (2024)
Yiming Xu, Michael Norrish
Dependently Sorted Theorem Proving for Mathematical Foundations. ITP (2023)
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
Pancake: Verified Systems Programming Made Sweeter. PLOS@SOSP (2023)
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti
PureCake: A Verified Compiler for a Lazy Functional Language. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, Michael Norrish
Kalas: A Verified, End-To-End Compiler for a Choreographic Language. ITP (2022)
Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas
Mechanizing Soundness of Off-Policy Evaluation. ITP (2022)
Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. CoRR (2021)
Elliot Catt, Michael Norrish
On the formalisation of Kolmogorov complexity. CPP (2021)
Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. NeurIPS (2021)
Hing-Lun Chan, Michael Norrish
Mechanisation of the AKS Algorithm. J. Autom. Reason. 65 (2) (2021)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65 (2) (2021)
Adrian Herrera, Hendra Gunadi, Shane Magrath, Michael Norrish, Mathias Payer, Antony L. Hosking
Seed selection for successful fuzzing. ISSTA (2021)
Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, Yong Kiam Tan
Proof-Producing Synthesis of CakeML from Monadic HOL Functions. J. Autom. Reason. 64 (7) (2020)
Yiming Xu, Michael Norrish
Mechanised Modal Model Theory. IJCAR (1) (2020)
Hing-Lun Chan, Michael Norrish
Proof Pearl: Bounding Least Common Multiples with Triangles. J. Autom. Reason. 62 (2) (2019)
Javad Ebrahimian Amiri, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish
Designing a low-level virtual machine for implementing real-time managed languages. VMIL@SPLASH (2019)
Hing-Lun Chan, Michael Norrish
Classification of Finite Fields with Applications. J. Autom. Reason. 63 (3) (2019)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
The verified CakeML compiler backend. J. Funct. Program. 29 (2019)
Liam Hayes, Hendra Gunadi, Adrian Herrera, Jonathon Milford, Shane Magrath, Maggi Sebastian, Michael Norrish, Antony L. Hosking
MoonLight: Effective Fuzzing with Near-Optimal Corpus Distillation. CoRR (2019)
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox
Verified compilation on a verified processor. PLDI (2019)
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough
Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. J. ACM 66 (1) (2019)
Mohammad Abdulaziz, Charles Gretton, Michael Norrish
A Verified Compositional Algorithm for AI Planning. ITP (2019)
Milad K. Ghale, Dirk Pattinson, Michael Norrish
Modular synthesis of verified verifiers of computation with STV algorithms. FormaliSE@ICSE (2019)
Mohammad Abdulaziz, Michael Norrish, Charles Gretton
Formally Verified Algorithms for Upper-Bounding State Space Diameters. J. Autom. Reason. 61 (1-4) (2018)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
Learning to Prove with Tactics. CoRR (2018)
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. IJCAR (2018)
Simon Jantsch, Michael Norrish
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. ITP (2018)
Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish
Verified Certificate Checking for Counting Votes. VSTTE (2018)
Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish
Hop, Skip, & Jump: Practical On-Stack Replacement for a Cross-Platform Language-Neutral VM. VEE (2018)
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish
Verified Characteristic Formulae for CakeML. ESOP (2017)
Mohammad Abdulaziz, Charles Gretton, Michael Norrish
A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds. ICAPS (2017)
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan
Verifying efficient function calls in CakeML. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
A new verified compiler backend for CakeML. ICFP (2016)
Hing-Lun Chan, Michael Norrish
Proof Pearl: Bounding Least Common Multiples with Triangles. ITP (2016)
Yi Lin, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish
Rust as a language for high performance GC implementation. ISMM (2016)
Hing-Lun Chan, Michael Norrish
Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. ITP (2015)
Mohammad Abdulaziz, Charles Gretton, Michael Norrish
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. ITP (2015)
Kunshan Wang, Yi Lin, Stephen M. Blackburn, Michael Norrish, Antony L. Hosking
Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development. SNAPL (2015)
Mohammad Abdulaziz, Michael Norrish, Charles Gretton
Exploiting Symmetries by Planning for a Descriptive Quotient. IJCAI (2015)
Yi Lin, Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish
Stop and go: understanding yieldpoint behavior. ISMM (2015)
Michael Norrish, Michelle Mills Strout
An Approach for Proving the Correctness of Inspector/Executor Transformations. LCPC (2014)
Aditi Barthwal, Michael Norrish
A mechanisation of some context-free language theory in HOL4. J. Comput. Syst. Sci. 80 (2) (2014)
Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens
CakeML: a verified implementation of ML. POPL (2014)
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish
Beagle as a HOL4 external ATP method. PAAR@IJCAR (2014)
Michael Norrish, Brian Huffman
Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. ITP (2013)
Andreas Bauer, Peter Baumgartner, Martin Diller, Michael Norrish
Tableaux for Verification of Data-Centric Processes. TABLEAUX (2013)
Hing-Lun Chan, Michael Norrish
A String of Pearls: Proofs of Fermat's Little Theorem. J. Formaliz. Reason. 6 (1) (2013)
Andreas Klaus Bauer, Peter Baumgartner, Michael Norrish
Reasoning with Data-Centric Business Processes CoRR (2012)
James Cheney, Michael Norrish, René Vestergaard
Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax. J. Autom. Reason. 49 (2) (2012)
Hing-Lun Chan, Michael Norrish
A String of Pearls: Proofs of Fermat's Little Theorem. CPP (2012)
Michael Norrish
Mechanised Computability Theory. ITP (2011)
Aditi Barthwal, Michael Norrish
A Formalisation of the Normal Forms of Context-Free Grammars in HOL4. CSL (2010)
Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
seL4: formal verification of an operating-system kernel. Commun. ACM 53 (6) (2010)
Aditi Barthwal, Michael Norrish
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. WoLLIC (2010)
Ramana Kumar, Michael Norrish
(Nominal) Unification by Recursive Descent with Triangular Substitutions. ITP (2010)
Michael Norrish
Rewriting Conversions Implemented with Continuations. J. Autom. Reason. 43 (3) (2009)
Aditi Barthwal, Michael Norrish
Verified, Executable Parsing. ESOP (2009)
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish
Mind the Gap. TPHOLs (2009)
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood
seL4: formal verification of an OS kernel. SOSP (2009)
Konrad Slind, Michael Norrish
A Brief Overview of HOL4. TPHOLs (2008)
Tom Ridge, Michael Norrish, Peter Sewell
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. FM (2008)
Christian Urban, Stefan Berghofer, Michael Norrish
Barendregt's Variable Convention in Rule Inductions. CADE (2007)
Michael Norrish, René Vestergaard
Proof Pearl: De Bruijn Terms Really Do Work. TPHOLs (2007)
Harvey Tuch, Gerwin Klein, Michael Norrish
Types, bytes, and separation logic. POPL (2007)
Michael Norrish
Mechanising lambda-calculus using a classical first order theory of terms with permutations. High. Order Symb. Comput. 19 (2-3) (2006)
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. POPL (2006)
Christian Urban, Michael Norrish
A formal treatment of the barendregt variable convention in rule inductions. MERLIN (2005)
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets. SIGCOMM (2005)
Michael Norrish, Konrad Slind
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. TPHOLs (2005)
Michael Norrish
Recursive Function Definition for Types with Binders. TPHOLs (2004)
Michael Norrish
Mechanising Hankin and Barendregt using the Gordon-Melham axioms. MERLIN (2003)
Michael Norrish
Complete Integer Decision Procedures as Derived Rules in HOL. TPHOLs (2003)
Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham
The PROSPER toolkit. Int. J. Softw. Tools Technol. Transf. 4 (2) (2003)
Michael Norrish, Konrad Slind
A Thread of HOL Development. Comput. J. 45 (1) (2002)
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. ESOP (2002)
Michael Norrish, Peter Sewell, Keith Wansbrough
feasible: reflections on formal treatments of C and UDP sockets. ACM SIGOPS European Workshop (2002)
Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham
The PROSPER Toolkit. TACAS (2000)
Michael Norrish
Deterministic Expressions in C. ESOP (1999)