×
Author ID: myreen.magnus-o Recent zbMATH articles by "Myreen, Magnus O."
Published as: Myreen, Magnus O.; Myreen, Magnus

Publications by Year

Citations contained in zbMATH Open

22 Publications have been cited 173 times in 106 Documents Cited by Year
Cakeml, a verified implementation of ML. Zbl 1284.68405
Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott
46
2014
HOL with definitions: semantics, soundness, and a verified implementation. Zbl 1416.68167
Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott
13
2014
Proof-producing translation of higher-order logic into pure and stateful ML. Zbl 1297.68053
Myreen, Magnus O.; Owens, Scott
13
2014
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation. Zbl 1356.68194
Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott
13
2016
The verified CakeML compiler backend. Zbl 1493.68091
Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael
12
2019
Hoare logic for realistically modelled machine code. Zbl 1186.68118
Myreen, Magnus O.; Gordon, Michael J. C.
10
2007
A trustworthy monadic formalization of the ARMv7 instruction set architecture. Zbl 1291.68341
Fox, Anthony; Myreen, Magnus O.
9
2010
Verified characteristic formulae for CakeML. Zbl 1485.68030
Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael
8
2017
The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1356.68186
Davis, Jared; Myreen, Magnus O.
8
2015
A verified runtime for a verified theorem prover. Zbl 1342.68297
Myreen, Magnus O.; Davis, Jared
6
2011
Verified just-in-time compiler on x86. Zbl 1312.68046
Myreen, Magnus O.
5
2010
The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1416.68174
Myreen, Magnus O.; Davis, Jared
5
2014
Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions. Zbl 1468.68060
Ho, Son; Abrahamsson, Oskar; Kumar, Ramana; Myreen, Magnus O.; Tan, Yong Kiam; Norrish, Michael
5
2018
cake_lpr: verified propagation redundancy checking in CakeML. Zbl 1474.68194
Tan, Yong Kiam; Heule, Marijn J. H.; Myreen, Magnus O.
4
2021
A verified generational garbage collector for CakeML. Zbl 1468.68065
Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes
3
2017
Transforming programs into recursive functions. Zbl 1347.68304
Myreen, Magnus O.; Gordon, Michael J. C.
3
2009
Separation logic adapted for proofs by rewriting. Zbl 1291.68363
Myreen, Magnus O.
2
2010
Proof-producing synthesis of ML from higher-order logic. Zbl 1291.68364
Myreen, Magnus O.; Owens, Scott
2
2012
Automatically introducing tail recursion in CakeML. Zbl 1505.68004
Abrahamsson, Oskar; Myreen, Magnus O.
2
2018
Steps towards verified implementations of HOL Light. Zbl 1317.68225
Myreen, Magnus O.; Owens, Scott; Kumar, Ramana
2
2013
Hoare logic for ARM machine code. Zbl 1141.68373
Myreen, Magnus O.; Fox, Anthony C. J.; Gordon, Michael J. C.
1
2007
Software verification with ITPs should use binary code extraction to reduce the TCB (short paper). Zbl 1511.68320
Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O.
1
2018
cake_lpr: verified propagation redundancy checking in CakeML. Zbl 1474.68194
Tan, Yong Kiam; Heule, Marijn J. H.; Myreen, Magnus O.
4
2021
The verified CakeML compiler backend. Zbl 1493.68091
Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael
12
2019
Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions. Zbl 1468.68060
Ho, Son; Abrahamsson, Oskar; Kumar, Ramana; Myreen, Magnus O.; Tan, Yong Kiam; Norrish, Michael
5
2018
Automatically introducing tail recursion in CakeML. Zbl 1505.68004
Abrahamsson, Oskar; Myreen, Magnus O.
2
2018
Software verification with ITPs should use binary code extraction to reduce the TCB (short paper). Zbl 1511.68320
Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O.
1
2018
Verified characteristic formulae for CakeML. Zbl 1485.68030
Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael
8
2017
A verified generational garbage collector for CakeML. Zbl 1468.68065
Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes
3
2017
Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation. Zbl 1356.68194
Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott
13
2016
The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1356.68186
Davis, Jared; Myreen, Magnus O.
8
2015
Cakeml, a verified implementation of ML. Zbl 1284.68405
Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott
46
2014
HOL with definitions: semantics, soundness, and a verified implementation. Zbl 1416.68167
Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott
13
2014
Proof-producing translation of higher-order logic into pure and stateful ML. Zbl 1297.68053
Myreen, Magnus O.; Owens, Scott
13
2014
The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1416.68174
Myreen, Magnus O.; Davis, Jared
5
2014
Steps towards verified implementations of HOL Light. Zbl 1317.68225
Myreen, Magnus O.; Owens, Scott; Kumar, Ramana
2
2013
Proof-producing synthesis of ML from higher-order logic. Zbl 1291.68364
Myreen, Magnus O.; Owens, Scott
2
2012
A verified runtime for a verified theorem prover. Zbl 1342.68297
Myreen, Magnus O.; Davis, Jared
6
2011
A trustworthy monadic formalization of the ARMv7 instruction set architecture. Zbl 1291.68341
Fox, Anthony; Myreen, Magnus O.
9
2010
Verified just-in-time compiler on x86. Zbl 1312.68046
Myreen, Magnus O.
5
2010
Separation logic adapted for proofs by rewriting. Zbl 1291.68363
Myreen, Magnus O.
2
2010
Transforming programs into recursive functions. Zbl 1347.68304
Myreen, Magnus O.; Gordon, Michael J. C.
3
2009
Hoare logic for realistically modelled machine code. Zbl 1186.68118
Myreen, Magnus O.; Gordon, Michael J. C.
10
2007
Hoare logic for ARM machine code. Zbl 1141.68373
Myreen, Magnus O.; Fox, Anthony C. J.; Gordon, Michael J. C.
1
2007
all top 5

