Skip navigation
Skip navigation

Browsing by Author Norrish, Michael

Or enter first few letters:  
Showing results 1 to 20 of 30

A brief overview of HOL4

Author(s)Slind, Konrad; Norrish, Michael
TypeConference paper
Date Published2008
Date CreatedAugust 18-21 2008

A formal treatment of the Barendregt variable convention in rule inductions

Author(s)Urban, Christian; Norrish, Michael
TypeConference paper
Date Published2005
Date CreatedSeptember 30 2005

A Formalisation of the Normal Forms of Context-Free Grammars in HOL4

Author(s)Barthwal, Aditi; Norrish, Michael
TypeConference paper
Date Published2010
Date CreatedJuly 16 2010

A mechanisation of some context-free language theory in HOL4

Author(s)Barthwal, Aditi; Norrish, Michael
TypeJournal article
Date Published2014
Date Created-

A rigorous approach to networking: TCP, from implementation to protocol to service

Author(s)Ridge, Tom; Norrish, Michael; Sewell, Peter
TypeBook chapter
Date Published2008
Date Created-

A string of pearls: Proofs of Fermat's Little Theorem

Author(s)Chan, Hing Lun (Joseph); Norrish, Michael
TypeConference paper
Date Published2012
Date CreatedDecember 13-15 2012

A String of Pearls: Proofs of Fermat's Little Theorem

Author(s)Chan, Hing Lun (Joseph); Norrish, Michael
TypeJournal article
Date Published2013
Date Created-

Barendregt's variable convention in rule inductions

Author(s)Urban, Christian; Berghofer, Stefan; Norrish, Michael
TypeConference paper
Date Published2007
Date CreatedJuly 17-20 2007

CakeML: A Verified Implementation of ML

Author(s)Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael, et al
TypeConference paper
Date Published2014
Date CreatedJanuary 22-24 2014

Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations

Author(s)Bishop, Steve; Fairbairn, Matthew; Norrish, Michael, et al
TypeConference paper
Date Published2006
Date CreatedJanuary 11-13 2006

Exploiting Symmetries by Planning for a Descriptive Quotient

Author(s)Mansour (Abdulaziz), Mohammad; Norrish, Michael; Gretton, Charles
TypeConference paper
Date Published2015
Date CreatedJuly 25-31, 2015

Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax

Author(s)Cheney, James; Norrish, Michael; Vestergaard, Rene
TypeJournal article
Date Published2012
Date Created-

Mechanisation of AKS algorithm: Part 1 - The main theorem

Author(s)Chan, Hing Lun (Joseph); Norrish, Michael
TypeConference paper
Date Published2015
Date Created24 August 2015 through 27 August 2015

Mechanisation of PDA and Grammar Equivalence for Context-Free Languages

Author(s)Barthwal, Aditi; Norrish, Michael
TypeConference paper
Date Published2010
Date CreatedJuly 16 2010

Mechanised Computability Theory

Author(s)Norrish, Michael
TypeConference paper
Date Published2011
Date CreatedAugust 22-25 2011

Mechanising lambda-calculus using a classical first order theory of terms with permutations

Author(s)Norrish, Michael
TypeJournal article
Date Published2006
Date Created-

Mind the Gap: Verification Framework for Low-Level C

Author(s)Winwood, Simon; Klein, Gerwin; Sewell, Thomas, et al
TypeConference paper
Date Published2009
Date CreatedAugust 17-20 2009

(Nominal) Unification by Recursive Descent with Triangular Substitutions

Author(s)Kumar, Ramana; Norrish, Michael
TypeConference paper
Date Published2010
Date CreatedJuly 11 2010

Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1

Author(s)Norrish, Michael; Huffman, Brian
TypeBook chapter
Date Published2013
Date Created-

Proof pearl: de Bruijn terms really do work

Author(s)Norrish, Michael; Vestergaard, Rene
TypeBook chapter
Date Published2007
Date Created-

Updated:  12 April 2016/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator