| 2009 |
|---|
| 20 | EE | Aditi Barthwal,
Michael Norrish:
Verified, Executable Parsing.
ESOP 2009: 160-174 |
| 2008 |
|---|
| 19 | EE | Tom Ridge,
Michael Norrish,
Peter Sewell:
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service.
FM 2008: 294-309 |
| 18 | EE | Konrad Slind,
Michael Norrish:
A Brief Overview of HOL4.
TPHOLs 2008: 28-32 |
| 2007 |
|---|
| 17 | EE | Christian Urban,
Stefan Berghofer,
Michael Norrish:
Barendregt's Variable Convention in Rule Inductions.
CADE 2007: 35-50 |
| 16 | EE | Harvey Tuch,
Gerwin Klein,
Michael Norrish:
Types, bytes, and separation logic.
POPL 2007: 97-108 |
| 15 | EE | Michael Norrish,
René Vestergaard:
Proof Pearl: De Bruijn Terms Really Do Work.
TPHOLs 2007: 207-222 |
| 2006 |
|---|
| 14 | EE | Steve Bishop,
Matthew Fairbairn,
Michael Norrish,
Peter Sewell,
Michael Smith,
Keith Wansbrough:
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations.
POPL 2006: 55-66 |
| 13 | EE | Michael Norrish:
Mechanising lambda-calculus using a classical first order theory of terms with permutations.
Higher-Order and Symbolic Computation 19(2-3): 169-195 (2006) |
| 2005 |
|---|
| 12 | EE | Christian Urban,
Michael Norrish:
A formal treatment of the barendregt variable convention in rule inductions.
MERLIN 2005: 25-32 |
| 11 | EE | Steve Bishop,
Matthew Fairbairn,
Michael Norrish,
Peter Sewell,
Michael Smith,
Keith Wansbrough:
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets.
SIGCOMM 2005: 265-276 |
| 10 | EE | Michael Norrish,
Konrad Slind:
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.
TPHOLs 2005: 397-408 |
| 2004 |
|---|
| 9 | EE | Michael Norrish:
Recursive Function Definition for Types with Binders.
TPHOLs 2004: 241-256 |
| 2003 |
|---|
| 8 | EE | Michael Norrish:
Mechanising Hankin and Barendregt using the Gordon-Melham axioms.
MERLIN 2003 |
| 7 | EE | Michael Norrish:
Complete Integer Decision Procedures as Derived Rules in HOL.
TPHOLs 2003: 71-86 |
| 6 | EE | Louise A. Dennis,
Graham Collins,
Michael Norrish,
Richard J. Boulton,
Konrad Slind,
Thomas F. Melham:
The PROSPER toolkit.
STTT 4(2): 189-210 (2003) |
| 2002 |
|---|
| 5 | EE | Michael Norrish,
Peter Sewell,
Keith Wansbrough:
Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets.
ACM SIGOPS European Workshop 2002: 49-53 |
| 4 | EE | Keith Wansbrough,
Michael Norrish,
Peter Sewell,
Andrei Serjantov:
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures.
ESOP 2002: 278-294 |
| 3 | EE | Michael Norrish,
Konrad Slind:
A Thread of HOL Development.
Comput. J. 45(1): 37-45 (2002) |
| 2000 |
|---|
| 2 | EE | Louise A. Dennis,
Graham Collins,
Michael Norrish,
Richard J. Boulton,
Konrad Slind,
Graham Robinson,
Michael J. C. Gordon,
Thomas F. Melham:
The PROSPER Toolkit.
TACAS 2000: 78-92 |
| 1999 |
|---|
| 1 | EE | Michael Norrish:
Deterministic Expressions in C.
ESOP 1999: 147-161 |
