Scott Owens

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