Search the dblp DataBase

Publications of Author

1. Michael Norrish
   Deterministic Expressions in C. [Citation Graph (0, 0)][DBLP]
   ESOP, 1999, pp:147-161 [Conf]
   
2. Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
   Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. [Citation Graph (0, 0)][DBLP]
   ESOP, 2002, pp:278-294 [Conf]
   
3. Michael Norrish
   Mechanising Hankin and Barendregt using the Gordon-Melham axioms. [Citation Graph (0, 0)][DBLP]
   MERLIN, 2003, pp:- [Conf]
   
4. Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
   Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. [Citation Graph (0, 0)][DBLP]
   POPL, 2006, pp:55-66 [Conf]
   
5. Harvey Tuch, Gerwin Klein, Michael Norrish
   Types, bytes, and separation logic. [Citation Graph (0, 0)][DBLP]
   POPL, 2007, pp:97-108 [Conf]
   
6. 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. [Citation Graph (0, 0)][DBLP]
   SIGCOMM, 2005, pp:265-276 [Conf]
   
7. Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham
   The PROSPER Toolkit. [Citation Graph (0, 0)][DBLP]
   TACAS, 2000, pp:78-92 [Conf]
   
8. Michael Norrish
   Complete Integer Decision Procedures as Derived Rules in HOL. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:71-86 [Conf]
   
9. Michael Norrish
   Recursive Function Definition for Types with Binders. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2004, pp:241-256 [Conf]
   
10. Michael Norrish, Konrad Slind
    Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2005, pp:397-408 [Conf]
    
11. Michael Norrish, Konrad Slind
    A Thread of HOL Development. [Citation Graph (0, 0)][DBLP]
    Comput. J., 2002, v:45, n:1, pp:37-45 [Journal]
    
12. Michael Norrish
    Mechanising lambda-calculus using a classical first order theory of terms with permutations. [Citation Graph (0, 0)][DBLP]
    Higher-Order and Symbolic Computation, 2006, v:19, n:2-3, pp:169-195 [Journal]
    
13. Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham
    The PROSPER toolkit. [Citation Graph (0, 0)][DBLP]
    STTT, 2003, v:4, n:2, pp:189-210 [Journal]
    
14. Christian Urban, Stefan Berghofer, Michael Norrish
    Barendregt's Variable Convention in Rule Inductions. [Citation Graph (0, 0)][DBLP]
    CADE, 2007, pp:35-50 [Conf]
    
15. Michael Norrish, René Vestergaard
    Proof Pearl: De Bruijn Terms Really Do Work. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2007, pp:207-222 [Conf]
    
16. 
    A Formalisation of the Normal Forms of Context-Free Grammars in HOL4. [Citation Graph (, )][DBLP]
    
    
17. 
    Verified, Executable Parsing. [Citation Graph (, )][DBLP]
    
    
18. 
    A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. [Citation Graph (, )][DBLP]
    
    
19. 
    A formal treatment of the barendregt variable convention in rule inductions. [Citation Graph (, )][DBLP]
    
    
20. 
    Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets. [Citation Graph (, )][DBLP]
    
    
21. 
    seL4: formal verification of an OS kernel. [Citation Graph (, )][DBLP]
    
    
22. 
    A Brief Overview of HOL4. [Citation Graph (, )][DBLP]
    
    
23. 
    Mind the Gap. [Citation Graph (, )][DBLP]
    
    
24. 
    Mechanisation of PDA and Grammar Equivalence for Context-Free Languages. [Citation Graph (, )][DBLP]
    
    
25. 
    (Nominal) Unification by Recursive Descent with Triangular Substitutions. [Citation Graph (, )][DBLP]
    
    
26. 
    seL4: formal verification of an operating-system kernel. [Citation Graph (, )][DBLP]