Invited
Talks and Conference Presentations
- Dependent types and
program equivalence. Semantics Lunch, University of Cambridge
Computer Laboratory. November 2, 2009.
- Doing dependent types
wrong without going wrong. IFIP WG 2.8, Frauenchiemsee, Germany,
June 2009.
- Adventures in
Dependently-Typed Metatheory. IFIP WG 2.11,
Mountain View CA. April 15, 2009.
- Engineering Formal
Metatheory. Computer Science Colloquium, City University of New
York
Graduate Center. New York, NY. February 2, 2009.
- Coq for Programming
Language Metatheory. Summer School on Logic and Theorem Proving
in Programming Languages, Eugene OR, USA. July 22-25, 2008.
- First-Class Polymorphism
for Haskell. IFIP WG 2.8, Park City, UT. June
19, 2008.
- Using Proof Assistants
for Programming Language Research or, How to write your Next
POPL paper in Coq.
Tutorial session, San Francisco, CA, USA. January 8, 2008.
- Engineering Formal
Metatheory. Princeton University, Princeton, NJ. November 19,
2007.
- Engineering Formal
Metatheory. Cornell University, Ithaca, NY. October 12. 2007.
- Formal Reasoning about
Programs and Programming Languages. NSA. Fort Meade, MD. June
20, 2007.
- Engineering Aspects of Formal Metatheory.
Harvard University. Boston, MA. June 1, 2007.
- Getting Started in PL
Design Research. CRA-W/CDC Programming Languages Summer School.
Austin, TX. May 10, 2007.
- Career Paths: How
to get started in Academia or Industry. CRA-W/CDC
Programming Languages Summer School. Austin, TX. May 10, 2007.
- Dependently-typed languages.
Working session summary. IFIP WG 2.11, Portland, OR, USA. October 28,
2006.
- Simple Unification-based Type Inference
for GADTs. ICFP, September 18, 2006.
- RepLib:
A Library for Derivable Type Classes. Haskell Workshop,
September 17, 2006.
- Parametricity and GADTs. IFIP
WG 2.8, Boston, MA, USA. July 19, 2006.
- Practical Type Inference
for Advanced Type Systems. IFIP WG 2.11, Dagstuhl,
Wadern,
Germany. January 2006.
- Boxy
types: Inference for higher-rank and impredicative polymorphism.
IFIP WG 2.8, Kalvi Manor, Estonia. October 2005.
- A Core Language for
Generalized Algebraic
Datatypes. IFIP WG 2.8, West Point, NY, USA. November 2004.
- A Design for Type-Directed Programming in
Java. Yale University. October 1, 2004.
- A Core Language for
Generalized
Algebraic Datatypes. Dagstuhl Seminar 04381: Dependently
Typed Programming, Oct 12, 2004.
- A Design for Type-Directed
Programming in
Java. Microsoft Research, Cambridge. August 31, 2004.
- A
Design for
Type-Directed Programming in
Java. WOOD '04.
- Nominal and
Structural Ad-hoc Polymorphism.
IFIP WG 2.8, Coffs Harbour, Australia. December 2003.
- Unifying Nominal and
Structural Ad-hoc
Polymorphism. Computer Science Colloquium. City University
of New York. October 30, 2003.
- Boxes Go Bananas: Parametric
Higher-Order
Abstract Syntax in System F. Stevens Institute of
Technology, Laboratory for Secure Systems Seminar. May 5, 2003.
- Run-time Type Analysis in
Haskell with an Awful Lot of Newtypes. IFIP WG 2.8,
Crans-Montana, Switzerland, January 2003.
- Polytypic
Programming and Intensional Type Analysis. New
Jersey Programming Languages Seminar. University of
Pennsylvania. September 20, 2002.
- Programming
with Types
- OHSU/Oregon
Graduate Institute, February 11, 2002.
- University
of Oregon, February 15, 2002.
- University
of Pennsylvania, February 19, 2002.
- University
of Virginia, February 28, 2002.
- University
of Maryland, March 4, 2002.
- Northeastern
University, March 13, 2002.
- University
of California, San Diego, March 15, 2002.
- Purdue
University, March 25, 2002.
- University
of Michigan, March 27, 2002.
- University
of Texas, April 2, 2002.
- University
of Colorado at Boulder, April 16, 2002.
- Pennsylvania
State University, April 19, 2002.
- Massachusetts
Institute of Technology, April 25, 2002.
- Rice
University, April 29, 2002.
- Higher-Order
Intensional Type Analysis. ESOP '02.
- Run-time
Type Analysis for Program Verification. "Research, Careers,
and Computer Science: A Maryland Symposium". University of Maryland,
November 16-17, 2001.
- Polytypic Programming and
Intensional Type (Constructor) Analysis. IFIP WG 2.8,
Åre, Sweden, April 2001.
- Encoding Intensional Type Analysis.
ESOP '01.
- Resource
Bound Certification. Harvard University, February
2001.
- Type-Safe Cast. ICFP '00.
- Resource
Bound Certification. IBM Research, June 2000.
- Resource
Bound Certification. POPL '00.
- Flexible
Type Analysis. ICFP '99.
- Type Analysis and Typed
Compilation. Princeton University, June 1999.
- Intensional
Polymorphism in Type Erasure Semantics. ICFP '98.
|