Blog

• 2023

  • 2023-11-02: More Data Types with Negation at Fun in the REPL
  • 2023-01-17: Compiling higher-order specifications to SMT solvers
  • 2023-01-16: Simple semantics for defaults in Catala
  • 2023-01-15: Data types with Negation

• 2020

  • 2020-11-23: Slides and Video for “Resource Constrained Programming with Full Dependent Types”
  • 2020-08-13: Quantitative Typing with Non-idempotent Intersection Types
  • 2020-01-24: Slides for “Resource Constrained Programming with Full Dependent Types”

• 2016

  • 2016-10-10: Off the Beaten Track 2017: Call for Talk Proposals
  • 2016-04-12: Authenticated Data Structures, as a Library, for Free!
  • 2016-01-26: Slides and notes for my OBT “Generalising Abstraction” talk

• 2015

  • 2015-04-23: The Incremental λ-Calculus and Relational Parametricity
  • 2015-04-19: Slides for “An Algebraic Approach to Typechecking and Elaboration”
  • 2015-04-17: Propositions as Filenames, Builds as Proofs: The Essence of Make

• 2014

  • 2014-01-29: POPL Slides

• 2013

  • 2013-07-17: One Done, Two Submitted
  • 2013-03-29: Productive Coprogramming with Guarded Recursion

• 2012

  • 2012-11-07: Abstraction and Invariance for Algebraically Indexed Types
  • 2012-11-07: Theorems for Free
  • 2012-09-06: Interleaving Data and Effects
  • 2012-09-05: Relational Parametricity for Higher Kinds
  • 2012-01-06: Reasoning about Stream Processing with Effects

• 2011

  • 2011-12-14: A Type Checker that knows its Monad from its Elbow
  • 2011-11-14: How to be a Productive Programmer
  • 2011-04-28: On Structural Recursion II: Folds and Induction
  • 2011-04-22: On Structural Recursion