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 Scott Owens' Homepage
Workshop on Modules and Libraries for Proof Assistants
Supervisions: Specification and Verification 1 and
Specification and Verification 2
Research group: Cambridge Programming, Logic, and Semantics Group PLT Scheme
Publications:
Reasoning about the Implementation of Concurrency Abstractions on x86-TSO ECOOP 2010
(bibtex )Full proofs
Ott: Effective Tool Support for the Working Semanticist Peter Sewell ,
Francesco Zappa Nardelli ,
Scott Owens,
Gilles Peskine ,
Thomas Ridge ,
Susmit Sarkar , and
Rok Strniša JFP , 20(1), January 2010
(bibtex ) (Copyright Cambridge University Press)Ott web page .
A Better x86 Memory Model: x86-TSO Susmit Sarkar , and
Peter Sewell TPHOLs 2009
(bibtex )the accompanying tech. report and our project's homepage .
Regular-expression Derivatives Re-examined John Reppy , and
Aaron Turon JFP , 19(2), March 2009
(bibtex ) (Copyright Cambridge University Press)
The Semantics of x86-CC Multiprocessor Machine Code Susmit Sarkar ,
Peter Sewell ,
Francesco Zappa Nardelli ,
Scott Owens,
Tom Ridge ,
Thomas Braibant ,
Magnus O. Myreen , and
Jade Alglave POPL 2009
(bibtex )our project's homepage .
Adapting Functional Programs to Higher-order Logic HOSC , 21(4), December 2008
(bibtex )
A Sound Semantics for OCaml light ESOP 2008
(bibtex )the OCaml light web page .
Verifying type soundness in HOL for OCaml: the core language. Gilles Peskine Workshop on Mechanizing Metatheory 2007
(bibtex )A Sound Semantics for OCaml light and the OCaml light web page .
Ott: Effective Tool Support for the Working Semanticist Peter Sewell ,
Francesco Zappa Nardelli ,
Scott Owens,
Gilles Peskine ,
Thomas Ridge ,
Susmit Sarkar , and
Rok Strniša ICFP 2007
(bibtex )Ott web page .
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic ESOP 2007
(bibtex )
From Structures and Functors to Modules and Units Matthew Flatt ICFP 2006
(bibtex )PhD thesis .
Functional Correctness Proofs of Encryption Algorithms Joe Hurd ,
Guodong Li,
Scott Owens,
Konrad Slind, and
Junxing Zhang LPAR 2005
(bibtex )
Automatic Formal Synthesis of Hardware from Higher Order Logic Mike Gordon ,
Juliano Iyoda ,
Scott Owens, and
Konrad SlindAVoCS 2005
(bibtex )
Syntactic Abstraction in Component Interfaces Ryan Culpepper ,
Scott Owens, and
Matthew Flatt GPCE 2005
(bibtex )
A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic Mike Gordon ,
Juliano Iyoda ,
Scott Owens, and
Konrad SlindTPHOLs 2005 , Emerging Trends
(bibtex )
Lexer and Parser Generators in Scheme Matthew Flatt ,
Olin Shivers , and
Benjamin McMullanScheme Workshop 2004
(bibtex )
Proving as Programming with DrHOL: A Preliminary Design UITP 2003
(bibtex )
Ph.D. dissertation:
Teaching:
Supervisor for Semantics of Programming Languages (Computer Science, part IB) and Advanced Graphics, Optimising Compilers, Specification and Verification I and II, and Types (Computer Science, part II) at the University of CambridgePart II project supervisor at the University of Cambridge, 2008-2010
TeachScheme! Introduction to Java, University of Utah, Summer 2003
TA for Programming Languages , fall 2002
PLT Scheme programming:
OpenGL bindings
Lexer and parser generators
On-the-fly syntax coloring for DrScheme
Compilation manager
GNU Multi Precision library support
A model checker and BDD library in PLT Scheme, for teaching model checking.
HOL programming:
Personal: