Supervisions: Specification and Verification 1
Research Group: Cambridge Programming, Logic, and Semantics Group
Previous research group: PLT Scheme
Current projects:
Publications:
- Reasoning about the Implementation of Concurrency Abstractions on x86-TSO
Scott Owens
Draft
- 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)
See also the Ott web page.
- A Better x86 Memory Model: x86-TSO
Scott Owens,
Susmit Sarkar, and
Peter Sewell
TPHOLs 2009
(bibtex)
See also the the accompanying tech. report and our project's homepage.
- Regular-expression Derivatives Re-examined
Scott Owens,
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)
See also our project's homepage.
- Adapting Functional Programs to Higher-order Logic
Scott Owens and
Konrad Slind
HOSC, 21(4), December 2008
(bibtex)
- A Sound Semantics for OCaml light
Scott Owens
ESOP 2008
(bibtex)
See also the OCaml light web page.
- 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 journal version (above) and 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.
- 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
(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 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:
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 Cambridge
- Part 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:
