Talks

• Some tricks for making Agda code faster
  Talk/discussion at Agda Implementors' Meeting XXXII, 2020-06-01. ["slides"]
• Logical properties of a modality for erasure
  Talk given at meeting #79 of IFIP WG2.1, Otterlo, 2020-01-06. [pdf]
• Some theory about nothing
  Talk given at the Logic and Types division meeting, Aspenäs, 2019-09-21. [pdf]
• Up-to Techniques using Sized Types
  Talk given at POPL 2018, Los Angeles, 2018-01-11. [pdf, video]
• Up-to Techniques Using Sized Types
  Talk given at the Joint Stockholm–Göteborg type theory seminar, Göteborg, 2017-10-25. [pdf]
• Up-to Techniques Using Sized Types
  Talk given at meeting #76 of IFIP WG2.1, Lesbos, 2017-10-17. [pdf]
• Higher and/or dependent lenses
  Agda Implementors' Meeting XXII, Leuven, 2015–09–16. [pdf, accompanying code]
• Isomorphism is equality
  Talk given at meeting #73 of IFIP WG2.1, Lökeberg, 2015-08-25. [pdf]
• Nested induction and coinduction
  Docent lecture, 2014-06-13. (Slightly edited.) [abstract, pdf]
• Operational Semantics Using the Partiality Monad
  Talk given at Shonan Meeting 026: Coinduction for computation structures and programming languages, Shonan Village Center, 2013-10-08. [abstract, pdf]
• Correct-by-Construction Pretty-Printing
  Talk given at DTP 2013, Boston, MA, 2013-09-25. [pdf]
• Correct-by-Construction Pretty-Printing
  Talk given at meeting #70 of IFIP WG2.1, Schloss Reisensburg, 2013-07-04. (Slightly edited.) [abstract, pdf]
• Operational Semantics Using the Partiality Monad
  Talk given at ICFP 2012, København, 2012-09-10. [pdf, video]
• Bag Equivalence via a Proof-Relevant Membership Relation
  Talk given at ITP 2012, Princeton, 2012-08-14. [pdf]
• Calculating Bag Equalities
  Talk given at meeting #68 of IFIP WG2.1, Rome, 2012-02-06. (Slightly edited.) [abstract, pdf]
• Total Parser Combinators
  Talk given at ICFP 2010, Baltimore, 2010-09-29. (Slightly edited.) [pdf, video]
• Total Parser Combinators Using Mixed Induction and Coinduction
  Talk given at meeting #66 of IFIP WG2.1, Atlantic City, 2010-09-20. [abstract, pdf]
• Beating the Productivity Checker Using Embedded Languages
  Talk given at PAR 2010, Edinburgh, 2010-07-15. [pdf]
• Operational Semantics Using the Partiality Monad
  Talk given at DTP 2010, Edinburgh, 2010-07-09. [abstract, pdf, accompanying code]
• Subtyping, Declaratively
  An Exercise in Mixed Induction and Coinduction
  Talk given at MPC 2010, Lac-Beauport, Québec, 2010-06-23. [pdf]
• Operational Semantics Using the Partiality Monad
  Agda Implementors' Meeting XI, Awaji Yumebutai, 2010-03-24. (Slightly edited.) [abstract, pdf, accompanying code]
• Total Parser Combinators
  MGS Christmas Seminars 2009, Sheffield, 2009-12-15. For more information, see Total Parser Combinators. [abstract, pdf]
• Mixing Induction and Coinduction
  TYPES 2009, Aussois, 2009-05-15. For more information, see Total Parser Combinators and Subtyping, Declaratively. [abstract, pdf]
• Structurally Recursive Descent Parsing
  Logic and Semantics Seminar, Cambridge, 2009-03-20. [abstract, pdf]
• An ad-hoc and monolithic method for ensuring that corecursive definitions are productive
  Agda Intensive Meeting 9, Sendai, 2008-11-27. (Slightly edited.) For more information, see Beating the Productivity Checker Using Embedded Languages. [abstract, pdf, pdf (n-up)]
• Parsing Mixfix Operators
  IFL 2008, Hatfield, 2008-09-10. [pdf, pdf (n-up)]
• Improved handling of mixfix operators: Design and implementation
  Agda Implementors' Meeting 8, Göteborg, 2008-05-29. [pdf, pdf (n-up)]
• Structurally Recursive Descent Parsing
  Dependently Typed Programming 2008, Nottingham, 2008-02-18. [abstract, pdf, pdf (n-up)]
• Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures
  POPL 2008, San Francisco, 2008-01-10. (Slightly edited.) [pdf, pdf (n-up)]
• A Well-typed Interpreter for a Dependently Typed Language
  Fun in the Afternoon, Nottingham, 2007-02-21. [abstract, pdf, pdf (n-up)]
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
  Proglog meeting, 2007-01-31. Slides slightly edited. [abstract, pdf, pdf (n-up)]
• Fast and Loose Reasoning is Morally Correct
  POPL 2006, 2006-01-12. [pdf]
• Cover Summary
  Talk given for the Programatica group, 2005-03-18. [pdf]
• Chasing Bottoms, A Case Study in Program Verification in the Presence of Partial and Infinite Values
  MPC 2004, the Seventh International Conference on Mathematics of Program Construction, Stirling, UK, July 2004. [pdf, ps.gz (n-up)]
• Factoring is in BQP
  Algorithms Research Seminar, 2003-05-12. [abstract]
• Introduction to Quantum Computation
  Algorithms Research Seminar, 2003-04-28. [abstract, pdf]
• Matroids from Modules
  MFCSIT2002, the Second Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, National University of Ireland, Galway, July 2002. [pdf, ps.gz]