Deprecated : The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Publications by Scott Owens
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 SlindHOSC , 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 OwensECOOP 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 OwensESOP 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 SlindESOP 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 ApplicationsElliot 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 SlindAVoCS 2005 (bibtex ) (definitive version )A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic Mike Gordon , Juliano Iyoda , Scott Owens, Konrad SlindTPHOLs 2005, emerging trends (bibtex )Lexer and Parser Generators in Scheme Scott Owens, Matthew Flatt , Olin Shivers , Benjamin McMullanScheme Workshop 2004 (bibtex )Proving as Programming with DrHOL: A Preliminary Design Scott Owens, Konrad SlindUITP 2003 (bibtex )Technical Reports Validate XHTML 1.0 Strict Validate CSS