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
University of Cambridge
The Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD

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

OCaml light
Supervision for Optimising Compilers

Research Groups: Cambridge Theory and Semantics Group PLT Scheme

Publications:

A Sound Semantics for OCaml light. Scott Owens. To appear at ESOP 2008.
Regular Expression Derivatives Reexamined. Scott Owens, John Reppy, and Aaron Turon. To appear in the Journal of Functional Programming.
Verifying type soundness in HOL for OCaml: the core language. Scott Owens and Gilles Peskine. Workshop on Mechanizing Metatheory 2007.
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. International Conference on Functional Programming 2007.
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. Guodong Li, Scott Owens, and Konrad Slind. European Symposium on Programming 2007.
From Structures and Functors to Modules and Units. Scott Owens and Matthew Flatt. International Conference on Functional Programming 2006.
Adapting Functional Programs to Higher-order Logic. Scott Owens and Konrad Slind. To appear in the journal of Higher-order and Symbolic Computation.
Functional Correctness Proofs of Encryption Algorithms. Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, and Junxing Zhang. Logic for Programming, Artificial Intellegence, and Reasoning 2005.
Automatic Formal Synthesis of Hardware from Higher Order Logic. Mike Gordon, Juliano Iyoda, Scott Owens, and Konrad Slind. Automated Verification of Critical Systems 2005.
Syntactic Abstraction in Component Interfaces. Ryan Culpepper, Scott Owens, and Matthew Flatt. Generative Programming and Component Engineering 2005.
A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic. Mike Gordon, Juliano Iyoda, Scott Owens, and Konrad Slind. Theorem Proving in Higher Order Logics 2005, Emerging Trends.
Lexer and Parser Generators in Scheme. Scott Owens, Matthew Flatt, Olin Shivers, and Benjamin McMullan. Scheme Workshop 2004.
Proving as Programming with DrHOL: A Preliminary Design. Scott Owens and Konrad Slind. User Interfaces for Theorem Provers 2003.

Ph.D. dissertation:

Compile-time Information in Software Components

Software 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, Types, and Advanced Graphics
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