Cited by 230 Authors

13 Myreen, Magnus O.
7 Nipkow, Tobias
6 Kumar, Ramana
6 Popescu, Andrei
5 Heule, Marijn J. H.
4 Murray, Toby
4 Norrish, Michael
4 Schlichtkrull, Anders
3 Abrahamsson, Oskar
3 Bryant, Randal E.
3 Fox, Anthony C. J.
3 Kaliszyk, Cezary
3 Keller, Gabriele Cornelia
3 Klein, Gerwin
3 Kunčar, Ondřej
3 Lammich, Peter
3 Owens, Scott
3 Paulson, Lawrence Charles
3 Pichardie, David
3 Rizkallah, Christine
3 Sutcliffe, Geoff
3 Tan, Yong Kiam
2 Abate, Carmine
2 Adams, Mark
2 Åman Pohjola, Johannes
2 Appel, Andrew W.
2 Arthan, Rob D.
2 Bauereiß, Thomas
2 Blazy, Sandrine
2 Bohrer, Brandon
2 Chen, Zilin
2 Davis, Jared
2 Gauthier, Thibault
2 Hou, Zhe
2 Immler, Fabian
2 Liu, Yang
2 O’Connor, Liam
2 Pesenti Gritti, Armando
2 Raimondi, Franco
2 Reeves, Joseph E.
2 Roßkopf, Simon
2 Sanán, David
2 Sandberg Ericsson, Adam
2 Sewell, Thomas D.
2 Slind, Konrad
2 Tiu, Alwen Fernanto
2 Urban, Josef
2 Wang, Yuting
2 Wenzel, Makarius
1 Abdulaziz, Mohammad
1 Abel, Andreas M.
1 Allais, Guillaume
1 Åman, Pohjola Johannes
1 Amani, Sidney
1 Annenkov, Danil
1 Back, Ralph-Johan
1 Baek, Seulkee
1 Bauer, Gertrud
1 Bengtson, Jesper
1 Bérard, Béatrice
1 Beringer, Lennart
1 Blanco, Roberto
1 Blot, Arthur
1 Bockenek, Joshua A.
1 Böhm, Peter
1 Bollig, Benedikt
1 Boulton, Richard J.
1 Breitner, Joachim
1 Brinkop, Hauke
1 Brown, Chad Edward
1 Bundy, Alan
1 Busi, Matteo
1 Cachera, David
1 Cao, Qinxiang
1 Chakravarty, Manuel M. T.
1 Charguéraud, Arthur
1 Chlipala, Adam J.
1 Christensen, Michael F.
1 Ciobâcă, Ştefan
1 Cohen, Joshua M.
1 Coughlin, Nicholas
1 Crary, Karl
1 Crespo, Juan Manuel
1 Dagand, Pierre-Evariste
1 Dalla Preda, Mila
1 Dang, Tat Dat
1 Debray, Saumya K.
1 Delaware, Benjamin
1 Demange, Delphine
1 Demba, Moussa
1 Dietsch, Daniel
1 Dodds, Josiah
1 Dong, JinSong
1 Durier, Adrien
1 Engelhardt, Kai
1 Eriksson, Johannes
1 Ernst, Gidon
1 Fallenstein, Benya
1 Farzan, Azadeh
1 Fava, Daniel Schnetzer
...and 130 more Authors

Citations by Year