Michael is interested in the use of mathematics and logic to help in the specification and development of computer hardware and software. He is interested both in working on specific applications projects in this area, and in the development of tools to make all such projects easier to work on.
| Phone: | +61 2 6218 3719 |
|---|---|
| Email: | Michael.Norrish@anu.edu.au |
More contact information is available at the Contact page.
Michael is interested in the use of mathematics and logic to help in the specification and development of computer hardware and software. He is interested both in working on specific applications projects in this area, and in the development of tools to make all such projects easier to work on.
PhD [University of Cambridge, 1999]; BSc(Hons) [Victoria University of Wellington, 1993]; BA, BSc [Victoria University of Wellington, 1992]
Interactive Theorem Proving, Certified Programs and Proofs
PLDI 2015 ITP 2014 CPP 2013 ITP 2013 ESOP 2013 EMSOFT 2012 CAV 2011 CPP 2011 ITP 2011 ITP 2010 TPHOLs 2009 LICS 2008
|
 |
Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens CakeML: A verified implementation of ML ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–191, San Diego, January, 2014 |
|
 |
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 ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97–108, Nice, France, January, 2007 |
|
|
 |
Michael Norrish and Yiming Xu Mechanised modal model theory International Joint Conference on Automated Reasoning, pp. 518-533, Paris, July, 2020 |
|
|
|
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus Myreen, Michael Norrish, Oskar Abrahamsson and Anthony Fox Verified compilation on a verified processor ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1041-1053, Phoenix, Arizona, United States of America, June, 2019 |
|
|
|
Hing-Lun Chan and Michael Norrish Proof pearl: Bounding least common multiples with triangles Journal of Automated Reasoning, Volume 62, Issue 2, pp. 171-192, February, 2019 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish The verified CakeML compiler backend Journal of Functional Programming, Volume 29, February, 2019 |
|
|
|
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith and Keith Wanbrough Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the sockets API Journal of the ACM, Volume 66, Issue 1, January, 2019 |
|
|
|
Milad Ghale, Dirk Pattinson, Ramana Kumar and Michael Norrish Verified certificate checking for counting votes Verified Software. Theories, Tools, and Experiments, pp. 69–87, Oxford, December, 2018 |
|
|
|
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus Myreen, Yong Kiam Tan and Michael Norrish Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions International Joint Conference on Automated Reasoning, pp. 646-662, Oxford, July, 2018 |
|
|
|
Simon Jantsch and Michael Norrish Verifying the LTL to Büchi automata translation via very weak alternating automata International Conference on Interactive Theorem Proving, pp. 306-323, Oxford, July, 2018 |
|
|
|
Kunshan Wang, Stephen Blackburn, Tony Hosking and Michael Norrish Hop, skip, & jump: Practical on-stack replacement for a cross-platform language-neutral VM International Conference on Virtual Execution Environments, pp. 1-16, Williamsburg, VA, March, 2018 |
|
|
|
Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen Verifying efficient function calls in CakeML International Conference on Functional Programming, Oxford, September, 2017 |
|
|
|
Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish Verified characteristic formulae for CakeML European Symposium on Programming, pp. 584–610, Uppsala, Sweden, April, 2017 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish A new verified compiler backend for CakeML International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016 |
|
|
|
Yi Lin, Steve Blackburn, Tony Hosking and Michael Norrish Rust as a language for high performance GC implementation International Symposium on Memory Management, pp. 89–98, Santa Barbara, California, USA, June, 2016 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Verified over-approximation of the diameter of propositionally factored transition systems International Conference on Interactive Theorem Proving, pp. 1–16, Nanjing, China, August, 2015 |
|
|
|
Joseph Chan and Michael Norrish Mechanisation of AKS algorithm: Part 1 — the main theorem International Conference on Interactive Theorem Proving, pp. 117–136, Nanjing, China, August, 2015 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Exploiting symmetries by planning for a descriptive quotient Proceedings of the 24th International Joint Conference on Artificial Intelligence, pp. 1479–1486, Buenos Aires, July, 2015 |
|
|
|
Yi Lin, Stephen M. Blackburn, Kunshan Wang, Tony Hosking and Michael Norrish Stop and go: Understanding yieldpoint behavior International Symposium on Memory Management, pp. 70–80, Portland, OR, USA, June, 2015 |
|
|
|
Michael Norrish and Michelle Mills Strout An approach for proving the correctness of inspector/executor transformations Languages and Compilers for Parallel Computing, pp. 131–145, Hillsboro, Oregon, USA, May, 2015 |
|
|
|
Kunshan Wang, Yi Lin, Stephen M Blackburn, Michael Norrish and Tony Hosking Draining the swamp: Micro virtual machines as a solid foundation for language development SNAPL, pp. 321–336, Asilomar, California, May, 2015 |
|
|
|
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish Beagle as a HOL4 external ATP method Practical Aspects of Automated Reasoning, pp. 50–59, Vienna, July, 2014 |
|
|
|
Mohammad Abdulaziz, Charles Gretton and Michael Norrish Mechanising theoretical upper bounds in planning Workshop on Knowledge Engineering for Planning and Scheduling, Portsmouth, USA, June, 2014 |
|
|
|
Aditi Barthwal and Michael Norrish A mechanisation of some context-free 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 SIGPLAN-SIGACT 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 data-centric 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 |
|
|
|
Hing-Lun 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 |
|
|
|
James Cheney, Michael Norrish and René Vestergaard Formalizing adequacy: A case study for higher-order abstract syntax Journal of Automated Reasoning, Volume 49, Number 2, pp. 209–239, August, 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 context-free grammars in HOL4 19th EACSL Annual Conferences on Computer Science Logic, pp. 95–109, Brno, Czech Republic, August, 2010 |
|
|
|
Aditi Barthwal and Michael Norrish Mechanisation of PDA and grammar equivalence for context-free languages 17th Workshop on Logic, Language, Information and Computation , pp. 125–135, Brasília, Brazil, July, 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 |
|
|
|
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, Volume 53, Number 6, pp. 107–115, June, 2010 Research Highlights paper |
|
|
|
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 ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009 Best Paper Award Hall of Fame Award |
|
|
|
Michael Norrish Rewriting conversions implemented with continuations Journal of Automated Reasoning, Volume 43, Number 3, pp. 305–336, October, 2009 |
|
|
|
Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish Mind the gap: A verification framework for low-level C International Conference on Theorem Proving in Higher Order Logics, pp. 500–515, Munich, Germany, August, 2009 |
|
|
|
Aditi Barthwal and Michael Norrish Verified, executable parsing European Symposium on Programming, pp. 160–174, York, March, 2009 |
|
|
|
James Cheney, René Vestergaard and Michael Norrish Formalizing adequacy 2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming, York, March, 2009 |
|
|
|
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 |
|
|
|
Michael Norrish A formal semantics for c++ Technical Report, NICTA, November, 2007 |
|
|
|
Michael Norrish and René Vestergaard Proof pearl: de bruijn terms really do work International Conference on Theorem Proving in Higher Order Logics, pp. 207–222, Kaiserslautern, September, 2007 |
|
|
|
Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007 |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 97–108, Nice, France, January, 2007 |
|
|
|
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 ACM SIGPLAN-SIGACT 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 Recursive function definition for types with binders International Conference on Theorem Proving in Higher Order Logics, pp. 241—256, Park City, Utah, United States, September, 2004 |
|
|
|
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 |
|
|
|
Joseph Chan and Michael Norrish No title August, |
|
|
|
Yi Lin An efficient implementation of a micro virtual machine PhD Thesis, The Australian National University, March, 2019 |
|
|
|
Kunshan Wang Micro virtual machines: A solid foundation for managed language implementation PhD Thesis, Australian National University, September, 2018 |
|
|
|
Mohammad Abdulaziz Formally verified compositional algorithms for factored transition systems PhD Thesis, Australian National University, June, 2018 |
|
|
|
Aditi Barthwal A formalisation of the theory of context-free languages in higher order logic PhD Thesis, The Australian National University, Canberra, December, 2010 |