2024
Evaluating Frontier Models for Dangerous Capabilities.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
CoRR, 2024
Discovering Agents (Abstract Reprint).
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024
2023
Artif. Intell., September, 2023
Cakes That Bake Cakes: Dynamic Computation in CakeML.
Proc. ACM Program. Lang., 2023
Explaining grokking through circuit efficiency.
CoRR, 2023
Scaling Goal-based Exploration via Pruning Proto-goals.
CoRR, 2023
2022
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact).
Dagstuhl Artifacts Ser., 2022
Solving math word problems with process- and outcome-based feedback.
CoRR, 2022
Goal Misgeneralization: Why Correct Specifications Aren't Enough For Correct Goals.
CoRR, 2022
Safe Deep RL in 3D Environments using Human Feedback.
CoRR, 2022
Candle: A Verified Implementation of HOL Light.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022
Verified Compilation and Optimization of Floating-Point Programs in CakeML.
Proceedings of the 36th European Conference on Object-Oriented Programming, 2022
2021
Reward tampering problems and solutions in reinforcement learning: a causal influence diagram perspective.
Synth., 2021
TacticToe: Learning to Prove with Tactics.
J. Autom. Reason., 2021
Formal Methods for the Informal Engineer: Workshop Recommendations.
CoRR, 2021
2020
Proof-Producing Synthesis of CakeML from Monadic HOL Functions.
J. Autom. Reason., 2020
Avoiding Tampering Incentives in Deep RL via Decoupled Approval.
CoRR, 2020
REALab: An Embedded Perspective on Tampering.
CoRR, 2020
2019
The verified CakeML compiler backend.
J. Funct. Program., 2019
Verified compilation on a verified processor.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019
Modeling AGI Safety Frameworks with Causal Influence Diagrams.
Proceedings of the Workshop on Artificial Intelligence Safety 2019 co-located with the 28th International Joint Conference on Artificial Intelligence, 2019
2018
Learning to Prove with Tactics.
CoRR, 2018
Clocked Definitions in HOL.
CoRR, 2018
Verified Certificate Checking for Counting Votes.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018
Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB - (Short Paper).
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018
2017
Verifying efficient function calls in CakeML.
Proc. ACM Program. Lang., 2017
Verified Characteristic Formulae for CakeML.
Proceedings of the Programming Languages and Systems, 2017
Verified compilation of CakeML to multiple machine-code targets.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL.
Proceedings of the Automated Deduction - CADE 26, 2017
2016
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation.
J. Autom. Reason., 2016
A Proof Strategy Language and Proof Script Generation for Isabelle.
CoRR, 2016
A new verified compiler backend for CakeML.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016
Functional Big-Step Semantics.
Proceedings of the Programming Languages and Systems, 2016
2015
Pattern Matches in HOL: - A New Representation and Improved Code Generation.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015
Proof-Producing Reflection for HOL - With an Application to Model Polymorphism.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015
A verified type system for CakeML.
Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, 2015
2014
CakeML: a verified implementation of ML.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014
HOL with Definitions: Semantics, Soundness, and a Verified Implementation.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014
2013
Steps towards Verified Implementations of HOL Light.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013
2012
Standalone Tactics Using OpenTheory.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012
2011
Validating QBF Validity in HOL4.
Proceedings of the Interactive Theorem Proving - Second International Conference, 2011
Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study.
Proceedings of the Formal Methods for Industrial Critical Systems, 2011
2010
(Nominal) Unification by Recursive Descent with Triangular Substitutions.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010