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.

• Workshop on Syntax and Semantics of Low-Level Languages (LOLA) 2012: Program committee member

• 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.

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