*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

Thorsten Altenkirch Last modified: Tue Jun 5 10:05:40 CEST 2018