

Aditi Barthwal and Michael Norrish
A mechanisation of some contextfree language theory in HOL4
Journal of Computer and System Sciences, Volume 80, Number 2, pp. 346–362, March, 2014 


Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens
CakeML: A verified implementation of ML
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014 


Joseph Chan and Michael Norrish
A string of pearls: Proofs of fermat's little theorem
Journal of Formal Reasoning, Volume 6, Number 1, pp. 63–87, December, 2013 


Andreas Bauer, Peter Baumgartner, Diller Martin and Michael Norrish
Tableaux for verification of datacentric processes
Automated Reasoning with Analytic Tableaux and Related Methods, pp. 28–43, Nancy, France, September, 2013 


Michael Norrish and Brian Huffman
Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$
International Conference on Interactive Theorem Proving, pp. 133–146, Rennes, France, July, 2013 


HingLun Chan and Michael Norrish
A string of pearls: Proofs of fermat’s little theorem
International Conference on Certified Programs and Proofs, pp. 188–207, Kyoto, Japan, October, 2012 


Michael Norrish
Mechanised computability theory
International Conference on Interactive Theorem Proving, pp. 297—311, Nijmegen, The Netherlands, August, 2011 


Aditi Barthwal and Michael Norrish
A formalisation of the normal forms of contextfree grammars in HOL4
19th EACSL Annual Conferences on Computer Science Logic, pp. 95–109, Brno, Czech Republic, August, 2010 


Ramana Kumar and Michael Norrish
(nominal) unification by recursive descent with triangular substitutions
International Conference on Interactive Theorem Proving, pp. 51–66, Edinburgh, United Kingdom, July, 2010 


Konrad Slind and Michael Norrish
A brief overview of HOL4
International Conference on Theorem Proving in Higher Order Logics, pp. 28–32, Montréal, Canada, August, 2008 


Tom Ridge, Michael Norrish and Peter Sewell
A rigorous approach to networking: TCP, from implementation to protocol to service
International Symposium on Formal Methods (FM), pp. 294—309, Turku, Finland, May, 2008 


Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough
Engineering with logic: HOL specification and symbolicevaluation testing for TCP implementations
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pp. 55—66, Charleston, South Carolina, USA, January, 2006 


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
ACM Conference on Communications, pp. 265–276, Philadelphia, August, 2005 


Michael Norrish
Complete integer decision procedures as derived rules in HOL
International Conference on Theorem Proving in Higher Order Logics, pp. 71–86, Rome, September, 2003 