Author of the publication

Steps towards Verified Implementations of HOL Light.

, , and . ITP, volume 7998 of Lecture Notes in Computer Science, page 490-495. Springer, (2013)

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)Deformable Volumes in Path Planning Applications., , , and . ICRA, page 2290-2295. IEEE, (2000)Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation., , , and . J. Autom. Reason., 56 (3): 221-259 (2016)Compiling Higher Order Logic by Proof., , and . Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, (2010)Steps towards Verified Implementations of HOL Light., , and . ITP, volume 7998 of Lecture Notes in Computer Science, page 490-495. Springer, (2013)Lem: reusable engineering of real-world semantics., , , , and . ICFP, page 175-188. ACM, (2014)Synchronising C/C++ and POWER., , , , , , , and . PLDI, page 311-322. ACM, (2012)Proof-producing translation of higher-order logic into pure and stateful ML., and . J. Funct. Program., 24 (2-3): 284-315 (2014)Verifying efficient function calls in CakeML., , , , and . Proc. ACM Program. Lang., 1 (ICFP): 18:1-18:27 (2017)