Publications by Scott Owens
return home
Sorted by [Reverse chronological | Venue type | Topic]
Journals
- x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen
CACM, 53(7), July 2010 (bibtex) (author's local version) - Ott: Effective Tool Support for the Working Semanticist
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa
JFP, 20(1), January 2010 (bibtex) (definitive version)
See also the Ott web page.
(Copyright Cambridge University Press) - Regular-expression Derivatives Re-examined
Scott Owens, John Reppy, Aaron Turon
JFP, 19(2), March 2009 (bibtex) (definitive version) - Adapting Functional Programs to Higher-Order Logic
Scott Owens, Konrad Slind
HOSC, 21(4), December 2008 (bibtex) (definitive version) - Proof Producing Synthesis of Arithmetic and Cryptographic Hardware
Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon
FAC, 19(3), August 2007 (bibtex) (definitive version)
Conferences
- An Axiomatic Memory Model for Power Multiprocessors
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo Martin, Peter Sewell
CAV 2012 (bibtex) - Synchronising C/C++ and POWER
Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams
PLDI 2012 (bibtex) - Clarifying and Compiling C/C++ Concurrency: From C++11 to POWER
Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell
POPL 2012 (bibtex) (author's local version) - Lem: A Lightweight Tool for Heavyweight Semantics
Scott Owens, Peter Boehm, Francesco Zappa Nardelli, Peter Sewell
ITP 2011 ("Rough Diamond" section) (bibtex) (definitive version)
Lem's homepage - Nitpicking C++ Concurrency
Jasmin Christian Blanchette, Tjark Weber, Mark Batty, Scott Owens, Susmit Sarkar
PPDP 2011 (bibtex) (author's local version) - Mathematizing C++ Concurrency
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
POPL 2011 (bibtex) (author's local version) - Reasoning about the Implementation of Concurrency Abstractions on x86-TSO
Scott Owens
ECOOP 2010 (bibtex) (definitive version)
Full proofs - A Better x86 Memory Model: x86-TSO
Scott Owens, Susmit Sarkar, Peter Sewell
TPHOLs 2009 (bibtex) (definitive version) - 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 (bibtex) (author's local version) - A Sound Semantics for OCaml light
Scott Owens
ESOP 2008 (bibtex) (definitive version) - Ott: Effective Tool Support for the Working Semanticist
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa
ICFP 2007 (bibtex) (author's local version) - Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
Guodong Li, Scott Owens, Konrad Slind
ESOP 2007 (bibtex) (definitive version) - From Structures and Functors to Modules and Units
Scott Owens, Matthew Flatt
ICFP 2006 (bibtex) (author's local version) - Functional Correctness Proofs of Encryption Algorithms
Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang
LPAR 2005 (bibtex) (definitive version) - Syntactic Abstraction in Component Interfaces
Ryan Culpepper, Scott Owens, Matthew Flatt
GPCE 2005 (bibtex) (definitive version) - Deformable Volumes in Path Planning Applications
Elliot Anshelevich, Scott Owens, Florent Lamiraux, Lydia E. Kavraki
ICRA 2000 (bibtex)
PhD Thesis
Book Chapters
- Compiling Higher Order Logic by Proof
Konrad Slind, Guodong Li, Scott Owens
Book chapter in Design and Verification of Microprocessor Systems for High-Assurance Applications (bibtex) (definitive version)
Workshops
- Ott or Nott
Stephanie Weirich, Scott Owens, Peter Sewell, Francesco Zappa Nardelli
WMM 2010 (bibtex) - Relaxed Memory Models Must Be Rigorous
Francesco Zappa Nardelli, Peter Sewell, Jaroslav Sevcik, Susmit Sarkar, Scott Owens, Luc Maranget, Mark Batty, Jade Alglave
EC2 2009 (bibtex) - Verifying Type Soundness for OCaml: The Core Language
Scott Owens, Gilles Peskine
WMM 2007 (bibtex) - Automatic Formal Synthesis of Hardware from Higher Order Logic
Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind
AVoCS 2005 (bibtex) (definitive version) - A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic
Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind
TPHOLs 2005, emerging trends (bibtex) - Lexer and Parser Generators in Scheme
Scott Owens, Matthew Flatt, Olin Shivers, Benjamin McMullan
Scheme Workshop 2004 (bibtex) - Proving as Programming with DrHOL: A Preliminary Design
Scott Owens, Konrad Slind
UITP 2003 (bibtex)
Technical Reports
Validate XHTML 1.0 Strict Validate CSS