×

zbMATH — the first resource for mathematics

Norrish, Michael

Compute Distance To:
Author ID: norrish.michael Recent zbMATH articles by "Norrish, Michael"
Published as: Norrish, Michael
External Links: MGP
Documents Indexed: 39 Publications since 2000, including 1 Book

Publications by Year

Citations contained in zbMATH Open

28 Publications have been cited 167 times in 135 Documents Cited by Year
A brief overview of HOL4. Zbl 1165.68474
Slind, Konrad; Norrish, Michael
42
2008
Cakeml, a verified implementation of ML. Zbl 1284.68405
Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott
21
2014
Types, bytes, and separation logic. Zbl 1295.68094
Tuch, Harvey; Klein, Gerwin; Norrish, Michael
21
2007
Barendregt’s variable convention in rule inductions. Zbl 1213.03024
Urban, Christian; Berghofer, Stefan; Norrish, Michael
11
2007
Mechanisation of AKS algorithm. I. The main theorem. Zbl 1465.68302
Chan, Hing-Lun; Norrish, Michael
7
2015
Recursive function definition for types with binders. Zbl 1099.68735
Norrish, Michael
7
2004
Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations. Zbl 1105.68093
Norrish, Michael
6
2006
(Nominal) unification by recursive descent with triangular substitutions. Zbl 1291.68356
Kumar, Ramana; Norrish, Michael
6
2010
Proof pearl: de Bruijn terms really do work. Zbl 1144.68362
Norrish, Michael; Vestergaard, René
6
2007
The PROSPER toolkit. Zbl 0971.68638
Dennis, Louise A.; Collins, Graham; Norrish, Michael; Boulton, Richard; Slind, Konrad; Robinson, Graham; Gordon, Mike; Melham, Tom
5
2000
Mechanised computability theory. Zbl 1342.68299
Norrish, Michael
5
2011
Complete integer decision procedures as derived rules in HOL. Zbl 1279.68292
Norrish, Michael
4
2003
Verified characteristic formulae for CakeML. Zbl 06721336
Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael
4
2017
A thread of HOL development. Zbl 1008.68122
Norrish, Michael; Slind, Konrad
3
2002
Verified, executable parsing. Zbl 1234.68359
Barthwal, Aditi; Norrish, Michael
3
2009
Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\). Zbl 1317.68227
Norrish, Michael; Huffman, Brian
2
2013
A formalisation of the normal forms of context-free grammars in HOL4. Zbl 1287.68151
Barthwal, Aditi; Norrish, Michael
2
2010
A string of pearls: proofs of Fermat’s little theorem. Zbl 1383.68072
Chan, Hing-Lun; Norrish, Michael
2
2012
Timing UDP: Mechanized semantics for sockets, threads, and failures. Zbl 1077.68597
Wansbrough, Keith; Norrish, Michael; Sewell, Peter; Serjantov, Andrei
1
2002
Verified over-approximation of the diameter of propositionally factored transition systems. Zbl 1465.68170
Abdulaziz, Mohammad; Gretton, Charles; Norrish, Michael
1
2015
Proof pearl: Bounding least common multiples with triangles. Zbl 06644741
Chan, Hing-Lun; Norrish, Michael
1
2016
Mechanisation of PDA and grammar equivalence for context-free languages. Zbl 1253.68201
Barthwal, Aditi; Norrish, Michael
1
2010
Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Zbl 1298.68028
Gonthier, Georges (ed.); Norrish, Michael (ed.)
1
2013
A mechanisation of some context-free language theory in HOL4. Zbl 1433.68531
Barthwal, Aditi; Norrish, Michael
1
2014
Classification of finite fields with applications. Zbl 07100459
Chan, Hing-Lun; Norrish, Michael
1
2019
A string of pearls: proofs of Fermat’s little theorem. Zbl 1451.68320
Chan, Hing Lun; Norrish, Michael
1
2013
Proof-producing synthesis of cakeml with I/O and local state from monadic HOL functions. Zbl 06958128
Ho, Son; Abrahamsson, Oskar; Kumar, Ramana; Myreen, Magnus O.; Tan, Yong Kiam; Norrish, Michael
1
2018
Proof pearl: Bounding least common multiples with triangles. Zbl 07024455
Chan, Hing-Lun; Norrish, Michael
1
2019
Classification of finite fields with applications. Zbl 07100459
Chan, Hing-Lun; Norrish, Michael
1
2019
Proof pearl: Bounding least common multiples with triangles. Zbl 07024455
Chan, Hing-Lun; Norrish, Michael
1
2019
Proof-producing synthesis of cakeml with I/O and local state from monadic HOL functions. Zbl 06958128
Ho, Son; Abrahamsson, Oskar; Kumar, Ramana; Myreen, Magnus O.; Tan, Yong Kiam; Norrish, Michael
1
2018
Verified characteristic formulae for CakeML. Zbl 06721336
Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael
4
2017
Proof pearl: Bounding least common multiples with triangles. Zbl 06644741
Chan, Hing-Lun; Norrish, Michael
1
2016
Mechanisation of AKS algorithm. I. The main theorem. Zbl 1465.68302
Chan, Hing-Lun; Norrish, Michael
7
2015
Verified over-approximation of the diameter of propositionally factored transition systems. Zbl 1465.68170
Abdulaziz, Mohammad; Gretton, Charles; Norrish, Michael
1
2015
Cakeml, a verified implementation of ML. Zbl 1284.68405
Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott
21
2014
A mechanisation of some context-free language theory in HOL4. Zbl 1433.68531
Barthwal, Aditi; Norrish, Michael
1
2014
Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\). Zbl 1317.68227
Norrish, Michael; Huffman, Brian
2
2013
Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Zbl 1298.68028
Gonthier, Georges; Norrish, Michael
1
2013
A string of pearls: proofs of Fermat’s little theorem. Zbl 1451.68320
Chan, Hing Lun; Norrish, Michael
1
2013
A string of pearls: proofs of Fermat’s little theorem. Zbl 1383.68072
Chan, Hing-Lun; Norrish, Michael
2
2012
Mechanised computability theory. Zbl 1342.68299
Norrish, Michael
5
2011
(Nominal) unification by recursive descent with triangular substitutions. Zbl 1291.68356
Kumar, Ramana; Norrish, Michael
6
2010
A formalisation of the normal forms of context-free grammars in HOL4. Zbl 1287.68151
Barthwal, Aditi; Norrish, Michael
2
2010
Mechanisation of PDA and grammar equivalence for context-free languages. Zbl 1253.68201
Barthwal, Aditi; Norrish, Michael
1
2010
Verified, executable parsing. Zbl 1234.68359
Barthwal, Aditi; Norrish, Michael
3
2009
A brief overview of HOL4. Zbl 1165.68474
Slind, Konrad; Norrish, Michael
42
2008
Types, bytes, and separation logic. Zbl 1295.68094
Tuch, Harvey; Klein, Gerwin; Norrish, Michael
21
2007
Barendregt’s variable convention in rule inductions. Zbl 1213.03024
Urban, Christian; Berghofer, Stefan; Norrish, Michael
11
2007
Proof pearl: de Bruijn terms really do work. Zbl 1144.68362
Norrish, Michael; Vestergaard, René
6
2007
Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations. Zbl 1105.68093
Norrish, Michael
6
2006
Recursive function definition for types with binders. Zbl 1099.68735
Norrish, Michael
7
2004
Complete integer decision procedures as derived rules in HOL. Zbl 1279.68292
Norrish, Michael
4
2003
A thread of HOL development. Zbl 1008.68122
Norrish, Michael; Slind, Konrad
3
2002
Timing UDP: Mechanized semantics for sockets, threads, and failures. Zbl 1077.68597
Wansbrough, Keith; Norrish, Michael; Sewell, Peter; Serjantov, Andrei
1
2002
The PROSPER toolkit. Zbl 0971.68638
Dennis, Louise A.; Collins, Graham; Norrish, Michael; Boulton, Richard; Slind, Konrad; Robinson, Graham; Gordon, Mike; Melham, Tom
5
2000
all top 5

