Author of the publication

Fast, Verified Computation for Candle.

, and . ITP, volume 268 of LIPIcs, page 4:1-4:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2023)

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

PureCake: A Verified Compiler for a Lazy Functional Language., , , , , , and . Proc. ACM Program. Lang., 7 (PLDI): 952-976 (2023)A verified proof checker for higher-order logic.. J. Log. Algebraic Methods Program., (2020)Candle: A Verified Implementation of HOL Light., , , and . ITP, volume 237 of LIPIcs, page 3:1-3:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2022)Proof-Producing Synthesis of CakeML from Monadic HOL Functions., , , , , , and . J. Autom. Reason., 64 (7): 1287-1306 (2020)Fast, Verified Computation for Candle., and . ITP, volume 268 of LIPIcs, page 4:1-4:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2023)Cakes That Bake Cakes: Dynamic Computation in CakeML., , , , , , and . Proc. ACM Program. Lang., 7 (PLDI): 1121-1144 (2023)Verified compilation on a verified processor., , , , , , and . PLDI, page 1041-1053. ACM, (2019)Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions., , , , , and . IJCAR, volume 10900 of Lecture Notes in Computer Science, page 646-662. Springer, (2018)Automatically Introducing Tail Recursion in CakeML., and . TFP, volume 10788 of Lecture Notes in Computer Science, page 118-134. Springer, (2017)