Publications by Scott Owens

• Steps Towards Verified Implementations of HOL Light
  Magnus O. Myreen, Scott Owens, Ramana Kumar
  ITP 2013 ("Rough Diamond" section)  (bibtex)
• Proof-Producing Synthesis of ML from Higher-Order Logic
  Magnus O. Myreen, Scott Owens
  ICFP 2012  (bibtex)  (author's local version)
• 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  (bibtex)  (definitive version)
• Synchronising C/C++ and POWER
  Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams
  PLDI 2012  (bibtex)  (author's local version)
• 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)
• Ott or Nott
  Stephanie Weirich, Scott Owens, Peter Sewell, Francesco Zappa Nardelli
  WMM 2010  (bibtex)
• Mathematizing C++ Concurrency: The Post-Rapperswil Model
  Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
  Technical report  (bibtex)
• 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)
• Reasoning about the Implementation of Concurrency Abstractions on x86-TSO
  Scott Owens
  ECOOP 2010  (bibtex)  (definitive version)
  Full proofs
• 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)
• 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)
• A Better x86 Memory Model: x86-TSO
  Scott Owens, Susmit Sarkar, Peter Sewell
  TPHOLs 2009  (bibtex)  (definitive version)
• 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)
• A Better x86 Memory Model: x86-TSO (Extended Version)
  Scott Owens, Susmit Sarkar, Peter Sewell
  Technical report  (bibtex)
• Regular-expression Derivatives Re-examined
  Scott Owens, John Reppy, Aaron Turon
  JFP, 19(2), March 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)
• Adapting Functional Programs to Higher-Order Logic
  Scott Owens, Konrad Slind
  HOSC, 21(4), December 2008  (bibtex)  (definitive 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)
• Verifying Type Soundness for OCaml: The Core Language
  Scott Owens, Gilles Peskine
  WMM 2007  (bibtex)
• Proof Producing Synthesis of Arithmetic and Cryptographic Hardware
  Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon
  FAC, 19(3), August 2007  (bibtex)  (definitive version)
• Compile-time Information in Software Components
  Scott Owens
  PhD thesis  (bibtex)
• 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)
• Automatic Formal Synthesis of Hardware from Higher Order Logic
  Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind
  AVoCS 2005  (bibtex)  (definitive 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)
• 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)
• Deformable Volumes in Path Planning Applications
  Elliot Anshelevich, Scott Owens, Florent Lamiraux, Lydia E. Kavraki
  ICRA 2000  (bibtex)

Validate XHTML 1.0 Strict Validate CSS