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
- The Pleasure and Pain of Advanced Type
Systems, Facebook Faculty Summit, Menlo Park, CA.
August 2013.
- 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.
|