Anthony C. J. Fox
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
15
Venues
9
Active years
1996–2022
Best venue rank
A*
Where they publish
Papers
15 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2022 | ECOOP | Verified Compilation and Optimization of Floating-Point Programs in CakeML. | Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox |
| 2022 | ITP | Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. | Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen |
| 2020 | SP | Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. | Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell |
| 2019 | PLDI | Verified compilation on a verified processor. | Andreas Lw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox |
| 2018 | FMCAD | A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. | Heiko Becker, Nikita Zyuzin, Raphal Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox |
| 2017 | CPP | Verified compilation of CakeML to multiple machine-code targets. | Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar |
| 2016 | ICFP | A new verified compiler backend for CakeML. | Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish |
| 2015 | ITP | Improved Tool Support for Machine-Code Decompilation in HOL4. | Anthony C. J. Fox |
| 2012 | ITP | Directions in ISA Specification. | Anthony C. J. Fox |
| 2011 | CPP | Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. | Sascha Bhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber |
| 2011 | ITP | LCF-Style Bit-Blasting in HOL4. | Anthony C. J. Fox |
| 2010 | ITP | A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. | Anthony C. J. Fox, Magnus O. Myreen |
| 2009 | POPL | The semantics of power and ARM multiprocessor machine code. | Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli |
| 2005 | CALCO | An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL. | Anthony C. J. Fox |
| 1996 | FMCAD | An Algebraic Model of Correctness for Superscalar Microprocessors. | Anthony C. J. Fox, Neal A. Harman |