Publications by Scott Owens

Compiler Verification

• CakeML: A Verified Implementation of ML
  Ramana Kumar, Magnus O. Myreen, Scott Owens, Michael Norrish
  POPL 2014  (bibtex)

Multi-core Memory Models

• 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)
• 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)
• 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
• 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)
• 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)

Mechanised Semantics

• 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
• Ott or Nott
  Stephanie Weirich, Scott Owens, Peter Sewell, Francesco Zappa Nardelli
  WMM 2010  (bibtex)
• 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)
• 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)

Theorem Proving

• Proof-producing translation of higher-order logic into pure and stateful ML
  Magnus O. Myreen, Scott Owens
  JFP  (bibtex)
• Steps Towards Verified Implementations of HOL Light
  Magnus O. Myreen, Scott Owens, Ramana Kumar
  ITP 2013 ("Rough Diamond" section)  (bibtex)  (definitive version)
• Proof-Producing Synthesis of ML from Higher-Order Logic
  Magnus O. Myreen, Scott Owens
  ICFP 2012  (bibtex)  (author's local version)
• 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)
• 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)
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
  Guodong Li, Scott Owens, Konrad Slind
  ESOP 2007  (bibtex)  (definitive 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)
• 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)
• Proving as Programming with DrHOL: A Preliminary Design
  Scott Owens, Konrad Slind
  UITP 2003  (bibtex)

Module Systems

• Compile-time Information in Software Components
  Scott Owens
  PhD thesis  (bibtex)
• From Structures and Functors to Modules and Units
  Scott Owens, Matthew Flatt
  ICFP 2006  (bibtex)  (author's local version)
• Syntactic Abstraction in Component Interfaces
  Ryan Culpepper, Scott Owens, Matthew Flatt
  GPCE 2005  (bibtex)  (definitive version)

Compiler Front-ends

• Regular-expression Derivatives Re-examined
  Scott Owens, John Reppy, Aaron Turon
  JFP, 19(2), March 2009  (bibtex)  (definitive version)
• Lexer and Parser Generators in Scheme
  Scott Owens, Matthew Flatt, Olin Shivers, Benjamin McMullan
  Scheme Workshop 2004  (bibtex)

Validate XHTML 1.0 Strict Validate CSS