Scott Owens' Homepage

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

Scott Owens

Research Associate, Computer Laboratory, University of Cambridge

e-mail: Scott.Owens@cl.cam.ac.uk

Picture of me

Research Group: Cambridge Programming, Logic, and Semantics Group
Previous research group: PLT Scheme

Current projects:

Publications:

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)
See also our project's homepage.

A Sound Semantics for OCaml light
Scott Owens
ESOP 2008 (bibtex)
See also the OCaml light web page.

Regular-expression Derivatives Re-examined
Scott Owens, John Reppy, and Aaron Turon
JFP, 19(2), March 2009 (bibtex) (Copyright Cambridge University Press)

Verifying type soundness in HOL for OCaml: the core language.
Scott Owens and Gilles Peskine
Workshop on Mechanizing Metatheory 2007 (bibtex)
See also the ESOP 2008 publication, 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)
See also the Ott web page.

Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
Guodong Li, Scott Owens, and Konrad Slind
ESOP 2007 (bibtex)

From Structures and Functors to Modules and Units
Scott Owens and Matthew Flatt
ICFP 2006 (bibtex)
See also chapters 2 and 3 of my PhD thesis.

Adapting Functional Programs to Higher-order Logic
Scott Owens and Konrad Slind
HOSC, 21(4), December 2008 (bibtex)

Functional Correctness Proofs of Encryption Algorithms
Jianjun Duan, 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 Slind
AVoCS 2005

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 Slind
TPHOLs 2005, Emerging Trends (bibtex)

Lexer and Parser Generators in Scheme
Scott Owens, Matthew Flatt, Olin Shivers, and Benjamin McMullan
Scheme Workshop 2004 (bibtex)

Proving as Programming with DrHOL: A Preliminary Design
Scott Owens and Konrad Slind
UITP 2003 (bibtex)

Ph.D. dissertation:

Compile-time Information in Software Components
(bibtex)

Past projects:

OpenGL bindings for PLT Scheme
Lexer and parser generators for PLT Scheme
On-the-fly syntax coloring for DrScheme
Compilation manager for PLT Scheme
GNU Multi Precision library support for PLT Scheme
Verification of AES in HOL-4
A model checker and BDD library in PLT Scheme, for teaching model checking.

Teaching:

Supervisor for Semantics of Programming Languages (Computer Science, part IB) and Advanced Graphics, Optimising Compilers, Specification and Verification II, and Types (Computer Science, part II) at the University of Cambridge.
TeachScheme!
Introduction to Java
TA for Programming Languages, fall 2002

Biography:

Education:
Ph.D. in Computer Science, University of Utah, May 2007
B.S. in Computer Science and B.A. in Mathematics, Rice University, May 2000
Leisure: Cambridge Go Society
Senior Member of Wolfson College