Tutorials
- Designing
Dependently-Typed Programming Languages. Oregon
Programming
Languages
Summer School: Types, Logic, and Verification,
Eugene OR, USA. July, 2013.
- Generic
Programming with
Dependent Types. Spring School
on Generic and Indexed
Programming. Oxford, England. March 24-26, 2010.
- Coq for Programming
Language Metatheory. Summer
School
on
Logic and Theorem Proving
in Programming Languages, Eugene OR, USA. July 22-25, 2008.
- Using Proof Assistants
for Programming Language Research or, How to write your Next
POPL paper in Coq. Tutorial
session at POPL, San Francisco, CA, USA. January 8, 2008.
Invited
Talks, Workshop and Conference Presentations
- A POPLmark retrospective:
Using proof assistants in programming language research.
Invited talk for LFMTP
2012. Copenhagen, Denmark, September 2012.
- Paradoxical Typecase. WG
2.8,
Anapolis,
MD, November 7, 2012.
- Dependently-typed
Programming in GHC. Invited Talk for Eleventh International
Symposium on Functional and Logic Programming (FLOPS 2012) Kobe,
Japan, May 25, 2012. (Red Black Tree code
from the talk.)
- Binders Unbound. ICFP 2011. Tokyo, Japan.
September 2011.
- Combining Proofs and
Programs. Dependently Typed Programming, Shonan Seminar 007,
Shonan Village, Japan, September 16, 2011.
- Combining Proofs and Programs. Joint invited
speaker for Rewriting
Techniques
and
Applications (RTA 2011) and Typed Lambda Calculi and
Applications (TLCA 2011). Novi Sad, Serbia, June 1, 2011.
- Combining Proofs and Programs in Trellys. Plenary
Address, MFPS
27. Pittsburgh, PA. May 26, 2011.
- Generic Binding and Telescopes. WG 2.8, Marble
Falls, TX. March 11, 2011.
- ICFP Program Chair's report, Baltimore, MD,
September 27, 2010.
- Dependent types and
program equivalence. University of
Strathclyde. Glasgow, Scotland. April 30, 2010.
- Generic Programming with Dependent Types.
IFIP
2.11,
St.
Andrews,
Scotland.
March
1-3,
2010.
- Dependent types and
program equivalence. University of Nottingham. Nottingham,
England. February 5, 2010.
- Trellys Status Report. PLPV
Discussion. Madrid, Spain. January 19, 2010.
- A POPLmark retrospective:
Using proof assistants in programming language research.
University of Cambridge Computer Laboratory Wednesday Seminars.
Cambridge, England.
December 2, 2009.
- Dependent types and
program equivalence. Semantics Lunch, University of
Cambridge
Computer Laboratory. Cambridge, England. 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.
- First-Class Polymorphism
for Haskell. IFIP WG 2.8, Park City, UT. June
19, 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.
|