All papers appearing in LNCS (Lecture Notes in Computer Science) are copyright Springer-Verlag, and appear here with their permission.

• Michael Norrish. Mechanised Computability Theory. Proceedings of ITP, Nijmegen, 2011. LNCS 6898, pp297–311. (BibTeX)

  (The published version of this paper contains a minor error, which this version of the paper corrects.  The error is that one of the rules specifying normal order reduction was left out.)

• James Cheney, Michael Norrish and René Vestergaard. Formalizing adequacy: a case study for higher-order abstract syntax. Journal of Automated Reasoning. Available online at SpringerLink; still to appear in print.

• Aditi Barthwal and Michael Norrish. A Formalisation of the Normal Forms of Context-Free Grammars in HOL4. Proceedings of CSL, Brno, Czech Republic, 2010. LNCS 6247, pp95–109. (BibTeX)
• Aditi Barthwal and Michael Norrish. Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. Proceedings of WoLLiC, Brasilia, 2010. LNCS 6188, pp125–135. (BibTeX)
• Ramana Kumar and Michael Norrish. (Nominal) Unification by Recursive Descent with Triangular Substitutions. Proceedings of ITP, Edinburgh, 2010. LNCS 6172, pp51–66. (BibTeX) (Slides)
• Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood. seL4: Formal Verification of an Operating-System Kernel. Communications of the ACM, 53(6):107–115, June 2010. (BibTeX)
• Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood. seL4: Formal Verification of an OS Kernel. Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009. [This paper won a Best Paper prize.] (BibTeX)
• Michael Norrish. Rewriting Conversions Implemented with Continuations. Journal of Automated Reasoning, 43(3):305–336, 2009. (BibTeX).
• Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish. Mind the Gap: A Verification Framework for Low-Level C. Proceedings of TPHOLs, Munich, 2009. LNCS 5674, pp500–515. (BibTeX)
• Aditi Barthwal and Michael Norrish. Verified, Executable Parsing. Proceedings of ESOP, York, 2009. LNCS 5502, pp160–174. (BibTeX)
• Michael Norrish. A Formal Semantics for C++. NICTA Technical Report, 2008. (BibTeX)
• Konrad Slind and Michael Norrish. A Brief Overview of HOL4. Proceedings of TPHOLs, Montréal, 2008. LNCS 5170, pp28–32. (BibTeX)
• Tom Ridge, Michael Norrish and Peter Sewell. A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. 15th International Symposium on Formal Methods: 2008 Proceedings, Turku, 2008. LNCS 5014, pp294–309. (BibTeX) (Slides)
• Michael Norrish and René Vestergaard. Proof Pearl: de Bruijn Terms Really Do Work. Proceedings of TPHOLs, Kaiserslautern, 2007. LNCS 4732, pp207–222. (BibTeX) (Slides)
• Christian Urban, Stefan Berghofer and Michael Norrish. Barendregt’s Variable Convention in Rule Inductions. Proceedings of CADE, Bremen, 2007. LNCS 4603, pp35–50. (BibTeX)
• Harvey Tuch, Gerwin Klein and Michael Norrish.Types, Bytes and Separation Logic. Proceedings of POPL, Nice, 2007. pp97–108. (BibTeX) 
• Michael Norrish. Mechanising λ-calculus using a Classical First Order Theory of Terms with Permutations. Higher Order and Symbolic Computation, 19:169–195, 2006. (BibTeX)

  (Note: In Section 3.3 Other approaches, this paper misrepresents Homeier’s approach as being unable to do rule inductions satisfactorily. This is incorrect: he proves and uses “height-based” rule induction principles that give the same sort of ease-of-use as his height-based structural principles.) 

• Michael Norrish and René Vestergaard. Structural Preservation and Reflection of Diagrams. NICTA Technical Report PA006140, 2006. (Also available as JAIST Technical Report IS-RR-2006-011.) (BibTeX)
• Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough. Engineering with Logic: HOL Specification and Symbolic-evaluation Testing for TCP Implementations. Proceedings of POPL, Charleston, 2006. pp55–66. (BibTeX)
• Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough. Rigorous Specification and Conformance Testing Techniques for Network Protocols, as applied to TCP, UDP, and Sockets. Proceedings of SIGCOMM, Philadelphia, 2005. pp265–276. (BibTeX)
• Michael Norrish and Konrad Slind. Proof pearl: using combinators to manipulate let-expressions in proof. Proceedings of TPHOLs, Oxford, 2005. LNCS 3603, pp397–408. (BibTeX) (Slides)
• Michael Norrish. Recursive Function Definition for Types with Binders. Proceedings of TPHOLs, Park City, 2004. LNCS 3223, pp241–256. (BibTeX)
• Michael Norrish. Complete Integer Decision Procedures as Derived Rules in HOL. Proceedings of TPHOLs, Rome, 2003. LNCS 2758, pp71–86. (BibTeX) (Slides)

• Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, M. J. C. Gordon and T. Melham. The PROSPER Toolkit. International Journal on Software Tools for Technology Transfer, 4(2):189–210, 2003. (BibTeX)

• Michael Norrish and Konrad Slind. A Thread of HOL Development. Computer Journal, 45(1):37–45, 2002. (BibTeX)

• Keith Wansbrough, Michael Norrish, Peter Sewell and Andrei Serjantov, Timing UDP: Mechanized Semantics for Sockets, Threads and Failures. Proceedings of the 11th European Symposium on Programming,Grenoble, 2002.  LNCS 2305, pp278–294. (BibTeX)

• Louise A. Dennis, Graham Collins, Michael Norrish, Richard Boulton, Konrad Slind, Graham Robinson, M. J. C. Gordon and T. Melham. The PROSPER Toolkit. Proceedings of TACAS, Berlin, 2000. LNCS 1785, pp78–92. (BibTeX) [This paper won a Best Paper prize.]

• Michael Norrish. Deterministic Expressions in C. Proceedings of ESOP, Amsterdam, 1999. LNCS 1576, pp147–161. (BibTeX) [This paper won a Best Paper prize.]