Cited by 211 Authors

15 Norrish, Michael
9 Myreen, Magnus O.
6 Fernández, Maribel
6 Kaliszyk, Cezary
6 Kumar, Ramana
6 Nipkow, Tobias
5 Chan, Hing-Lun
5 Klein, Gerwin
5 Owens, Scott
5 Popescu, Andrei
4 Ayala-Rincón, Mauricio
4 Blanchette, Jasmin Christian
4 Hasan, Osman
4 Paulson, Lawrence Charles
4 Slind, Konrad
4 Tahar, Sofiène
3 Ahmed, Waqar
3 Arthan, Rob D.
3 Cheney, James
3 Gauthier, Thibault
3 Gordon, Michael J. C.
3 Guan, Yong
3 Ray, Sandip
3 Rocha-Oliveira, Ana Cristina
3 Sutcliffe, Geoff
3 Urban, Christian
3 Weber, Tjark
2 Bauereiß, Thomas
2 Bengtson, Jesper
2 Blazy, Sandrine
2 Bulwahn, Lukas
2 Copello, Ernesto
2 Davis, Jared
2 de Carvalho-Segundo, Washington
2 Kaufmann, Matt
2 Krauss, Alexander
2 Kunčar, Ondřej
2 Lammich, Peter
2 Li, Yongdong
2 Lochbihler, Andreas
2 Momigliano, Alberto
2 Parrow, Joachim
2 Pesenti Gritti, Armando
2 Pollack, Randy
2 Raimondi, Franco
2 Ricciotti, Wilmer
2 Sato, Masahiko
2 Sewell, Thomas D.
2 Shi, Zhiping
2 Smolka, Gert
2 Sobrinho, Daniele Nantes
2 Szasz, Nora
2 Tan, Yong Kiam
2 Tasistro, Alvaro
2 Tiu, Alwen Fernanto
2 Traytel, Dmitry
2 Urban, Josef
2 Wang, Guohui
2 Wenzel, Makarius
2 Wolff, Burkhart
2 Zhang, Jingzhi
1 Abdulaziz, Mohammad
1 Abel, Andreas M.
1 Abrahamsson, Oskar
1 Adams, Mark
1 Allais, Guillaume
1 Andronick, June
1 Appel, Andrew W.
1 Asperti, Andrea
1 Aspinall, David
1 Bacelar Almeida, José
1 Backes, Julian
1 Ballarin, Clemens
1 Barendregt, Hendrik Pieter
1 Barsotti, Damián
1 Barthwal, Aditi
1 Bartoletti, Massimo
1 Basin, David A.
1 Benzmüller, Christoph Ewald
1 Berghofer, Stefan
1 Beringer, Lennart
1 Besson, Frédéric
1 Blandford, Ann
1 Böhme, Sascha
1 Boulton, Richard J.
1 Bouzy, Aymeric
1 Bove, Ana
1 Bowen, Jonathan P.
1 Brinkop, Hauke
1 Brown, Chad Edward
1 Calude, Cristian S.
1 Cao, Qinxiang
1 Cavalcanti, Ana
1 Chaieb, Amine
1 Charguéraud, Arthur
1 Chen, Zilin
1 Clouston, Ranald A.
1 Cock, David
1 Crespo, Juan Manuel
1 Crole, Roy L.
...and 111 more Authors

Citations by Year