Mr Michael Norrish
Areas of expertise
- Mathematical Software 080204
- Networking And Communications 080503
- Computational Logic And Formal Languages 080203
- Computation Theory And Mathematics 0802
Biography
Research interests:
My research interests lie in the areas of formal methods, interactive theorem proving (I am one of the developers of the HOL4 system), and formal semantics for complicated real-world systems. I am currently involved in the Trustworthy Embedded Systems project within NICTA, and in various collaborations around the world.
Bio:
I received my PhD in 1999 from the University of Cambridge, and was an undergraduate at Victoria University of Wellington.
Available student projects
Theory of Co-algebraic Types with Binders - Keywords: nominal theory, mechanisation, theorem-proving
Publications
- Bishop, S, Fairbairn, M, Mehnert, H et al 2018, 'Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the Sockets API', Journal of the ACM, vol. 66, no. 1, pp. 1-77pp.
- Abdulaziz, M, Norrish, M & Gretton, C 2018, 'Formally Verified Algorithms for Upper-Bounding State Space Diameters', Journal of Automated Reasoning, vol. 61, no. 1, pp. 485-520.
- Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, Michael Norrish, 2018, 'Hop, Skip, & Jump: Practical on-stack replacement for a cross-platform language-neutral VM', 14th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments, VEE 2018, Williamsburg, Virginia, pp. 1-16. doi: 10.1145/3186411.3186412
- CHAN, H & Norrish, M 2017, 'Proof Pearl: Bounding Least Common Multiples with Triangles', Journal of Automated Reasoning, pp. 1-22.
- Abdulaziz, M, Gretton, C & Norrish, M 2017, 'A state-space acyclicity property for exponentially tighter plan length bounds', 27th International Conference on Automated Planning and Scheduling (ICAPS 2017), AAAI Press, AAAI Press, pp. 2-10.
- Guéneau, A, Myreen, M, Kumar, R et al 2017, 'Verified characteristic formulae for CakeML', 26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, ed. Yang H., Conference Organising Committee, TBC, pp. 584-610.
- CHAN, H & Norrish, M 2016, 'Proof pearl: Bounding least common multiples with triangles', International Conference on Interactive Theorem Proving, ITP 2016, ed. Blanchette J.C.Merz, Springer International Publishing Switzerland, Switzerland, pp. 140-150.
- Y. Lin, S. M. Blackburn, A. L. Hosking, and M. Norrish. Rust as a language for high performance GC implementation. In ACM SIGPLAN International Symposium on Memory Management, ISMM, pages 89–98, Santa Barbara, California, June 2016. doi: 10.1145/2926697.2926707
- Norrish, M & Strout, M 2015, 'An Approach for Proving the Correctness of Inspector/Executor Transformations', Lecture Notes in Computer Science (LNCS), vol. 8967, pp. 131-145.
- Abdulaziz, M, Gretton, C & Norrish, M 2015, 'Verified over-approximation of the diameter of propositionally factored transition systems', 6th International Conference on Interactive Theorem Proving, ITP 2015, ed. Zhang X.Urban C., Springer International Publishing Switzerland, TBC, pp. 1-16.
- Abdulaziz, M, Norrish, M & Gretton, C 2015, 'Exploiting Symmetries by Planning for a Descriptive Quotient', International Joint Conference on Artificial Intelligence IJCAI 2015, ed. Qiang Yang, Michael Wooldridge, AAAI Press, Palo Alto, California, USA, pp. 1479-1486.
- Chan, H & Norrish, M 2015, 'Mechanisation of AKS algorithm: Part 1—The main theorem', 6th International Conference on Interactive Theorem Proving, ITP 2015, ed. Zhang X.Urban C., Conference Organising Committee, TBC, pp. 117-136.
- K. Wang, Y. Lin, S. M. Blackburn, M. Norrish, and A. L. Hosking. Draining the swamp: Micro virtual machines as solid foundation for language development. In T. Ball, R. Bodík, S. Krishnamurthi, B. S. Lerner, and G. Morrisett, editors, Inaugural Summit on Advances in Programming Languages, SNAPL, pages 321–336, Asilomar, California, May 2015. doi: 10.4230/LIPIcs.SNAPL.2015.321
- Y. Lin, K. Wang, S. M. Blackburn, A. L. Hosking, and M. Norrish. Stop and go: Understanding yieldpoint behavior. In ACM SIGPLAN International Symposium on Memory Management, ISMM, pages 70–80, Portland, Oregon, June 2015. doi: 10.1145/2754169.2754187
- Barthwal, A & Norrish, M 2014, 'A mechanisation of some context-free language theory in HOL4', Journal of Computer and System Sciences, vol. 80, no. 2, pp. 346-362.
- Kumar, R, Norrish, M, Owens, S et al 2014, 'CakeML: A Verified Implementation of ML', POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery (ACM), USA, pp. 179-191.
- Bauer, A, Baumgartner, P, Diller, M, Norrish, M. 2013, 'Tableaux for Verification of Data-Centric Processes', TABLEAUX 2013, ed. D. Galmiche and D. Larchey-Wendling, Springer-Verlag Berlin Heidelberg, USA, pp. 23-43.
- Chan, H & Norrish, M 2013, 'A String of Pearls: Proofs of Fermat’s Little Theorem', Journal of Formalized Reasoning, vol. 6, no. 1, 2013, pp. 63-87.
- Norrish, M & Huffman, B 2013, 'Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) omega_1', in Sandrine Blazy, Christin Paulin-Mohring, David Pichardie (ed.), Lecture Notes in Computer Science: Interactive Theorem Proving, Springer Science + Business Media, Chennai, India, pp. 133-146.
- Cheney, J, Norrish, M & Vestergaard, R 2012, 'Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax', Journal of Automated Reasoning, vol. 49, no. 2, pp. 209-239.
- Chan H-L, Norrish, M 2012, 'A string of pearls: Proofs of Fermat's Little Theorem', 2nd International Conference on Certified Programs CPP 2012, Conference Organising Committee, Kyoto, pp. 188-207.
- Norrish, M 2011, 'Mechanised Computability Theory', International Conference on Interactive Theorem Proving (ITP 2011), ed. van Eekelen, Springer, Berlin Germany, p. 15.
- Klein, G, Andronick, J, Elphinstone, K et al 2010, 'SeL4: Formal verification of an operating-system kernel', Communications of the Association for Computing Machinery, vol. 53, no. 6, pp. 107-115.
- Barthwal, A & Norrish, M 2010, 'A Formalisation of the Normal Forms of Context-Free Grammars in HOL4', Workshop on Logic, Language, Information and Computation (WoLLIC 2010), ed. Anuj Dawar, Springer, Berlin, p. 15.
- Kumar, R & Norrish, M 2010, '(Nominal) Unification by Recursive Descent with Triangular Substitutions', International Conference on Interactive Theorem Proving (ITP 2010), Springer, Berlin, p. 16.
- Barthwal, A & Norrish, M 2010, 'Mechanisation of PDA and Grammar Equivalence for Context-Free Languages', Workshop on Logic, Language, Information and Computation (WoLLIC 2010), ed. Anuj Dawar, Springer, Berlin, p. 10.
- Klein, G, Elphinstone, K, Heiser, G et al 2009, 'seL4: Formal Verification of an OS Kernel', ACM Symposium on Operating Systems Principles (SOSP 2009), ed. J. Matthews, T. Anderson, Association for Computing Machinery Inc (ACM), New York, pp. 207-220.
- Winwood, S, Klein, G, Sewell, T et al 2009, 'Mind the Gap: Verification Framework for Low-Level C', International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), ed. S.Berghofer, T Nipkow, C. urban, MWenzel, Springer, Germany, pp. 500-515.
- Barthwal, A & Norrish, M 2009, 'Verified, Executable Parsing', in Giuseppe Castagna (ed.), Programming Languages and Systems (ETAPS 2009), Springer, Berlin, Germany, pp. 160-174.
- Norrish, M 2009, 'Rewriting Conversions Implemented with Continuations', Journal of Automated Reasoning, vol. 43, no. 3, pp. 305-336.
- Slind, K & Norrish, M 2008, 'A brief overview of HOL4', International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), ed. O.A. Mohamed, C. Munoz, S. Tahar, Springer, Berlin, Germany, pp. 28-32.
- Ridge, T, Norrish, M & Sewell, P 2008, 'A rigorous approach to networking: TCP, from implementation to protocol to service', in J. Cuellar, T. Maibaum, K. Sere (ed.), International Symposium of Formal Methods Europe, Springer, Berlin, Germany, pp. 294-309.
- Tuch, H, Klein, G & Norrish, M 2007, 'Types, bytes, and separation logic', ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), ed. M. Hormann & M. Felleisen, Association for Computing Machinery Inc (ACM), USA, pp. 97-108.
- Norrish, M & Vestergaard, R 2007, 'Proof pearl: de Bruijn terms really do work', in Klaus Schneider, Jens Brandt (ed.), Theorem Proving in Higher Order Logics, Springer, Berlin, Germany, pp. 207-222.
- Urban, C, Berghofer, S & Norrish, M 2007, 'Barendregt's variable convention in rule inductions', International Conference on Automated Deduction (CADE 2007), ed. Frank Pfenning, Springer, New York, pp. 35-50.
- Norrish, M 2006, 'Mechanising lambda-calculus using a classical first order theory of terms with permutations', Higher-Order and Symbolic Computation, vol. 19, no. 2-3, pp. 169-195.
- Bishop, S, Fairbairn, M, Norrish, M et al 2006, 'Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations', ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006), ed. J.G. Morrisett, S.L. Peyton Jones, Association for Computing Machinery Inc (ACM), USA, pp. 55-66.
- Norrish, M & Slind, K 2005, 'Proof pearl: using combinators to manipulate let-expressions in proof', in Joe Hurd, Tom Helham (ed.), Theorem Proving in Higher Order Logics: 18th international conference TPHOLs 2005, Oxford 2005, proceedings, Springer, United Kingdom, pp. 397-408.
- Bishop, S, Fairbairn, M, Norrish, M et al 2005, 'Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets', SIGCOMM Computer Communications Review, vol. 35, no. 4, pp. 265-276.
- Urban, C & Norrish, M 2005, 'A formal treatment of the Barendregt variable convention in rule inductions', ACM SIGPLAN Workshop on MEchanized Reasoning about Languages with VarIable BiNding (MERLIN 2005), ed. Alberto Momigliano, Randy Pollack, Association for Computing Machinery Inc (ACM), Tallinn, Estonia, pp. 25-32.
- Bishop, S, Fairbairn, M, Norrish, M et al 2005, TCP, UDP, and sockets: rigorous and experimentally-validated behavioural specification, University of Cambridge Computer Laboratory.
- Norrish, M 2004, 'Recursive function definition for types with binders', in Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (ed.), Theorem Proving in Higher Order Logics: 17th international conference, TPHOLs 2004, Springer, Berlin, Germany, pp. 241-256.