default search action

combined dblp search
author search
venue search
publication search

ask others

Michael Norrish

Name: dblp XML data dump
Creator: Schloss Dagstuhl - Leibniz Center for Informatics
Published: 1993
License: https://creativecommons.org/publicdomain/zero/1.0/
Keywords: dblp, XML, computer science, scholarly publications, metadata

◀ ▶ joint publications with coauthor community group 1

> Home > Persons > Michael Norrish

Publications

2025
[j21]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/AbrahamssonMNKP25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/AbrahamssonMNKP25
Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Hrutvik Kanabar, Johannes Åman Pohjola:
Fast, Verified Computation for HOL ITPs. J. Autom. Reason. 69(1): 7 (2025)
[j20]
- view
  authority control:
- export record
  dblp key:
  - journals/jss/HassanTNWP25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jss/HassanTNWP25
Zara Hassan, Christoph Treude, Michael Norrish, Graham J. Williams, Alex Potanin:
Characterising reproducibility debt in scientific software: A systematic literature review. J. Syst. Softw. 222: 112327 (2025)
[i7]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2501-08249
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2501-08249
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:
Verifying Device Drivers with Pancake. CoRR abs/2501.08249 (2025)
2024
[j19]
- view
  - electronic edition @ isa-afp.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/afp/BrecknellGHIKKLNSSSTW24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/afp/BrecknellGHIKKLNSSSTW24
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)
[c56]
- view
  authority control:
- export record
  dblp key:
  - conf/sigsoft/HassanTNWP24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigsoft/HassanTNWP24
Zara Hassan, Christoph Treude, Michael Norrish, Graham J. Williams, Alex Potanin:
Reproducibility Debt: Challenges and Future Pathways. SIGSOFT FSE Companion 2024: 462-466
2023
[j18]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/KanabarVAMNPZ23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/KanabarVAMNPZ23
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)
[c54]
- view
  authority control:
- export record
  dblp key:
  - conf/plos/PohjolaSTWSNUMS23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/plos/PohjolaSTWSNUMS23
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]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/itp/PohjolaGSN22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/PohjolaGSN22
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]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/itp/YeagerMNT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/YeagerMNT22
Jared Yeager, J. Eliot B. Moss, Michael Norrish, Philip S. Thomas:
Mechanizing Soundness of Off-Policy Evaluation. ITP 2022: 32:1-32:20
2021
[j16]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/GauthierKUKN21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/GauthierKUKN21
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]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CattN21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CattN21
Elliot Catt, Michael Norrish:
On the formalisation of Kolmogorov complexity. CPP 2021: 291-299
[c50]
- view
  authority control:
- export record
  dblp key:
  - conf/issta/HerreraGMNPH21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/issta/HerreraGMNPH21
Adrian Herrera, Hendra Gunadi, Shane Magrath, Michael Norrish, Mathias Payer, Antony L. Hosking:
Seed selection for successful fuzzing. ISSTA 2021: 230-243
2020
[j15]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jar/AbrahamssonHKKM20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/AbrahamssonHKKM20
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)
2019
[j14]
- view
  authority control:
- export record
  dblp key:
  - journals/jacm/BishopFMNRSSW19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jacm/BishopFMNRSSW19
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)
[j11]
- view
  authority control:
- export record
  dblp key:
  - journals/jfp/TanMKFON19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfp/TanMKFON19
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]
- view
  authority control:
- export record
  dblp key:
  - conf/icse/GhalePN19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icse/GhalePN19
Milad K. Ghale, Dirk Pattinson, Michael Norrish:
Modular synthesis of verified verifiers of computation with STV algorithms. FormaliSE@ICSE 2019: 85-94
[c45]
- view
  authority control:
- export record
  dblp key:
  - conf/oopsla/AmiriBHN19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/oopsla/AmiriBHN19
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]
- view
  authority control:
- export record
  dblp key:
  - conf/pldi/LoowKTMNAF19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pldi/LoowKTMNAF19
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]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1905-13055
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1905-13055
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
[c43]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/HoAKMTN18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/HoAKMTN18
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
[c41]
- view
  authority control:
- export record
  dblp key:
  - conf/vee/WangBHN18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vee/WangBHN18
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]
- view
  authority control:
- export record
  dblp key:
  - conf/vstte/GhalePKN18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vstte/GhalePKN18
Milad K. Ghale, Dirk Pattinson, Ramana Kumar, Michael Norrish:
Verified Certificate Checking for Counting Votes. VSTTE 2018: 69-87
[i2]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1804-00596
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1804-00596
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
Learning to Prove with Tactics. CoRR abs/1804.00596 (2018)
2017
[j9]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/OwensNKMT17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/OwensNKMT17
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)
[c38]
- view
  authority control:
