Deformable Volumes in Path Planning Applications. - Elliot Anshelevich; Scott Owens; Florent Lamiraux; Lydia E. Kavraki (ICRA, 2000)

Syntactic Abstraction in Component Interfaces. - Ryan Culpepper; Scott Owens; Matthew Flatt (GPCE, 2005)

Functional Correctness Proofs of Encryption Algorithms. - Jianjun Duan; Joe Hurd; Guodong Li; Scott Owens; Konrad Slind; Junxing Zhang (LPAR, 2005)

Automatic Formal Synthesis of Hardware from Higher Order Logic. - Mike Gordon; Juliano Iyoda; Scott Owens; Konrad Slind (AVoCS, 2005)

From structures and functors to modules and units. - Scott Owens; Matthew Flatt (ICFP, 2006)

Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. - Guodong Li; Scott Owens; Konrad Slind (ESOP, 2007)

Proof producing synthesis of arithmetic and cryptographic hardware. - Konrad Slind; Scott Owens; Juliano Iyoda; Mike Gordon (Formal Aspects Comput., 2007)

Compile-Time Information in Software Components. - Scott Owens (2007)

A Sound Semantics for OCamllight. - Scott Owens (ESOP, 2008)

Adapting functional programs to higher order logic. - Scott Owens; Konrad Slind (High. Order Symb. Comput., 2008)

The semantics of x86-CC multiprocessor machine code. - Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli; Scott Owens; Tom Ridge; Thomas Braibant; Magnus O. Myreen; Jade Alglave (POPL, 2009)

A Better x86 Memory Model: x86-TSO. - Scott Owens; Susmit Sarkar; Peter Sewell (TPHOLs, 2009)

Regular-expression derivatives re-examined. - Scott Owens; John H. Reppy; Aaron Turon (J. Funct. Program., 2009)

Compiling Higher Order Logic by Proof. - Konrad Slind; Guodong Li; Scott Owens (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. - Scott Owens (ECOOP, 2010)

x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. - Peter Sewell; Susmit Sarkar; Scott Owens; Francesco Zappa Nardelli; Magnus O. Myreen (Commun. ACM, 2010)

Ott: Effective tool support for the working semanticist. - Peter Sewell; Francesco Zappa Nardelli; Scott Owens; Gilles Peskine; Thomas Ridge; Susmit Sarkar; Rok Strnisa (J. Funct. Program., 2010)

Lem: A Lightweight Tool for Heavyweight Semantics. - Scott Owens; Peter Böhm; Francesco Zappa Nardelli; Peter Sewell (ITP, 2011)

Mathematizing C++ concurrency. - Mark Batty; Scott Owens; Susmit Sarkar; Peter Sewell; Tjark Weber (POPL, 2011)

Nitpicking C++ concurrency. - Jasmin Christian Blanchette; Tjark Weber; Mark Batty; Scott Owens; Susmit Sarkar (PPDP, 2011)

An Axiomatic Memory Model for POWER Multiprocessors. - Sela Mador-Haim; Luc Maranget; Susmit Sarkar; Kayvan Memarian; Jade Alglave; Scott Owens; Rajeev Alur; Milo M. K. Martin; Peter Sewell; Derek Williams (CAV, 2012)

Proof-producing synthesis of ML from higher-order logic. - Magnus O. Myreen; Scott Owens (ICFP, 2012)

Synchronising C/C++ and POWER. - Susmit Sarkar; Kayvan Memarian; Scott Owens; Mark Batty; Peter Sewell; Luc Maranget; Jade Alglave; Derek Williams (PLDI, 2012)

Clarifying and compiling C/C++ concurrency: from C++11 to POWER. - Mark Batty; Kayvan Memarian; Scott Owens; Susmit Sarkar; Peter Sewell (POPL, 2012)

Steps towards Verified Implementations of HOL Light. - Magnus O. Myreen; Scott Owens; Ramana Kumar (ITP, 2013)

Lem: reusable engineering of real-world semantics. - Dominic P. Mulligan; Scott Owens; Kathryn E. Gray; Tom Ridge; Peter Sewell (ICFP, 2014)

HOL with Definitions: Semantics, Soundness, and a Verified Implementation. - Ramana Kumar; Rob Arthan; Magnus O. Myreen; Scott Owens (ITP, 2014)

CakeML: a verified implementation of ML. - Ramana Kumar; Magnus O. Myreen; Michael Norrish; Scott Owens (POPL, 2014)

Proof-producing translation of higher-order logic into pure and stateful ML. - Magnus O. Myreen; Scott Owens (J. Funct. Program., 2014)

A verified type system for CakeML. - Yong Kiam Tan; Scott Owens; Ramana Kumar (IFL, 2015)

Functional Big-Step Semantics. - Scott Owens; Magnus O. Myreen; Ramana Kumar; Yong Kiam Tan (ESOP, 2016)

A new verified compiler backend for CakeML. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (ICFP, 2016)

Benchmarking weak memory models. - Carl G. Ritson; Scott Owens (PPoPP, 2016)

A High-Assurance, High-Performance Hardware-Based Cross-Domain System. - David S. Hardin; Konrad Slind; Mark Bortz; James Potts; Scott Owens (SAFECOMP, 2016)

Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. - Ramana Kumar; Rob Arthan; Magnus O. Myreen; Scott Owens (J. Autom. Reason., 2016)

Verifying efficient function calls in CakeML. - Scott Owens; Michael Norrish; Ramana Kumar; Magnus O. Myreen; Yong Kiam Tan (Proc. ACM Program. Lang., 2017)

Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. - Hugo Férée; Johannes Åman Pohjola; Ramana Kumar; Scott Owens; Magnus O. Myreen; Son Ho (VSTTE, 2018)

Building trustworthy software with CakeML. - Scott Owens (FTfJP@ECOOP, 2019)

Rotor: a tool for renaming values in OCaml's module system. - Reuben N. S. Rowe; Hugo Férée; Simon J. Thompson; Scott Owens (IWOR@ICSE, 2019)

Characterising renaming within OCaml's module system: theory and implementation. - Reuben N. S. Rowe; Hugo Férée; Simon J. Thompson; Scott Owens (PLDI, 2019)

The verified CakeML compiler backend. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (J. Funct. Program., 2019)

Modular Relaxed Dependencies in Weak Memory Concurrency. - Marco Paviotti; Simon Cooksey; Anouk Paradis; Daniel Wright 001; Scott Owens; Mark Batty (ESOP, 2020)

Cakes That Bake Cakes: Dynamic Computation in CakeML. - Thomas Sewell; Magnus O. Myreen; Yong Kiam Tan; Ramana Kumar; Alexander Mihajlovic; Oskar Abrahamsson; Scott Owens (Proc. ACM Program. Lang., 2023)