Michael Norrish

90 papers A* 10A 9B 20C 3Journal 29Unranked 18

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