Recent Talks

• Homotopy Type Theory without Homotopy Theory
  Foundations of Mathematics for Computer Aided Formalisation (FOMCAF13), Padova, Januray 2013
• Homotopy Type Theory in 10 minutes
  Research Away Day, School for Computer Science, Nottingham, September 2012
• A syntactical approach to weak ω-groupoids
  Computer Science Logic 2012, International Conference, Fontainebleau, France, September 2012
• Towards an ω-groupoid model of Type Theory
  Workshop on Higher Dimensional Algebra, Categories and Types(HDACT12), invited talk, Lubljana, Slovenia, June 2012
• Weak ω-Groupoids in Type Theory
  Applied and Computational Category Theory (ACCAT12), invited talk, Tallinn, Estonia; April 2012
• What is the problem with Induction-Recursion?
  Symposium on occasion of Peter Hancock's 60th birthday, Glasgow, December 2011
• To Infinity, and Beyond: From Setoids to Weak ω-Categories
  Theory Days, Tõrve, Estonia; October 2011
• Why dependent types matter
  12th Symposium on Programming Languages and Software Tools, Tallinn, Estonia, October 2011; invited talk.
• The case of the smart case
  Shonan seminar on Dependently Typed Programming, Shonan, Japan, October 2011
• To Infinity, and Beyond: From Setoids to Weak ω-Categories
  FP lab Away Day, July 2011
• Towards higher dimensional Type Theory
  Jointly with Thierry Coquand. Presented at AIM XIII, Gothenburg, April 2011
• A short history of equality
  Presented at Fun in the Afternoon, Birmingham, March 2011
• Termination Checking in the Presence of Nested Inductive and Coinductive Types
  Presented at PAR10 at FLOCS 2010 in Edinburgh, July 2010
• Higher Order Containers
  Invited talk at the special session on Proof Theory and Computation, CIE 2010, Ponta Delgada, Azores, Portugal, July 2010
• Mixing induction and coinduction in Agda,
  (Agda source) May 2010, Institute of Cybernetics, Tallinn
• Monads Need Not Be Endofunctors
  May 2010, ScotCats, Edinburgh
• ΠΣ: Dependent Types without the Sugar
  Talk at Fun in the Afternoon, November 2009, Microsoft Cambridge
• Normalisation by Completeness
  Invited Talk given at NBE 09 in Los Angeles, August 2009
• PiSigma a core language for dependently typed programming
  Talk given at Types 09 in Aussois, May 2009
• Quantum Computing
  Talk given at the MSc seminar in Leicester, February 2009
• Containers
  Talk given at the Fun in the afternoon in Hertfordshire, May 2008
• A Core Language For Dependently Typed Programming
  joint work with Nicolas Oury
  Talk given at the the Types meeting in Torino, March 2008
• Towards Type Theory with Continuity
  Talk given at the Russell 08 workshop in Swansea, March 2008
• Is Intuitionistic Logic relevant for Computer Science?
  Talk given at the OASIS seminar in Oxford, February 2008
• Why dependent types matter
  Talk given at the TYPES workshop on Dependently Typed Programming, Nottingham, February 2008
• The Beauty and the Beast: A Happy End?
  Talk given at the TYPES workshop on Effects in Type Theory in Tallinn, December 2007
• Observational Equality, now!
  Talk given at the PLPV workshop in Freiburg, October 2007
• Extensionality now!
  Talk given at the Types meeting in Cividale, May 2007
• Indexed Container
  Talk given at the Institute of Cybernetics in Tallinn, April 2007
• How not to prove strong normalisation
  Talk given at BCTCS in Oxford, April 2007
• Functional Quantum Programming
  Talk given at the QICS meeting in Oxford, March 2007
• Isomorphisms for context-free types
  based on joint work with Wouter Swierstra
  Talk given at the FOP Away day in Nottingham, January 2007
• The Quantum IO Monad
  based on joint work with Alexaner Green
  Talk given at the QNET meeting / Qdays III in Glasgow, December 2006
• Beauty in the Beast - Functional specifications of effects
  based on joint work with Wouter Swierstra
  Talk given at the Logic and Semantics Seminar, Cambridge, June 2006
• Should Extensional Type Theory be considered harmful?
  Talk given at the Workshop on Trends in Constructive Mathematics, Kloster Frauenwoerth, June 2006
• Stop thinking about bottoms when writing programs
  Talk given at the British Colloqium for Theoretical Computer Science (BCTCS 06), Swansea, April 2006
• An Algebra of Pure Quantum Programming
  based on joint work with Jon Grattage, Amr Sabry and Juliana Vizzotto
  Talk given at the Quoxic meeting, Oxford, November 2005
• Isomorphisms on inductive types
  based on joint work with Wouter Swierstra
  Talk given at the Second International Workshop on Isomorphisms of Types in Toulouse, France, October 2005
• Dependent Container
  based on joint work with Neil Ghani, Peter Hancock and Peter Morris
  Talk given at the APPSEM 2005 meeting at Frauenchiemsee, Germany, September 2005
• Is Constructive Logic Relevant for Computer Science?
  Talk given at the British Colloqium for Theoretical Computer Science (BCTCS 05), Nottingham, March 2005
• Codata
  Talk given at the Annual Types Workshop in Jouy-en-Josas, December 2004
• Towards a High Level Quantum Programming Language
  Invited lecture at the Midland Graduate School Christmas seminar, 13/12/04 in Leicester
  More detailed than previous talks.
• A functional quantum programming language
  Talk given at Trends in Functional Programming, November 2004, Munich
  Further evolution based on previous talks.
• Towards a High Level Quantum Programming Language
  Talk given at the University of Akureyri, Iceland, 5/11/04
  This is a modified version of the IFIP talk, below.
• Functional Quantum Programming
  Talk at the meeting of the IFIP WG 2.1 in Nottingham, 6/9/2004
  based on joint work with Jonathan Grattage and discussions with Slava Belavkin.
• Inductive Types for Free
  Talk at ICALP 2004 in Turku on our paper Representing Nested Inductive Types using W-types
  based on joint work with Michael Abbott and Neil Ghani
• Programming with Universes
  Workshop on Datatype-Generic Programming, Oxford, 2004.
• Normalization by evaluation for
  based on joint work with Tarmo Uustalu
  FLOPS 2004, Nara, Japan
• Why Dependent Types Matter
  Nijmegen, 26.8.03
  Departmental seminar on invitation by Henk Barendregt.
• Towards a monadic semantics of quantum computation
  Invited talk at the Workshop on Quantum Programming Languages, Ottawa, 15.6.03
• Containers
  IFIP WG 1.3 meeeting, Menorca, 1.6.03
• Generalized general recursion
  TYPES Termination workshop in Sweden, November 2002
• Normalisation by Completeness
  Seminar talk in Edinburgh, 2001