- export record
  dblp key:
  - conf/esop/GueneauMKN17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/GueneauMKN17
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish:
Verified Characteristic Formulae for CakeML. ESOP 2017: 584-610
2016
[c37]
- view
  authority control:
- export record
  dblp key:
  - conf/icfp/TanMKFON16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icfp/TanMKFON16
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
[c35]
- view
  authority control:
- export record
  dblp key:
  - conf/iwmm/LinBHN16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/iwmm/LinBHN16
Yi Lin, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish:
Rust as a language for high performance GC implementation. ISMM 2016: 89-98
2015
[c31]
- view
  authority control:
- export record
  dblp key:
  - conf/iwmm/LinWBHN15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/iwmm/LinWBHN15
Yi Lin, Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish:
Stop and go: understanding yieldpoint behavior. ISMM 2015: 70-80
[c30]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/snapl/WangLBNH15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/snapl/WangLBNH15
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
[c29]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/GauthierKKN14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/GauthierKKN14
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish:
Beagle as a HOL4 external ATP method. PAAR@IJCAR 2014: 50-59
[c27]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/KumarMNO14
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/KumarMNO14
Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens:
CakeML: a verified implementation of ML. POPL 2014: 179-192
2013
[c26]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/NorrishH13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/NorrishH13
Michael Norrish, Brian Huffman:
Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. ITP 2013: 133-146
[c25]
- view
  authority control:
- export record
  dblp key:
  - conf/tableaux/0002BDN13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tableaux/0002BDN13
Andreas Bauer, Peter Baumgartner, Martin Diller, Michael Norrish:
Tableaux for Verification of Data-Centric Processes. TABLEAUX 2013: 28-43
2012
[j6]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/CheneyNV12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/CheneyNV12
James Cheney, Michael Norrish, René Vestergaard:
Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax. J. Autom. Reason. 49(2): 209-239 (2012)
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1207-2461
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1207-2461
Andreas Klaus Bauer, Peter Baumgartner, Michael Norrish:
Reasoning with Data-Centric Business Processes. CoRR abs/1207.2461 (2012)
2010
[j5]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/KleinAEHCDEEKNSTW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/KleinAEHCDEEKNSTW10
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)
[c21]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/KumarN10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KumarN10
Ramana Kumar, Michael Norrish:
(Nominal) Unification by Recursive Descent with Triangular Substitutions. ITP 2010: 51-66
2009
[c18]
- view
  authority control:
- export record
  dblp key:
  - conf/sosp/KleinEHACDEEKNSTW09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sosp/KleinEHACDEEKNSTW09
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]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/WinwoodKSACN09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/WinwoodKSACN09
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish:
Mind the Gap. TPHOLs 2009: 500-515
2008
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/fm/RidgeNS08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/RidgeNS08
Tom Ridge, Michael Norrish, Peter Sewell:
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. FM 2008: 294-309
[c15]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/SlindN08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/SlindN08
Konrad Slind, Michael Norrish:
A Brief Overview of HOL4. TPHOLs 2008: 28-32
2007
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/UrbanBN07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/UrbanBN07
Christian Urban, Stefan Berghofer, Michael Norrish:
Barendregt's Variable Convention in Rule Inductions. CADE 2007: 35-50
[c13]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/TuchKN07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/TuchKN07
Harvey Tuch, Gerwin Klein, Michael Norrish:
Types, bytes, and separation logic. POPL 2007: 97-108
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/NorrishV07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/NorrishV07
Michael Norrish, René Vestergaard:
Proof Pearl: De Bruijn Terms Really Do Work. TPHOLs 2007: 207-222
2006
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/BishopFNSSW06
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/BishopFNSSW06
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]
- view
  authority control:
- export record
  dblp key:
  - conf/icfp/UrbanN05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icfp/UrbanN05
Christian Urban, Michael Norrish:
A formal treatment of the barendregt variable convention in rule inductions. MERLIN 2005: 25-32
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/sigcomm/BishopFNSSW05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigcomm/BishopFNSSW05
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]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/NorrishS05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/NorrishS05
Michael Norrish, Konrad Slind:
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. TPHOLs 2005: 397-408
2003
[j2]
- view
  authority control:
- export record
  dblp key:
  - journals/sttt/DennisCNBSM03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/sttt/DennisCNBSM03
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)
2002
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/cj/NorrishS02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cj/NorrishS02
Michael Norrish, Konrad Slind:
A Thread of HOL Development. Comput. J. 45(1): 37-45 (2002)
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/esop/WansbroughNSS02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/esop/WansbroughNSS02
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov:
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. ESOP 2002: 278-294
[c3]
- view
  authority control:
- export record
  dblp key:
  - conf/sigopsE/NorrishSW02
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sigopsE/NorrishSW02
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]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/DennisCNBSRGM00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/DennisCNBSRGM00
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

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.