Robert Dockins
Contact Info
Computer Science Department
35 Olden Street
Princeton NJ, 08540
Phone: x1794
Office: 215
E-Mail:
rdockins AT princeton DOT edu
I am currently a fifth-year PhD student in
Computer Science at
Princeton. I am interested
in programming languages, formal logics and proof methods
for reasoning about programs.
I am currently seeking employment. Please see my CV
if you are interested in hiring a researcher in programming languages.
I was recently inducted into the
Siebel Scholar Class of 2012!
Siebel scholarships are awarded annually
by the Siebel Foundation
for academic excellence and demonstrated leadership to 85 top students from the world's leading graduate schools.
Academic Service
Publications
- Time Bounds for General Function Pointers. Robert Dockins and Aquinas Hobor.
To appear in Mathematical Foundations of Prgramming Semantics (MFPS XXVIII), 2012.
- A List-machine Benchmark for Mechanized Metatheory.
Andrew W. Appel, Robert Dockins and Xavier Leroy.
Journal of Automated Reasoning.
Accepted for publication.
- A Logical Mix of Approximation and Separation
Invited tutoral/paper in
APLAS 2010, November 2010.
- A Theory of Indirection via Approximation
Aquinas Hobor, Robert Dockins and Andrew W. Appel.
In
POPL 2010: The
37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, January 2010.
- A Fresh Look at Separation Algrbras
and Share Accounting Robert Dockins, Aquinas Hobor, and Andrew W. Appel.
In the 7th Asian Symposium on
Programming Languages and Systems, December 2009.
- Comparing Semantic and Syntactic Methods in
Mechanized Proof Frameworks C.J. Bell, Robert Dockins,
Aquinas Hobor, Andrew W. Appel, David Walker. Workshop paper.
In
2nd International Workshop on Proof-Carrying Code (PCC). June 2008.
- Multimodal Separation Logic for Reasoning
about Operational Semantics Robert Dockins, Andrew W. Appel and Aquinas Hobor.
In Proc.
Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics.
ENTCS, Volume 218. Pages 5-20. October 2008. Elsevier.
- Bytecode Verification for Haskell.
Robert Dockins and Samuel Z. Guyer. Workshop paper.
The Eighth Symposium on
Trends in Functional Programming (TFP). April 2007.
[Slides]
- Bytecode Verification for Haskell
(extended version). Robert Dockins and Samuel Z. Guyer. Technical Report,
Tufts University Department of Computer Science.
TR-2007-2.
Teaching
Spring 2011
I was an assistant instructor for
COS 333: Advanced Programming Techniques.
Spring 2009
I was the preceptor for sections P01A and P03 of
COS 126: General Computer Science.
Fall 2008
I was the assistant instructor (AI) for
COS 441: Programming Languages.
Software
I maintain a number of open-source projects, which you can find
on this website. These programs and libraries are written
in the language Haskell.
Haskell is, among other things, strongly typed and purely functional.
- Edison, a library of purely-functional
datastructures for Haskell
- Shellac, a framework for creating
REPL shells in Haskell
- The Lambda Shell, a shell for
evaluating terms of the pure, untyped lambda calculus, and
exemplar for creating shells using Shellac
In addition to the maintained projects above, I have a number of
other unmaintained projects that people may nonetheless find interesting.
Links
The Programming Languages and Security group at Princeton