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

• 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)  (definitive version)
• Mathematizing C++ Concurrency
  Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
  POPL 2011  (bibtex)  (definitive 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)  (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)  (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)
• From Structures and Functors to Modules and Units
  Scott Owens, Matthew Flatt
  ICFP 2006  (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)
• Deformable Volumes in Path Planning Applications
  Elliot Anshelevich, Scott Owens, Florent Lamiraux, Lydia E. Kavraki
  ICRA 2000  (bibtex)

PhD Thesis

• Compile-time Information in Software Components
  Scott Owens
  PhD thesis  (bibtex)

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

• Mathematizing C++ Concurrency: The Post-Rapperswil Model
  Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
  Technical report  (bibtex)
• A Better x86 Memory Model: x86-TSO (Extended Version)
  Scott Owens, Susmit Sarkar, Peter Sewell
  Technical report  (bibtex)

Validate XHTML 1.0 Strict Validate CSS