• Publications
• Teaching Material

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

• 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)
• 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)
• Michael Norrish. Deterministic Expressions in C. Proceedings of ESOP, Amsterdam, 1999. LNCS 1576, pp147–161. (BibTeX)