BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Czech Republic
1 × Finland
1 × The Netherlands
1 × United Kingdom
2 × France
2 × Germany
4 × USA
Collaborated with:
A.Barthwal R.Kumar M.O.Myreen P.Sewell K.Wansbrough G.Klein H.Tuch T.Ridge C.Urban S.Berghofer O.Abrahamsson Y.K.Tan S.Owens A.Serjantov A.Guéneau Y.Lin K.Wang S.M.Blackburn A.L.Hosking S.Bishop M.Fairbairn M.Smith S.Ho Andreas Lööw Anthony C. J. Fox L.A.Dennis G.Collins R.J.Boulton K.Slind G.Robinson M.J.C.Gordon T.F.Melham K.Elphinstone G.Heiser J.Andronick D.Cock P.Derrin D.Elkaduwe K.Engelhardt R.Kolanski T.Sewell S.Winwood
Talks about:
verifi (5) ml (4) implement (3) cake (3) hol (3) logic (2) tcp (2) characterist (1) determinist (1) yieldpoint (1)

Person: Michael Norrish

DBLP DBLP: Norrish:Michael

Contributed to:

ISMM 20152015
POPL 20142014
CSL 20102010
ESOP 20092009
SOSP 20092009
FM 20082008
CADE 20072007
POPL 20072007
POPL 20062006
ESOP 20022002
TACAS 20002000
ESOP 19991999
ESOP 20172017
IJCAR 20182018
PLDI 20192019

Wrote 15 papers:

ISMM-2015-LinWBHN #behaviour #comprehension
Stop and go: understanding yieldpoint behavior (YL, KW, SMB, ALH, MN), pp. 70–80.
POPL-2014-KumarMNO #implementation #ml #named
CakeML: a verified implementation of ML (RK, MOM, MN, SO), pp. 179–192.
CSL-2010-BarthwalN #context-free grammar #formal method #normalisation
A Formalisation of the Normal Forms of Context-Free Grammars in HOL4 (AB, MN), pp. 95–109.
ESOP-2009-BarthwalN #execution #parsing
Verified, Executable Parsing (AB, MN), pp. 160–174.
SOSP-2009-KleinEHACDEEKNSTW #kernel #named #verification
seL4: formal verification of an OS kernel (GK, KE, GH, JA, DC, PD, DE, KE, RK, MN, TS, HT, SW), pp. 207–220.
FM-2008-RidgeNS #approach #implementation #network #protocol
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service (TR, MN, PS), pp. 294–309.
Barendregt’s Variable Convention in Rule Inductions (CU, SB, MN), pp. 35–50.
POPL-2007-TuchKN #logic
Types, bytes, and separation logic (HT, GK, MN), pp. 97–108.
POPL-2006-BishopFNSSW #implementation #logic #specification #testing
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations (SB, MF, MN, PS, MS, KW), pp. 55–66.
ESOP-2002-WansbroughNSS #semantics #thread
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures (KW, MN, PS, AS), pp. 278–294.
TACAS-2000-DennisCNBSRGM #tool support
The PROSPER Toolkit (LAD, GC, MN, RJB, KS, GR, MJCG, TFM), pp. 78–92.
ESOP-1999-Norrish #c
Deterministic Expressions in C (MN), pp. 147–161.
Verified Characteristic Formulae for CakeML (AG, MOM, RK, MN), pp. 584–610.
IJCAR-2018-HoAKMTN #monad #synthesis
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (SH, OA, RK, MOM, YKT, MN), pp. 646–662.
PLDI-2019-LoowKTMNAF #compilation
Verified compilation on a verified processor (AL, RK, YKT, MOM, MN, OA, ACJF), pp. 1041–1053.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.