default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMichael Norrish
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j19]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)- [c57]Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague:
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. AAAI 2024: 10607-10615 - [c56]Zara Hassan
, Christoph Treude, Michael Norrish, Graham J. Williams, Alex Potanin:
Reproducibility Debt: Challenges and Future Pathways. SIGSOFT FSE Companion 2024: 462-466 - [e2]Yves Bertot, Temur Kutsia, Michael Norrish:
15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia. LIPIcs 309, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2024, ISBN 978-3-95977-337-9 [contents] - [i5]Sean Lamont, Michael Norrish, Amir Dezfouli, Christian Walder, Paul Montague:
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving. CoRR abs/2403.03401 (2024) - 2023
- [j18]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): 952-976 (2023) - [c55]Yiming Xu, Michael Norrish:
Dependently Sorted Theorem Proving for Mathematical Foundations. ITP 2023: 33:1-33:18 - [c54]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: 1-9 - 2022
- [c53]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: 27:1-27:18 - [c52]Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas:
Mechanizing Soundness of Off-Policy Evaluation. ITP 2022: 32:1-32:20 - 2021
- [j17]Hing-Lun Chan, Michael Norrish:
Mechanisation of the AKS Algorithm. J. Autom. Reason. 65(2): 205-256 (2021) - [j16]Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65(2): 257-286 (2021) - [c51]Elliot Catt, Michael Norrish:
On the formalisation of Kolmogorov complexity. CPP 2021: 291-299 - [c50]Adrian Herrera, Hendra Gunadi, Shane Magrath, Michael Norrish, Mathias Payer, Antony L. Hosking:
Seed selection for successful fuzzing. ISSTA 2021: 230-243 - [c49]Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli:
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. NeurIPS 2021: 9330-9342 - [i4]Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli:
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. CoRR abs/2102.09756 (2021) - 2020
- [j15]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): 1287-1306 (2020) - [c48]Yiming Xu, Michael Norrish:
Mechanised Modal Model Theory. IJCAR (1) 2020: 518-533
2010 – 2019
- 2019
- [j14]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): 1:1-1:77 (2019) - [j13]Hing-Lun Chan, Michael Norrish:
Proof Pearl: Bounding Least Common Multiples with Triangles. J. Autom. Reason. 62(2): 171-192 (2019) - [j12]Hing-Lun Chan, Michael Norrish:
Classification of Finite Fields with Applications. J. Autom. Reason. 63(3): 667-693 (2019) - [j11]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: e2 (2019) - [c47]Milad K. Ghale, Dirk Pattinson, Michael Norrish:
Modular synthesis of verified verifiers of computation with STV algorithms. FormaliSE@ICSE 2019: 85-94 - [c46]Mohammad Abdulaziz, Charles Gretton, Michael Norrish:
A Verified Compositional Algorithm for AI Planning. ITP 2019: 4:1-4:19 - [c45]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: 1-11 - [c44]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: 1041-1053 - [i3]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 abs/1905.13055 (2019) - 2018
- [j10]Mohammad Abdulaziz, Michael Norrish, Charles Gretton:
Formally Verified Algorithms for Upper-Bounding State Space Diameters. J. Autom. Reason. 61(1-4): 485-520 (2018) - [c43]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: 646-662 - [c42]Simon Jantsch, Michael Norrish:
Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata. ITP 2018: 306-323 - [c41]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: 1-16 - [c40]Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish:
Verified Certificate Checking for Counting Votes. VSTTE 2018: 69-87 - [i2]Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
Learning to Prove with Tactics. CoRR abs/1804.00596 (2018) - 2017
- [j9]Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan:
Verifying efficient function calls in CakeML. Proc. ACM Program. Lang. 1(ICFP): 18:1-18:27 (2017) - [c39]Mohammad Abdulaziz, Charles Gretton, Michael Norrish:
A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds. ICAPS 2017: 2-10 - [c38]Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish:
Verified Characteristic Formulae for CakeML. ESOP 2017: 584-610 - 2016
- [c37]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: 60-73 - [c36]Hing-Lun Chan, Michael Norrish:
Proof Pearl: Bounding Least Common Multiples with Triangles. ITP 2016: 140-150 - [c35]Yi Lin, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish:
Rust as a language for high performance GC implementation. ISMM 2016: 89-98 - 2015
- [c34]Mohammad Abdulaziz, Michael Norrish, Charles Gretton:
Exploiting Symmetries by Planning for a Descriptive Quotient. IJCAI 2015: 1479-1486 - [c33]Mohammad Abdulaziz, Charles Gretton, Michael Norrish:
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. ITP 2015: 1-16 - [c32]Hing-Lun Chan, Michael Norrish:
Mechanisation of AKS Algorithm: Part 1 - The Main Theorem. ITP 2015: 117-136 - [c31]Yi Lin, Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish:
Stop and go: understanding yieldpoint behavior. ISMM 2015: 70-80 - [c30]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: 321-336 - 2014
- [j8]Aditi Barthwal, Michael Norrish:
A mechanisation of some context-free language theory in HOL4. J. Comput. Syst. Sci. 80(2): 346-362 (2014) - [c29]Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish:
Beagle as a HOL4 external ATP method. PAAR@IJCAR 2014: 50-59 - [c28]Michael Norrish, Michelle Mills Strout:
An Approach for Proving the Correctness of Inspector/Executor Transformations. LCPC 2014: 131-145 - [c27]Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens:
CakeML: a verified implementation of ML. POPL 2014: 179-192 - 2013
- [j7]Hing-Lun Chan, Michael Norrish:
A String of Pearls: Proofs of Fermat's Little Theorem. J. Formaliz. Reason. 6(1): 63-87 (2013) - [c26]Michael Norrish, Brian Huffman:
Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. ITP 2013: 133-146 - [c25]Andreas Bauer, Peter Baumgartner, Martin Diller, Michael Norrish:
Tableaux for Verification of Data-Centric Processes. TABLEAUX 2013: 28-43 - [e1]Georges Gonthier, Michael Norrish:
Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Lecture Notes in Computer Science 8307, Springer 2013, ISBN 978-3-319-03544-4 [contents] - 2012
- [j6]James Cheney, Michael Norrish, René Vestergaard:
Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax. J. Autom. Reason. 49(2): 209-239 (2012) - [c24]Hing-Lun Chan, Michael Norrish:
A String of Pearls: Proofs of Fermat's Little Theorem. CPP 2012: 188-207 - [i1]Andreas Klaus Bauer, Peter Baumgartner, Michael Norrish:
Reasoning with Data-Centric Business Processes. CoRR abs/1207.2461 (2012) - 2011
- [c23]Michael Norrish:
Mechanised Computability Theory. ITP 2011: 297-311 - 2010
- [j5]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:
seL4: formal verification of an operating-system kernel. Commun. ACM 53(6): 107-115 (2010) - [c22]Aditi Barthwal, Michael Norrish:
A Formalisation of the Normal Forms of Context-Free Grammars in HOL4. CSL 2010: 95-109 - [c21]Ramana Kumar, Michael Norrish:
(Nominal) Unification by Recursive Descent with Triangular Substitutions. ITP 2010: 51-66 - [c20]Aditi Barthwal, Michael Norrish:
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. WoLLIC 2010: 125-135
2000 – 2009
- 2009
- [j4]Michael Norrish:
Rewriting Conversions Implemented with Continuations. J. Autom. Reason. 43(3): 305-336 (2009) - [c19]Aditi Barthwal, Michael Norrish:
Verified, Executable Parsing. ESOP 2009: 160-174 - [c18]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:
seL4: formal verification of an OS kernel. SOSP 2009: 207-220 - [c17]Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish:
Mind the Gap. TPHOLs 2009: 500-515 - 2008
- [c16]Tom Ridge, Michael Norrish, Peter Sewell:
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. FM 2008: 294-309 - [c15]Konrad Slind, Michael Norrish:
A Brief Overview of HOL4. TPHOLs 2008: 28-32 - 2007
- [c14]Christian Urban, Stefan Berghofer, Michael Norrish:
Barendregt's Variable Convention in Rule Inductions. CADE 2007: 35-50 - [c13]Harvey Tuch, Gerwin Klein, Michael Norrish:
Types, bytes, and separation logic. POPL 2007: 97-108 - [c12]Michael Norrish, René Vestergaard:
Proof Pearl: De Bruijn Terms Really Do Work. TPHOLs 2007: 207-222 - 2006
- [j3]Michael Norrish:
Mechanising lambda-calculus using a classical first order theory of terms with permutations. High. Order Symb. Comput. 19(2-3): 169-195 (2006) - [c11]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: 55-66 - 2005
- [c10]Christian Urban, Michael Norrish:
A formal treatment of the barendregt variable convention in rule inductions. MERLIN 2005: 25-32 - [c9]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: 265-276 - [c8]Michael Norrish, Konrad Slind:
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. TPHOLs 2005: 397-408 - 2004
- [c7]Michael Norrish:
Recursive Function Definition for Types with Binders. TPHOLs 2004: 241-256 - 2003
- [j2]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): 189-210 (2003) - [c6]Michael Norrish:
Mechanising Hankin and Barendregt using the Gordon-Melham axioms. MERLIN 2003 - [c5]Michael Norrish:
Complete Integer Decision Procedures as Derived Rules in HOL. TPHOLs 2003: 71-86 - 2002
- [j1]Michael Norrish, Konrad Slind:
A Thread of HOL Development. Comput. J. 45(1): 37-45 (2002) - [c4]Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov:
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. ESOP 2002: 278-294 - [c3]Michael Norrish, Peter Sewell, Keith Wansbrough:
Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets. ACM SIGOPS European Workshop 2002: 49-53 - 2000
- [c2]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: 78-92
1990 – 1999
- 1999
- [b1]Michael Norrish:
C formalised in HOL. University of Cambridge, UK, 1999 - [c1]Michael Norrish:
Deterministic Expressions in C. ESOP 1999: 147-161
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-09 20:33 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
