Michael Norrish

	2009
22		Aditi Barthwal, Michael Norrish: Verified, Executable Parsing. ESOP 2009: 160-174
21		Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood: seL4: formal verification of an OS kernel. SOSP 2009: 207-220
20		Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish: Mind the Gap. TPHOLs 2009: 500-515
	2008
19		Tom Ridge, Michael Norrish, Peter Sewell: A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. FM 2008: 294-309
18		Konrad Slind, Michael Norrish: A Brief Overview of HOL4. TPHOLs 2008: 28-32
	2007
17		Christian Urban, Stefan Berghofer, Michael Norrish: Barendregt's Variable Convention in Rule Inductions. CADE 2007: 35-50
16		Harvey Tuch, Gerwin Klein, Michael Norrish: Types, bytes, and separation logic. POPL 2007: 97-108
15		Michael Norrish, René Vestergaard: Proof Pearl: De Bruijn Terms Really Do Work. TPHOLs 2007: 207-222
	2006
14		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		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		Christian Urban, Michael Norrish: A formal treatment of the barendregt variable convention in rule inductions. MERLIN 2005: 25-32
11		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		Michael Norrish, Konrad Slind: Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. TPHOLs 2005: 397-408
	2004
9		Michael Norrish: Recursive Function Definition for Types with Binders. TPHOLs 2004: 241-256
	2003
8		Michael Norrish: Mechanising Hankin and Barendregt using the Gordon-Melham axioms. MERLIN 2003
7		Michael Norrish: Complete Integer Decision Procedures as Derived Rules in HOL. TPHOLs 2003: 71-86
6		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		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		Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov: Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. ESOP 2002: 278-294
3		Michael Norrish, Konrad Slind: A Thread of HOL Development. Comput. J. 45(1): 37-45 (2002)
	2000
2		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		Michael Norrish: Deterministic Expressions in C. ESOP 1999: 147-161

Coauthor Index

1	June Andronick	[20] [21]
2	Aditi Barthwal	[22]
3	Stefan Berghofer	[17]
4	Steve Bishop	[11] [14]
5	Richard J. Boulton	[2] [6]
6	David Cock	[20] [21]
7	Graham Collins	[2] [6]
8	Louise A. Dennis	[2] [6]
9	Philip Derrin	[21]
10	Dhammika Elkaduwe	[21]
11	Kevin Elphinstone	[21]
12	Kai Engelhardt	[21]
13	Matthew Fairbairn	[11] [14]
14	Michael J. C. Gordon	[2]
15	Gernot Heiser	[21]
16	Gerwin Klein	[16] [20] [21]
17	Rafal Kolanski	[21]
18	Thomas F. Melham	[2] [6]
19	Tom Ridge (Thomas Ridge)	[19]
20	Graham Robinson	[2]
21	Andrei Serjantov	[4]
22	Peter Sewell	[4] [5] [11] [14] [19]
23	Thomas Sewell	[20] [21]
24	Konrad Slind	[2] [3] [6] [10] [18]
25	Michael Smith	[11] [14]
26	Harvey Tuch	[16] [21]
27	Christian Urban	[12] [17]
28	René Vestergaard	[15]
29	Keith Wansbrough	[4] [5] [11] [14]
30	Simon Winwood	[20] [21]

Colors in the list of coauthors