Thomas D. Sewell

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
Candle: a verified implementation of HOL Light (extended version) Journal of Automated Reasoning	2026-02-06	Paper
Candle: a verified implementation of HOL light	2024-07-15	Paper
Cogent: uniqueness types and certifying compilation Journal of Functional Programming	2021-12-27	Paper
Multiscale simulation of the responses of discrete nanostructures to extreme loading conditions based on the material point method Computer Methods in Applied Mechanics and Engineering	2019-05-15	Paper
Refinement through restraint: bringing down the cost of verification Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming	2017-05-10	Paper
A framework for the automatic formal verification of refinement from \textsc{Cogent} to C Interactive Theorem Proving	2016-10-27	Paper
Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL Certified Programs and Proofs	2011-11-22	Paper
seL4 enforces integrity Interactive Theorem Proving	2011-08-17	Paper
Secure Microkernels, State Monads and Scalable Refinement Lecture Notes in Computer Science	2008-12-04	Paper
Constituent properties of HMX needed for mesoscale simulations Combustion Theory and Modelling	2002-12-03	Paper

Research outcomes over time

This page was built for person: Thomas D. Sewell