I am currently a second-year PhD student in Computer Science at Princeton. I am interested in programming languages, formal logics and proof methods for reasoning about programs.

Teaching

Spring 2009 I am 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.

Publications

• Comparing Semantic and Syntactic Methods in Mechanized Proof Frameworks C.J. Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel, David Walker. To appear in the 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. To appear in Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics, May 2008.
• 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.