Scott Owens

Publication Activity (10 Years)

Years Active: 2000-2023
Publications (10 Years): 14

Top Topics

Theorem Proving

Higher Order Logic

Nested Transactions

Argumentation Semantics

Top Venues

Proc. ACM Program. Lang.

J. Funct. Program.

Publications

Thomas Sewell, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar, Alexander Mihajlovic, Oskar Abrahamsson, Scott Owens
Cakes That Bake Cakes: Dynamic Computation in CakeML. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, Mark Batty
Modular Relaxed Dependencies in Weak Memory Concurrency. ESOP (2020)
Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson, Scott Owens
Rotor: a tool for renaming values in OCaml's module system. IWOR@ICSE (2019)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
The verified CakeML compiler backend. J. Funct. Program. 29 (2019)
Scott Owens
Building trustworthy software with CakeML. FTfJP@ECOOP (2019)
Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson, Scott Owens
Characterising renaming within OCaml's module system: theory and implementation. PLDI (2019)
Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, Son Ho
Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. VSTTE (2018)
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan
Verifying efficient function calls in CakeML. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
A new verified compiler backend for CakeML. ICFP (2016)
Carl G. Ritson, Scott Owens
Benchmarking weak memory models. PPOPP (2016)
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation. J. Autom. Reason. 56 (3) (2016)
Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan
Functional Big-Step Semantics. ESOP (2016)
David S. Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens
A High-Assurance, High-Performance Hardware-Based Cross-Domain System. SAFECOMP (2016)
Yong Kiam Tan, Scott Owens, Ramana Kumar
A verified type system for CakeML. IFL (2015)
Magnus O. Myreen, Scott Owens
Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24 (2-3) (2014)
Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, Peter Sewell
Lem: reusable engineering of real-world semantics. ICFP (2014)
Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens
CakeML: a verified implementation of ML. POPL (2014)
Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens
HOL with Definitions: Semantics, Soundness, and a Verified Implementation. ITP (2014)
Magnus O. Myreen, Scott Owens, Ramana Kumar
Steps towards Verified Implementations of HOL Light. ITP (2013)
Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams
Synchronising C/C++ and POWER. PLDI (2012)
Magnus O. Myreen, Scott Owens
Proof-producing synthesis of ML from higher-order logic. ICFP (2012)
Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell
Clarifying and compiling C/C++ concurrency: from C++11 to POWER. POPL (2012)
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams
An Axiomatic Memory Model for POWER Multiprocessors. CAV (2012)
Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar
Nitpicking C++ concurrency. PPDP (2011)
Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell
Lem: A Lightweight Tool for Heavyweight Semantics. ITP (2011)
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
Mathematizing C++ concurrency. POPL (2011)
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53 (7) (2010)
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa
Ott: Effective tool support for the working semanticist. J. Funct. Program. 20 (1) (2010)
Scott Owens
Reasoning about the Implementation of Concurrency Abstractions on x86-TSO. ECOOP (2010)
Scott Owens, Susmit Sarkar, Peter Sewell
A Better x86 Memory Model: x86-TSO. TPHOLs (2009)
Scott Owens, John H. Reppy, Aaron Turon
Regular-expression derivatives re-examined. J. Funct. Program. 19 (2) (2009)
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave
The semantics of x86-CC multiprocessor machine code. POPL (2009)
Scott Owens
A Sound Semantics for OCamllight. ESOP (2008)
Scott Owens, Konrad Slind
Adapting functional programs to higher order logic. High. Order Symb. Comput. 21 (4) (2008)
Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon
Proof producing synthesis of arithmetic and cryptographic hardware. Formal Aspects Comput. 19 (3) (2007)
Guodong Li, Scott Owens, Konrad Slind
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. ESOP (2007)
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa
Ott: effective tool support for the working semanticist. ICFP (2007)
Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind
Automatic Formal Synthesis of Hardware from Higher Order Logic. Electron. Notes Theor. Comput. Sci. 145 (2006)
Scott Owens, Matthew Flatt
From structures and functors to modules and units. ICFP (2006)
Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang
Functional Correctness Proofs of Encryption Algorithms. LPAR (2005)
Ryan Culpepper, Scott Owens, Matthew Flatt
Syntactic Abstraction in Component Interfaces. GPCE (2005)
Elliot Anshelevich, Scott Owens, Florent Lamiraux, Lydia E. Kavraki
Deformable Volumes in Path Planning Applications. ICRA (2000)