Work

Overall Interests

I am interested in programming languages, and more specifically in the use of type theory to develop language implementations that combine safety and efficiency. My most recent research has been on type systems for assembly language that can be used to enforce timing policies in untrusted code.

In the past and at other times, I have spent some time thinking about type-safe object-oriented language design and type-directed implementation strategies for object-oriented languages.

My updated curriculum vitae will be available soon.

Papers

(In approximate reverse chronological order.)

C. Joseph Vanderwaart. Static Enforcement of Timing Policies Using Code Certification. Ph.D. thesis, Carnegie Mellon University, August 2006. Available as CMU Technical Report CMU-CS-06-143.
Joseph C. Vanderwaart and Karl Crary. Automated and Certified Conformance to Responsiveness Policies. To appear in the proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), 2005. [ps.gz][pdf]
Joseph C. Vanderwaart and Karl Crary. Foundational Typed Assembly Language for Grid Computing. CMU Technical Report CMU-CS-04-104. [ps.gz][pdf]
Joseph C. Vanderwaart and Karl Crary. A Typed Interface for Garbage Collection. In the proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), 2003. [ps.gz][pdf]
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper and Perry Cheng. Typed Compilation of Recursive Datatypes. In the proceedings of TLDI, 2003. [ps.gz][pdf]
Extended version: CMU Technical Report CMU-CS-02-200, 2002. [ps.gz][pdf]
Karl Crary and Joseph C. Vanderwaart. An Expressive, Scalable Type Theory for Certified Code. In the proceedings of ICFP, 2002. [ps.gz][pdf]
Earlier version: CMU Technical Report CMU-CS-01-113, 2001. [ps.gz][pdf]
Joseph C. Vanderwaart and Karl Crary. A Simplified Account of the Metatheory of Linear LF. In the proceedings of the Third International Workshop on Logical Frameworks and Meta-Languages (LFM), 2002. [ps.gz]
Extended version: CMU Technical Report CMU-CS-01-154, 2002. [ps.gz][pdf]
Jonathan Moody, Ricardo Silva and Joseph Vanderwaart. Data filtering for automatic classification of rocks from reflectance spectra. In Proceedings of the 7th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, 2001. [pdf]
Kim B. Bruce and Joseph C. Vanderwaart. Semantics-Driven Language Design: Statically Type-Safe Virtual Types in Object-Oriented Languages. In MFPS XV, 1999. [ps.gz]

Talks

Certified Code for Grid Computing. Student research presentation at the CMU CS open house for prospective graduate students, March 19, 2005. [ppt]
Automated and Certified Conformance to Responsiveness Policies. TLDI '05 Workshop (see paper above). [ppt]
Certified Bounds on the Resource Usage of Untrusted Mobile Code. December 5, 2003. [ppt]
Foundational Typed Assembly Language for Grid Computing. Thesis Proposal. October 24, 2003. [ppt]
A Typed Interface for Garbage Collection. TLDI '03 Workshop (see paper above). [ppt]
Type Theories for Certified Code. Williams College Computer Science Colloquium. November 15, 2002. [ppt]

Postgraduate Work

My graduate work at Carnegie Mellon University focused on the development of type systems for certified code that allow the integration of proofs of complex program properties. This has involved excursions into the metatheory of the LF and Linear LF logical frameworks, and into the typing properties of the garbage collector/mutator interface in the TILT/ML runtime system. My Ph.D. thesis, completed in August 2006 (text online soon), concerns a type system for certifying conformance of programs to timing policies, with applications to resource control problems.

I was a member of the ConCert Project, the successor to the Fox Project.

Undergraduate Honors Thesis

In 1999 I finished an undergraduate honors thesis, advised by Prof. Kim Bruce of the Williams College Computer Science Department. My thesis was on the use of typed intermediate representations in the compilation of object-oriented programming languages, and involved the design and partial implementation of a compiler for Bruce's LOOM language. A revised version of the thesis is available for download in gzipped PostScript form.

Links

There is a list of Programming language theory texts online

Online indexes of CS literature: CiteSeer and DBLP.