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: Norrish:Michael
Contributed to:
2015
2014
2010
2009
2009
2008
2007200720062002
200019992017
2018
2019Wrote 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.
- CADE-2007-UrbanBN
- 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.
- ESOP-2017-GueneauMKN
- 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.