Edit Profile (opens in new tab) Myreen, Magnus O. Compute Distance To: Compute Author ID: myreen.magnus-o Published as: Myreen, Magnus O.; Myreen, Magnus Documents Indexed: 27 Publications since 2007 1 Contribution as Editor Co-Authors: 21 Co-Authors with 26 Joint Publications 182 Co-Co-Authors all top 5 Co-Authors 2 single-authored 10 Kumar, Ramana 7 Owens, Scott 5 Norrish, Michael 4 Gordon, Michael J. C. 4 Tan, Yong Kiam 3 Abrahamsson, Oskar 3 Davis, Jared 3 Fox, Anthony C. J. 2 Åman Pohjola, Johannes 2 Arthan, Rob D. 2 Ho, Son Lam 2 Sandberg Ericsson, Adam 1 Åman, Pohjola Johannes 1 Guéneau, Armaël 1 Heule, Marijn J. H. 1 Kanabar, Hrutvik 1 Mullen, Eric 1 Pałka, Michał H. 1 Rostedt, Henrik 1 Tatlock, Zachary 1 Tuerk, Thomas Serials 4 Journal of Automated Reasoning 2 Journal of Functional Programming 1 Science of Computer Programming 1 Lecture Notes in Computer Science Fields 28 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 21 Publications have been cited 131 times in 86 Documents Cited by ▼ Year ▼ Cakeml, a verified implementation of ML. Zbl 1284.68405Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott 39 2014 Proof-producing translation of higher-order logic into pure and stateful ML. Zbl 1297.68053Myreen, Magnus O.; Owens, Scott 11 2014 HOL with definitions: semantics, soundness, and a verified implementation. Zbl 1416.68167Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott 10 2014 Hoare logic for realistically modelled machine code. Zbl 1186.68118Myreen, Magnus O.; Gordon, Michael J. C. 8 2007 A trustworthy monadic formalization of the ARMv7 instruction set architecture. Zbl 1291.68341Fox, Anthony; Myreen, Magnus O. 8 2010 Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation. Zbl 1356.68194Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott 8 2016 Verified characteristic formulae for CakeML. Zbl 1485.68030Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael 6 2017 Verified just-in-time compiler on x86. Zbl 1312.68046Myreen, Magnus O. 5 2010 A verified runtime for a verified theorem prover. Zbl 1342.68297Myreen, Magnus O.; Davis, Jared 5 2011 The verified CakeML compiler backend. Zbl 1493.68091Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael 5 2019 The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1356.68186Davis, Jared; Myreen, Magnus O. 5 2015 Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions. Zbl 1468.68060Ho, Son; Abrahamsson, Oskar; Kumar, Ramana; Myreen, Magnus O.; Tan, Yong Kiam; Norrish, Michael 4 2018 A verified generational garbage collector for CakeML. Zbl 1468.68065Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes 3 2017 The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1416.68174Myreen, Magnus O.; Davis, Jared 3 2014 Transforming programs into recursive functions. Zbl 1347.68304Myreen, Magnus O.; Gordon, Michael J. C. 3 2009 cake_lpr: verified propagation redundancy checking in CakeML. Zbl 1474.68194Tan, Yong Kiam; Heule, Marijn J. H.; Myreen, Magnus O. 2 2021 Steps towards verified implementations of HOL Light. Zbl 1317.68225Myreen, Magnus O.; Owens, Scott; Kumar, Ramana 2 2013 Software verification with ITPs should use binary code extraction to reduce the TCB (short paper). Zbl 06946990Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O. 1 2018 Hoare logic for ARM machine code. Zbl 1141.68373Myreen, Magnus O.; Fox, Anthony C. J.; Gordon, Michael J. C. 1 2007 Proof-producing synthesis of ML from higher-order logic. Zbl 1291.68364Myreen, Magnus O.; Owens, Scott 1 2012 Separation logic adapted for proofs by rewriting. Zbl 1291.68363Myreen, Magnus O. 1 2010 cake_lpr: verified propagation redundancy checking in CakeML. Zbl 1474.68194Tan, Yong Kiam; Heule, Marijn J. H.; Myreen, Magnus O. 2 2021 The verified CakeML compiler backend. Zbl 1493.68091Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael 5 2019 Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions. Zbl 1468.68060Ho, Son; Abrahamsson, Oskar; Kumar, Ramana; Myreen, Magnus O.; Tan, Yong Kiam; Norrish, Michael 4 2018 Software verification with ITPs should use binary code extraction to reduce the TCB (short paper). Zbl 06946990Kumar, Ramana; Mullen, Eric; Tatlock, Zachary; Myreen, Magnus O. 1 2018 Verified characteristic formulae for CakeML. Zbl 1485.68030Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael 6 2017 A verified generational garbage collector for CakeML. Zbl 1468.68065Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes 3 2017 Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation. Zbl 1356.68194Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott 8 2016 The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1356.68186Davis, Jared; Myreen, Magnus O. 5 2015 Cakeml, a verified implementation of ML. Zbl 1284.68405Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott 39 2014 Proof-producing translation of higher-order logic into pure and stateful ML. Zbl 1297.68053Myreen, Magnus O.; Owens, Scott 11 2014 HOL with definitions: semantics, soundness, and a verified implementation. Zbl 1416.68167Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott 10 2014 The reflective Milawa theorem prover is sound (down to the machine code that runs it). Zbl 1416.68174Myreen, Magnus O.; Davis, Jared 3 2014 Steps towards verified implementations of HOL Light. Zbl 1317.68225Myreen, Magnus O.; Owens, Scott; Kumar, Ramana 2 2013 Proof-producing synthesis of ML from higher-order logic. Zbl 1291.68364Myreen, Magnus O.; Owens, Scott 1 2012 A verified runtime for a verified theorem prover. Zbl 1342.68297Myreen, Magnus O.; Davis, Jared 5 2011 A trustworthy monadic formalization of the ARMv7 instruction set architecture. Zbl 1291.68341Fox, Anthony; Myreen, Magnus O. 8 2010 Verified just-in-time compiler on x86. Zbl 1312.68046Myreen, Magnus O. 5 2010 Separation logic adapted for proofs by rewriting. Zbl 1291.68363Myreen, Magnus O. 1 2010 Transforming programs into recursive functions. Zbl 1347.68304Myreen, Magnus O.; Gordon, Michael J. C. 3 2009 Hoare logic for realistically modelled machine code. Zbl 1186.68118Myreen, Magnus O.; Gordon, Michael J. C. 8 2007 Hoare logic for ARM machine code. Zbl 1141.68373Myreen, Magnus O.; Fox, Anthony C. J.; Gordon, Michael J. C. 1 2007 all cited Publications top 5 cited Publications all top 5 Cited by 200 Authors 10 Myreen, Magnus O. 6 Nipkow, Tobias 4 Kumar, Ramana 4 Murray, Toby 4 Norrish, Michael 4 Popescu, Andrei 4 Schlichtkrull, Anders 3 Heule, Marijn J. H. 3 Kaliszyk, Cezary 3 Keller, Gabriele Cornelia 3 Klein, Gerwin 3 Lammich, Peter 3 Owens, Scott 3 Pichardie, David 3 Rizkallah, Christine 3 Sutcliffe, Geoff 3 Tan, Yong Kiam 2 Adams, Mark 2 Arthan, Rob D. 2 Bauereiß, Thomas 2 Blazy, Sandrine 2 Bohrer, Brandon 2 Chen, Zilin 2 Davis, Jared 2 Fox, Anthony C. J. 2 Gauthier, Thibault 2 Immler, Fabian 2 Kunčar, Ondřej 2 O’Connor, Liam 2 Pesenti Gritti, Armando 2 Raimondi, Franco 2 Roßkopf, Simon 2 Sewell, Thomas D. 2 Slind, Konrad 2 Urban, Josef 2 Wang, Yuting 2 Wenzel, Makarius 1 Abdulaziz, Mohammad 1 Abel, Andreas M. 1 Abrahamsson, Oskar 1 Allais, Guillaume 1 Åman Pohjola, Johannes 1 Åman, Pohjola Johannes 1 Amani, Sidney 1 Annenkov, Danil 1 Appel, Andrew W. 1 Back, Ralph-Johan 1 Baek, Seulkee 1 Bauer, Gertrud 1 Bengtson, Jesper 1 Bérard, Béatrice 1 Beringer, Lennart 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 Bryant, Randal E. 1 Bundy, Alan 1 Cachera, David 1 Cao, Qinxiang 1 Chakravarty, Manuel M. T. 1 Charguéraud, Arthur 1 Chlipala, Adam J. 1 Christensen, Michael F. 1 Cohen, Joshua 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 Dodds, Josiah 1 Dong, JinSong 1 Engelhardt, Kai 1 Eriksson, Johannes 1 Ernst, Gidon 1 Fava, Daniel Schnetzer 1 Forster, Yannick 1 Gandhi, Rajeev 1 Gengelbach, Arve 1 Giacobazzi, Roberto 1 Gordon, Michael J. C. 1 Gross, Jason 1 Grov, Gudmund 1 Grütter, Samuel 1 Guéneau, Armaël 1 Hales, Thomas Callister 1 Hameer, Aliya 1 Hardekopf, Ben 1 Hayes, Ian J. 1 Ho, Son Lam 1 Hoa, Koh Chuen ...and 100 more Authors all top 5 Cited in 14 Serials 21 Journal of Automated Reasoning 7 Journal of Functional Programming 3 AI Communications 3 Journal of Logical and Algebraic Methods in Programming 2 Theoretical Computer Science 2 Formal Aspects of Computing 2 Mathematics in Computer Science 1 Information Processing Letters 1 Science of Computer Programming 1 Journal of Symbolic Computation 1 Formal Methods in System Design 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning 1 Forum of Mathematics, Pi all top 5 Cited in 9 Fields 86 Computer science (68-XX) 18 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) 1 History and biography (01-XX) 1 Ordinary differential equations (34-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Convex and discrete geometry (52-XX) 1 Numerical analysis (65-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year