Michael Norrish

According to our database1, Michael Norrish authored at least 68 papers between 1999 and 2021.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2021
TacticToe: Learning to Prove with Tactics.
J. Autom. Reason., 2021

Mechanisation of the AKS Algorithm.
J. Autom. Reason., 2021

TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning.
CoRR, 2021

On the formalisation of Kolmogorov complexity.
Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020
Proof-Producing Synthesis of CakeML from Monadic HOL Functions.
J. Autom. Reason., 2020

Mechanised Modal Model Theory.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
The verified CakeML compiler backend.
J. Funct. Program., 2019

Classification of Finite Fields with Applications.
J. Autom. Reason., 2019

Proof Pearl: Bounding Least Common Multiples with Triangles.
J. Autom. Reason., 2019

Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API.
J. ACM, 2019

MoonLight: Effective Fuzzing with Near-Optimal Corpus Distillation.
CoRR, 2019

Verified compilation on a verified processor.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Designing a low-level virtual machine for implementing real-time managed languages.
Proceedings of the 11th ACM SIGPLAN International Workshop on Virtual Machines and Intermediate Languages, 2019

A Verified Compositional Algorithm for AI Planning.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Modular synthesis of verified verifiers of computation with STV algorithms.
Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, 2019

2018
Formally Verified Algorithms for Upper-Bounding State Space Diameters.
J. Autom. Reason., 2018

Learning to Prove with Tactics.
CoRR, 2018

Verified Certificate Checking for Counting Votes.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Hop, Skip, & Jump: Practical On-Stack Replacement for a Cross-Platform Language-Neutral VM.
Proceedings of the 14th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments, 2018

Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017
Verifying efficient function calls in CakeML.
Proc. ACM Program. Lang., 2017

Verified Characteristic Formulae for CakeML.
Proceedings of the Programming Languages and Systems, 2017

A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds.
Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling, 2017

2016
Rust as a language for high performance GC implementation.
Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management, Santa Barbara, CA, USA, June 14, 2016

A new verified compiler backend for CakeML.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015
Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development.
Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Stop and go: understanding yieldpoint behavior.
Proceedings of the 2015 ACM SIGPLAN International Symposium on Memory Management, 2015

Mechanisation of AKS Algorithm: Part 1 - The Main Theorem.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Exploiting Symmetries by Planning for a Descriptive Quotient.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

2014
A mechanisation of some context-free language theory in HOL4.
J. Comput. Syst. Sci., 2014

CakeML: a verified implementation of ML.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

An Approach for Proving the Correctness of Inspector/Executor Transformations.
Proceedings of the Languages and Compilers for Parallel Computing, 2014

Beagle as a HOL4 external ATP method.
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013
A String of Pearls: Proofs of Fermat's Little Theorem.
J. Formaliz. Reason., 2013

Tableaux for Verification of Data-Centric Processes.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012
Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax.
J. Autom. Reason., 2012

Reasoning with Data-Centric Business Processes
CoRR, 2012

2011
Mechanised Computability Theory.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010
seL4: formal verification of an operating-system kernel.
Commun. ACM, 2010

Mechanisation of PDA and Grammar Equivalence for Context-Free Languages.
Proceedings of the Logic, 2010

(Nominal) Unification by Recursive Descent with Triangular Substitutions.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Formalisation of the Normal Forms of Context-Free Grammars in HOL4.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009
Rewriting Conversions Implemented with Continuations.
J. Autom. Reason., 2009

Mind the Gap.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

seL4: formal verification of an OS kernel.
Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

Verified, Executable Parsing.
Proceedings of the Programming Languages and Systems, 2009

2008
A Brief Overview of HOL4.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service.
Proceedings of the FM 2008: Formal Methods, 2008

2007
Proof Pearl: De Bruijn Terms Really Do Work.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Types, bytes, and separation logic.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Barendregt's Variable Convention in Rule Inductions.
Proceedings of the Automated Deduction, 2007

2006
Mechanising lambda-calculus using a classical first order theory of terms with permutations.
High. Order Symb. Comput., 2006

Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations.
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

2005
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets.
Proceedings of the ACM SIGCOMM 2005 Conference on Applications, 2005

A formal treatment of the barendregt variable convention in rule inductions.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2005

2004
Recursive Function Definition for Types with Binders.
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

2003
The PROSPER toolkit.
Int. J. Softw. Tools Technol. Transf., 2003

Complete Integer Decision Procedures as Derived Rules in HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Mechanising Hankin and Barendregt using the Gordon-Melham axioms.
Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

2002
A Thread of HOL Development.
Comput. J., 2002

Rigour is good for you <i>and</i> feasible: reflections on formal treatments of C and UDP sockets.
Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002, 2002

Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures.
Proceedings of the Programming Languages and Systems, 2002

2000
The PROSPER Toolkit.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

1999
Deterministic Expressions in C.
Proceedings of the Programming Languages and Systems, 1999


  Loading...