The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Michael Norrish: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

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]


Search in 0.002secs, Finished in 0.003secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002