Invited Talks and Technical Presentations

  1. A Foundation for Dependently Typed Haskell
    WG 2.8, Lake Placid, NY, July 19, 2016.

  2. Depending on Types
    Typelevel Summit, Philadelphia, PA, March 2-3, 2016.

  3. Dynamic Typing in GHC
    Compose :: Conference, Brooklyn, NY, February 4-5, 2016.

  4. Visible Type Application.
    Microsoft Research, Cambridge, UK, November 6, 2015.

  5. Visible Type Application.
    University of Kent, November 5, 2015.

  6. Depending on Types.
    Code Mesh 2015, London, November 4, 2015.

  7. From System F to Typed Assembly Language, by Morrisett, Walker, Crary, Glew.
    Papers We Love, Philadelphia. Philadelphia, PA, October 6, 2015

  8. Towards Dependently Typed Haskell
    WG 2.8, Kefalonia, Greece, May 24, 2015

  9. Pi-Forall: How to use and implement a dependently-typed language.
    Technical Keynote, Compose Conference. New York, January 30, 2015

  10. Programming up-to Congruence
    ACM Symposium on Principles of Programming Languages (POPL '15). Mumbai, India, January 16, 2015

  11. Depending on Types.
    Computer Science Colloquium Series, Indiana University. Bloomington, Indiana, October 17, 2014

  12. Programming Languages Panel.
    Cornell CS 50th Anniversary Symposium. Ithaca, New York, October 2, 2014

  13. Depending on Types.
    Keynote address, International Conference on Functional Programming (ICFP). Gothenburg, Sweden, September 3, 2014

  14. Programming Up-to Congruence, Again.
    WG 2.8, Estes Park, Colorado, August 12, 2014

  15. Combining Proofs and Programs.
    Certification of High-level and Low-level programs. Paris, France, July 7, 2014

  16. Why You Should Care About Dependent Types.
    Programming Languages Mentoring Workshop. San Diego, CA, January 21, 2014

  17. Programming Up-to Congruence.
    WG 2.8, Aussios, France, October 14, 2013

  18. The Pleasure and Pain of Advanced Type Systems.
    Invited speaker, Facebook Faculty Summit. Menlo Park, CA, August 6, 2013

  19. Paradoxical Typecase.
    WG 2.8, Anapolis, MD, November 7, 2012

  20. A POPLmark Retrospective: Using Proof Assistants in Programming Language Research.
    Invited speaker, LFMTP 2012: 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, Copenhagen, Denmark, September 9, 2012

  21. Dependently-typed programming in GHC.
    Invited speaker, FLOPS 2012: Eleventh International Symposium on Functional and Logic Programming, Kobe, Japan, May 25, 2012

  22. Binders Unbound.
    The 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012 Tokyo Japan, September 21, 2011

  23. Combining Proofs and Programs.
    Dependently Typed Programming, Shonan Seminar 007, Shonan Village, Japan, September 16, 2011

  24. 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

  25. Combining Proofs and Programs in Trellys.
    Plenary Address, MFPS 27. Pittsburgh, PA. May 26, 2011

  26. Generic Binding and Telescopes.
    WG 2.8, Marble Falls, TX. March 11, 2011

  27. Generative Type Abstraction and Type-level Computation.
    ACM Symposium on Principles of Programming Languages (POPL '11). Austin, TX, January 2011

  28. ICFP 2010 Program Chair's Report.
    Baltimore, MD. September 27, 2010

  29. Dependent Types and Program Equivalence.
    University of Strathclyde. Glasgow, Scotland. April 30, 2010

  30. Generic Programming with Dependent Types.
    IFIP 2.11, St. Andrews, Scotland. March 1-3, 2010

  31. Dependent Types and Program Equivalence.
    University of Nottingham. Nottingham, England. February 5, 2010

  32. Trellys Status Report.
    PLPV Discussion. Madrid, Spain. January 19, 2010

  33. A POPLmark Retrospective: Using Proof Assistants in Programming Language Research.
    University of Cambridge Computer Laboratory Wednesday Seminars. Cambridge, England. December 2, 2009

  34. Dependent Types and Program Equivalence.
    Semantics Lunch, University of Cambridge Computer Laboratory. Cambridge, England. November 2, 2009

  35. Haskell Symposium 2009 Program Chair's report.
    Edinburgh, Scotland. September 3, 2009

  36. Doing Dependent Types Wrong Without Going Wrong.
    IFIP WG 2.8, Frauenchiemsee, Germany, June 2009

  37. Adventures in Dependently-Typed Metatheory.
    IFIP WG 2.11, Mountain View CA. April 15, 2009

  38. Engineering Formal Metatheory
    Computer Science Colloquium, City University of New York Graduate Center. New York, NY. February 2, 2009

  39. First-class Polymorphism for Haskell.
    IFIP WG 2.8, Park City, UT. June 19, 2008

  40. Engineering Formal Metatheory.
    Princeton University, Princeton NJ, USA. November 19, 2007

  41. Machine Assistance for Programming Language Research.
    Cornell University, Ithaca, NY, USA. October 12, 2007

  42. Formal Reasoning About Programs and Programming Languages.
    National Security Agency. Fort Meade, MD, USA.
    July 20, 2007

  43. Engineering Aspects of Formal Metatheory.
    Harvard University, Boston MA, USA. June 1, 2007

  44. Dependently-Typed Languages.
    Working session summary. IFIP WG 2.11, Portland, OR, October 2006

  45. Simple Unification-Based Type Inference for GADTs.
    International Conference on Functional Programming (ICFP). Portland, OR. September 2006

  46. RepLib: A Library for Derivable Type Classes.
    Haskell Workshop. Portland, OR. September 2006

  47. Parametricity and GADTs.
    IFIP Working Group 2.8 (Functional Programming). Boston, MA. July 2006

  48. Practical Type Inference for Advanced Type Systems.
    International Federation for Information Processing (IFIP) Working Group 2.11, Dagstuhl, Wadern, Germany. January 2006

  49. Boxy Types: Inference for Higher-rank Types and Impredicativity.
    International Federation for Information Processing (IFIP) Working Group 2.8, Kalvi Manor, Estonia. October 2005

  50. A Core Language for Generalised Algebraic Datatypes.
    International Federation for Information Processing (IFIP) Working Group 2.8, West Point, USA. November 2004

  51. A Design for Type-directed Java.
    Programming Languages Seminar, Yale University, New Haven, CT. October 1, 2004

  52. 2004 ICFP Programming Contest Results.
    (Presented jointly with Benjamin Pierce and Steve Zdancewic) International Conference on Functional Programming, Snowbird, UT. September 20, 2004

  53. A Core Language for Generalised Algebraic Datatypes.
    Dagstuhl Seminar 04381: Dependently Typed Programming, Wadern, Germany. September 12, 2004

  54. A Design for Type-Directed Java.
    Microsoft Research Lab, Cambridge, UK. August 31, 2004

  55. A Design for Type-Directed Java.
    Workshop on Object-Oriented Developments (WOOD '04). London, UK, August 2004

  56. Unifying Nominal and Structural Ad-hoc Polymorphism.
    International Federation for Information Processing (IFIP) Working Group 2.8, Coffs Harbour, Australia. January 2003

  57. Unifying Nominal and Structural Ad-hoc Polymorphism.
    Computer Science Colloquium, City University of New York Graduate Center. New York, NY. October 30, 2003

  58. Boxes Go Bananas: Parametric Higher-Order Abstract Syntax in System F.
    Laboratory for Secure Systems Seminar, Stevens Institute of Technology. Hoboken, NJ. May 5, 2003

  59. Run-time type analysis in Haskell with an Awful Lot of Newtypes.
    International Federation for Information Processing (IFIP) Working Group 2.8, Crans-Montana, Switzerland. January 2003

  60. Polytypic Programming and Intensional Type Analysis.
    New Jersey Programming Languages Seminar. University of Pennsylvania, Philadelphia, PA. September 20, 2002

  61. Programming with Types.
    OHSU/Oregon Graduate Institute, Beaverton, OR. February 11, 2002

  62. Programming with Types.
    University of Oregon, Eugene, OR. February 15, 2002

  63. Programming with Types.
    University of Pennsylvania, Philadelphia, PA. February 19, 2002

  64. Programming with Types.
    University of Virginia, Charlottesville, VA. February 28, 2002

  65. Programming with Types.
    University of Maryland, College Park, MD. March 4, 2002

  66. Programming with Types.
    Northeastern University, Boston, MA. March 13, 2002

  67. Programming with Types.
    University of California, San Diego, CA. March 15, 2002

  68. Programming with Types.
    Purdue University, West Lafayette, IN. March 25, 2002

  69. Programming with Types.
    University of Michigan, Ann Arbor, MI. March 27, 2002

  70. Programming with Types.
    University of Texas, Austin, TX. April 2, 2002

  71. Higher-order Intensional Type Analysis.
    European Symposium on Programming (ESOP '02). Grenoble, France, April 2002

  72. Programming with Types.
    University of Colorado at Boulder, CO. April 16, 2002

  73. Programming with Types.
    Pennsylvania State University, State College, PA. April 19, 2002

  74. Programming with Types.
    Massachusetts Institute of Technology, Boston, MA. April 25, 2002

  75. Programming with Types.
    Rice University, Houston TX. April 29, 2002

  76. Run-Time Type Analysis and Program Verification.
    Research, Careers and Computer Science: A Maryland Symposium. University of Maryland, College Park, MD. November 2001

  77. Polytypic Programming and Intensional Type Constructor Analysis.
    International Federation for Information Processing (IFIP) Working Group 2.8, Are, Sweden. April 2001

  78. Encoding Intensional Type Analysis.
    European Symposium on Programming (ESOP '01). Genova, Italy. April 2001

  79. Resource Bound Certification. Harvard University, Boston, MA. February 2001

  80. Functional Pearl: Type-Safe Cast. International Conference on Functional Programming. Montreal, Canada. September 2000

  81. Resource Bound Certification. IBM Research, Hawthorne, NY. June 2000

  82. Resource Bound Certification. ACM Symposium on Principles of Programming Languages (POPL '00). Boston, MA, USA. January 2000

  83. Flexible Type Analysis.
    International Conference on Functional Programming (ICFP '99). Paris, France, September 1999

  84. Type Analysis and Typed Compilation.
    Princeton University, Princeton, NJ. June 1999

  85. Intensional Polymorphism in Type-Erasure Semantics.
    International conference on Functional Programming (ICFP '98). Baltimore, MD, USA, September 1998