Recent Talks

• The power of Pi, Lambda Days 2020, Krakow, February 2020
• Conceptual Programming with Python, Trends in Functional Programming in Education (TFPIE) , Krakow, February 2020
• On inductive types, Foundations and Applications of Univalent Mathematics, Herrsching, November 2019
• The Tao of Types, My inaugural lecture, video, Nottingham, November 2019
• Naturality for Free - The category interpretation of directed type theory, Third Symposium on Compositional Structures, Oxford, March 2019
• Naturality for Free - The category interpretation of directed type theory, EU TYPES WG meeting, Krakow, February 2019
• Why Type Theory matters, Lambda Days 2019, Krakow, February 2019
• The partiality monad, An Intersection of Neighbourhoods, Achim Jung Fest, Birmingham, September 2018
• Towards higher models and syntax of type theory, Types, Homotopy Type Theory, and Verification, workshop, Bonn, June 2018.
• An introduction to (Homotopy) Type Theory
  FMV Foundations in Mathematics, Munich, Germany, April 2018. Invited talk.
• The joy of QIITs
  AMS Special Session on Homotopy Type Theory, San Diego, USA, January 2018. Invited talk.
• A Taste of Homotopy Type Theory
  Kolloqium über reine Mathematik, Hamburg, Germany, December 2017. Invited talk.
• Homotopy Type Theory: Vladimir Voevodsky
  Computerphile (YouTube), October 2017
• Propositions as Types
  Computerphile (YouTube), September 2017
• Naïve Type Theory (invited talk)
  7th South of England Regional Programming Language Seminar, Warwick, UK, September 2017. Invited talk.
• Naïve Type Theory(tutorial)
  Workshop on Homotopy Type Theory/ Univalent Foundations, Oxford, UK, September 2017. Invited tutorial.
• Introduction to homotopy type theory
  EU Types summer school , Ohrid, Macedonia, July 2017. Invited course.
• Monadic containers and universes
  23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, June 2017. Contributed Talk.
• From setoid hell to homotopy heaven?
23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, June 2017. Contributed Talk.
• Naïve Type Theory
  Midland Graduate School 2017 (MGS 2017) , Leicester, UK, April 2017. Course.
• Introduction to homotopy type theory
  22nd Estonian Winter School in Computer Science (EWSCS) , Palmse, Estonia, January 2017. Invited course.
• Computer Science ∩ Mathematics (Type Theory) - Computerphile (youtube), January 2017
• A constructive justification of Homotopy Type Theory
  Homotopy Type Theory in Logic, Metaphysics and Philosophy of Physics, University of Bristol, September 2016.
• Homotopy Type Theory as a Foundation of Mathematics ?
  Workshop on Categorical Logic and Univalent Foundations, Leeds, July 2016.
• Naive Type Theory
  FOMUS - Foundations of Mathematics: Univalent Foundations and Set Theory,Bielefeld, July 2016. Invited Talk.
• Why cubical type theory?
  The 5th International Congress on Mathematical Software, Berlin, July 2016. Invited Talk.
• Partiality, revisited
  TYPES 2016, Novi Sad, May 2016.
• Why does Homotopy Type Theory matter?
  HoTT workshop at Fields Institute, Toronto, May 2016. Invited Talk.
• What is a category? (in univalent type theory)
  CHoCoLa meeting, ENS Lyon, February 2016. Invited Talk.
• The coherence problem in HoTT
  Minisymposium on HoTT and UF, DMV, Hamburg, September 2015. Invited Talk.
• Type Theory eats itself without indigestion
  Workshop on HoTT and UF, Warsaw, June 2015. Invited Talk.
• HoTT Xmas
  MGS Cristmas seminar. Sheffield, December 2014 Oxford, 2014
• A syntax for cubical type theory
  joint with Ambrus Kaposi, HoTT workshop, Oxford, November 2014
• The Coherence Problem in HoTT
  FP lab Away Day, Buxton, July 2014
• Towards a syntax for cubical Type Theory (1)(2)
  Semantics of Proofs and Certified Mathematics, Institute Henri Poincare, Paris, April 2014
• Containers in Homotopy Type Theory
  Mathematical Structures of Computation (Recent developments in Type Theory), Lyon, January 2014
• Homotopy Type Theory for Dummies
  LFCS seminar, University of Edinburgh, October 2013
• Extensionality in Type Theory
  Meeting in honor of Pierre-Louis Curien, Venice, September 2013
• From High School Algebra to University Algebra
  Functional Programming Lab Away Day, Cressbrook, June 2013
• Homotopy and Univalence
  Institute of Advanced Study, Special Year on Homotopy Type Theory, Princeton, January 2013
• Homotopy Type Theory without Homotopy Theory
  Foundations of Mathematics for Computer Aided Formalisation (FOMCAF13), Padova, Janruay 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