Keynotes

  1. What Have We Learned about Dependently Typed Programming from Haskell?. Keynote presentation at Haskell Symposium. Indianapolis, USA. August 29, 2026.

  2. Functional / Logic Programming in Verse. Keynote presentation at LOPSTR+PPDP. Indianapolis, USA. August 27, 2026.

  3. Tracking how dependently-typed functions use their arguments. LICS/ICALP/FSCD Joint Invited Speaker. Talinn, Estonia. 10 July, 2024.

  4. What are Dependent Types and What are they Good for? Milner lecture, Laboratory for Computer Science, Edinburgh. June 15, 2022.

  5. How to implement the Lambda Calculus, Quickly. Keynote presentations at IFL, The 33rd Symposium on Implementation and Application of Functional Languages. September 3, 2021.

  6. A Dependently-Typed Core Calculus for GHC. TYPES 2019 Conference Invited speaker. Oslo, Norway. June 2019.

  7. The Influence of Dependent Types. Keynote address, ACM Symposium on Principles of Programming Languages (POPL ’17) Paris, France, January 2017.

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

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

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

Conference talks, Seminars, and other Technical presentations

  1. Tracking how dependently-typed functions use their arguments. MPI-SWS, Saarbr"ucken, Germany. September 18, 2026.

  2. Well-scoped de Bruijn expressions in Dependent Haskell. University of Bristol. July 15, 2026.

  3. Tracking how dependently-typed functions use their arguments. EPFL, Lausanne, Switzerland. May 5, 2026.

  4. Tracking how dependently-typed functions use their arguments. CHoCoLa Seminar. Lyon, France. April 2, 2026.

  5. Tracking how dependently-typed functions use their arguments. Cambium team. Inria Paris, France. March 13, 2026.

  6. Commuting Conversions and CBPV. IFIP WG 2.8. Viana do Castelo, Portugal. March 2, 2026.

  7. Tracking how dependently-typed functions use their arguments. PPS Seminar. Institut de Recherche en Informatique Fondamentale (IRIF). Paris, France. February 26, 2026.

  8. Tracking how dependently-typed functions use their arguments. Epicure team, INRIA. Rennes, France. February 10, 2026.

  9. Tracking how dependently-typed functions use their arguments. Galinette team, INRIA. Nantes, France. February 6, 2026.

  10. Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach. POPL 2026, Rennes, France. January 16, 2026.

  11. A tale of four lambda calculus interpreters. WG 2.8 Meeting, York, Maine. May 2025.

  12. Tracking how dependently-typed functions use their arguments. Chalmers Department Seminar, Gothenberg, Sweden. 7 March 2025.

  13. CBPV+effects, CBPV+coeffects. WG 2.11 Meeting, Drexel University, Philadelphia, PA. March 2024.

  14. CBPV+effects, CBPV+coeffects. WG 2.8 Meeting, Pembroke College, Cambridge UK. April 2023.

  15. Stratified Type Theory, WG 2.8 Meeting, Pembroke College, Cambridge UK. April 2023.

  16. A Dependent Dependency Calculus. Ediburgh LFCS Seminar, June 14, 2022.

  17. Programming Language Design: From Grace Hopper to Today. ENIAC Day: 75th anniversary of ENIAC mini-symposium. February 15, 2021.

  18. Strongly-Typed System F in GHC. Chalmers Functional Programming Seminar Series. June 2020.

  19. Adventures in Quantitative Type Theory. IFIP WG 2.8 Meeting, Zion National Park. March 2020.

  20. A Dependently-Typed Core Calculus for GHC. PurPL Fest invited speaker. Purdue University. West Lafayette, IN. September 23, 2019.

  21. Strongly-typed System F in GHC. IFIP WG 2.8, Bordeaux, Fr. May 2019.

  22. Dependent Types in Haskell. Cornell CS Colloquium, Ithaca, NY. November 2018.

  23. Work-in-progress: Towards a formal semantics for GHC Core. DeepSpec 2018 Workshop, Philadelphia, PA. June 2018.

  24. Work-in-progress: Verifying the Glasgow Haskell Compiler Core language. IFIP WG 2.8, Asilomar, CA. June 2018.

  25. Work-in-progress: Verifying the Glasgow Haskell Compiler Core language. Dagstuhl Seminar 18201, “Secure Compilation” Wadern, Germany, May, 2018.

  26. Locally Nameless at Scale. Joint presentation with Anastasiya Kravchuck-Kirilyuk. CoqPL workshop, Los Angeles, CA. January 2018.

  27. Dependent Types in Haskell. University of Washington, PLSE Seminar Series, Seattle, WA, December 2017.

  28. Dependent Types in Haskell. McMaster University Departmental Seminar, Hamilton Ontario, November 2017.

  29. Eta-equivalence in Core Dependent Haskell. WG 2.8, Edinburgh, UK. June 2017.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  48. ICFP 2010 Program Chair’s Report. Baltimore, MD. September 27, 2010

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

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

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

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

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

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

  55. Haskell Symposium 2009 Program Chair’s report. Edinburgh, Scotland. September 3, 2009

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Industry Presentations

  1. TBA. Lambda World. Malaga, Spain. October 29-30, 2026.

  2. How to implement the Lambda Calculus, Quickly. Haskell Love, virtual developer conference. September 10, 2021.

  3. Strongly-Typed System F in GHC. YOW! Lambda Jam Online 2020. July 2020.

  4. Dependent Types in Haskell. BOBkonf invited speaker (research track). Berlin, Germany. August 21, 2019.

  5. Dependent Types in Haskell. Haskell eXchange keynote, London, October 2018.

  6. Work-in-progress: Verifying the Glasgow Haskell Compiler Core language using the Coq proof assistant. Intel Labs, Hillsboro, OR. August 2018.

  7. Dependent Types in Haskell. Invited speaker, Comcast Labs Connect: Functional Programming. March 9, 2018.

  8. Dependent Types in Haskell. StrangeLoop 2017, St. Louis, MO, September 2017.

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

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

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

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

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

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

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

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