Projects:

• Vellvm: Verified LLVM
• WPE II: Memory Models and Implementations for Shared-memory Multi-threaded Programming Languages.
• Relational Parametricity for Linear System F^o.
• The mechanized proof of an algorithmic Linear System F^o.
• Dependent Types and Program Equivalence - Lambda-eek.
• The mechanized proof of Softbound+CETS with a technical report.
• Encoding DCC into System F. (Under construction)
• Coq libs of Parametricity in System F.
• Security-Oriented Languages.

Reading:

• Compiler Verification
• Type and Effect Systems
• Logical Relations

TA:

• CIS341 - Compilers (Spring 2011)
• CIS551 - Computer and Network Security (Spring 2008, Spring 2009)

Contact:

• firstname at figure out the domain name