default search action

combined dblp search
author search
venue search
publication search

ask others

Anthony C. J. Fox

> Home > Persons

Person information

affiliation: University of Cambridge, Department of Computer Science and Technology, UK
affiliation: Arm Lid., UK

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

Books and Theses

see FAQ

What is the meaning of the colors in the publication lists?

1999
[b1]
- view
  - electronic edition @ bl.uk
  - details & citations
- export record
  dblp key:
  - phd/ethos/Fox99
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/phd/ethos/Fox99
Anthony C. J. Fox:
Algebraic models for advanced microprocessors. Swansea University, UK, 1999

Journal Articles

see FAQ

What is the meaning of the colors in the publication lists?

2023
[j6]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/pacmpl/FoxSXBMPC23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/pacmpl/FoxSXBMPC23
Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong:
A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations. Proc. ACM Program. Lang. 7(OOPSLA1): 376-405 (2023)
2022
[j5]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/darts/BeckerRDMTKTF22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/darts/BeckerRDMTKTF22
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox:
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). Dagstuhl Artifacts Ser. 8(2): 10:1-10:2 (2022)
2019
[j4]
- view
  authority control:
- export record
  dblp key:
  - journals/jfp/TanMKFON19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jfp/TanMKFON19
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish:
The verified CakeML compiler backend. J. Funct. Program. 29: e2 (2019)
[j3]
- view
  authority control:
- export record
  dblp key:
  - journals/tc/WoodruffJXFNCDG19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/tc/WoodruffJXFNCDG19
Jonathan Woodruff, Alexandre Joannou, Hongyan Xia, Anthony C. J. Fox, Robert M. Norton, David Chisnall, Brooks Davis, Khilan Gudka, Nathaniel Wesley Filardo, A. Theodore Markettos, Michael Roe, Peter G. Neumann, Robert N. M. Watson, Simon W. Moore:
CHERI Concentrate: Practical Compressed Capabilities. IEEE Trans. Computers 68(10): 1455-1469 (2019)
2003
[j2]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jlp/FoxH03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jlp/FoxH03
Anthony C. J. Fox, Neal A. Harman:
Algebraic models of correctness for abstract pipelines. J. Log. Algebraic Methods Program. 57(1-2): 71-107 (2003)
2000
[j1]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/fac/FoxH00
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/fac/FoxH00
Anthony C. J. Fox, Neal A. Harman:
Algebraic Models of Correctness for Microprocessors. Formal Aspects Comput. 12(4): 298-312 (2000)

Conference and Workshop Papers

see FAQ

What is the meaning of the colors in the publication lists?

2022
[c18]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/ecoop/BeckerRDMTKTF22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/ecoop/BeckerRDMTKTF22
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox:
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP 2022: 1:1-1:28
[c17]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/itp/KanabarFM22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KanabarFM22
Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen:
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. ITP 2022: 20:1-20:22
2020
[c16]
- view
  authority control:
- export record
  dblp key:
  - conf/sp/NienhuisJBFR0NN20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sp/NienhuisJBFR0NN20
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:
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. SP 2020: 1003-1020
2019
[c15]
- view
  authority control:
- export record
  dblp key:
  - conf/pldi/LoowKTMNAF19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/pldi/LoowKTMNAF19
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox:
Verified compilation on a verified processor. PLDI 2019: 1041-1053
2018
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/BeckerZMDMF18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/BeckerZMDMF18
Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox:
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. FMCAD 2018: 1-10
2017
[c13]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FoxMTK17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FoxMTK17
Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar:
Verified compilation of CakeML to multiple machine-code targets. CPP 2017: 125-137
2016
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/icfp/TanMKFON16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/icfp/TanMKFON16
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish:
A new verified compiler backend for CakeML. ICFP 2016: 60-73
2015
[c11]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Fox15
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Fox15
Anthony C. J. Fox:
Improved Tool Support for Machine-Code Decompilation in HOL4. ITP 2015: 187-202
2012
[c10]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Fox12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Fox12
Anthony C. J. Fox:
Directions in ISA Specification. ITP 2012: 338-344
2011
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BohmeFSW11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BohmeFSW11
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber:
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. CPP 2011: 183-198
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/Fox11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Fox11
Anthony C. J. Fox:
LCF-Style Bit-Blasting in HOL4. ITP 2011: 357-362
2010
[c7]
- view
  authority control:
- export record
  dblp key:
  - conf/itp/FoxM10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/FoxM10
Anthony C. J. Fox, Magnus O. Myreen:
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. ITP 2010: 243-258
2009
[c6]
- view
  authority control:
- export record
  dblp key:
  - conf/popl/AlglaveFIMSSN09
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/popl/AlglaveFIMSSN09
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli:
The semantics of power and ARM multiprocessor machine code. DAMP 2009: 13-24
2007
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/fsen/MyreenFG07
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fsen/MyreenFG07
Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon:
Hoare Logic for ARM Machine Code. FSEN 2007: 272-286
2005
[c4]
- view
  authority control:
- export record
  dblp key:
  - conf/calco/Fox05
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/calco/Fox05
Anthony C. J. Fox:
An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL. CALCO 2005: 157-174
2003
[c3]
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Fox03
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Fox03
Anthony C. J. Fox:
Formal Specification and Verification of ARM6. TPHOLs 2003: 25-40
1998
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/nada/FoxH98
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/nada/FoxH98
Anthony C. J. Fox, Neal A. Harman:
Algebraic Models of Superscalar Microprocessor Implementations: A Case Study. Prospects for Hardware Foundations 1998: 138-183
1996
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/FoxH96
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/FoxH96
Anthony C. J. Fox, Neal A. Harman:
An Algebraic Model of Correctness for Superscalar Microprocessors. FMCAD 1996: 346-361

Parts in Books or Collections

see FAQ

What is the meaning of the colors in the publication lists?

2010
[p1]
- view
  authority control:
- export record
  dblp key:
  - books/sp/10/FoxGM10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/books/sp/10/FoxGM10
Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen:
Specification and Verification of ARM Hardware and Software. Design and Verification of Microprocessor Systems for High-Assurance Applications 2010: 221-247

Coauthor Index

see FAQ

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.