Author of the publication

A Better x86 Memory Model: x86-TSO.

, , and . TPHOLs, volume 5674 of Lecture Notes in Computer Science, page 391-407. Springer, (2009)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Syntactic Abstraction in Component Interfaces., , and . GPCE, volume 3676 of Lecture Notes in Computer Science, page 373-388. Springer, (2005)Characterising renaming within OCaml's module system: theory and implementation., , , and . PLDI, page 950-965. ACM, (2019)Compiling Higher Order Logic by Proof., , and . Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, (2010)Deformable Volumes in Path Planning Applications., , , and . ICRA, page 2290-2295. IEEE, (2000)Steps towards Verified Implementations of HOL Light., , and . ITP, volume 7998 of Lecture Notes in Computer Science, page 490-495. Springer, (2013)Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation., , , and . J. Autom. Reason., 56 (3): 221-259 (2016)Synchronising C/C++ and POWER., , , , , , , and . PLDI, page 311-322. ACM, (2012)Lem: reusable engineering of real-world semantics., , , , and . ICFP, page 175-188. ACM, (2014)Verifying efficient function calls in CakeML., , , , and . Proc. ACM Program. Lang., 1 (ICFP): 18:1-18:27 (2017)Proof-producing translation of higher-order logic into pure and stateful ML., and . J. Funct. Program., 24 (2-3): 284-315 (2014)