- Álgebra topológica: uma abordagem para a
análise de circuitos. Gramado, Brazil, 1987. Décimo
Congresso Nacional da Sociedade Brasileira de Matemática
Aplicada e Computacional (CNMAC).
- Um sistema de tipos para Prolog. Vitória, Brazil,
1990. Décimo terceiro Simpósio da Sociedade Brasileira
de Computação (SBC).
- Induction and recursion on the uniform real line. Møller Centre,
Cambridge, September 1994. Second Imperial College Workshop on Theory
and Formal Methods.
- PCF extended with real numbers. FernUniversität Hagen, Germany,
August 1995. First Workshop on Computability and Complexity in
Analysis (CCA).
- Integration in Real PCF. Imperial College, London, October
1995. First Computation and Approximation Workshop (Comprox).
- Real PCF extended with existential is universal. Christ Church,
Oxford, March 1996. Third Imperial College Workshop on Theory
and Formal Methods.
- Integration in Real PCF. New Brunswick, New Jersey, July
1996. Eleventh Annual IEEE Symposium on Logics in Computer Science
(LICS).
- Many talks in the Mathematics Department of the Technische
Hoschule Darmstadt, in four visits in the period 1995-1997.
- Induction and recursion on the partial real line via
biquotients of bifree algebras. Technische Hoschule Darmstadt,
Germany, September 1996. Second Computation and Approximation
Workshop (Comprox).
- Real PCF. Birmingham University, School of Computer
Science, October 1996.
- Properly injective spaces and function
spaces. Pittsburgh, March 1997. Carnegie Mellon University,
Department of Computer Science.
- Injective spaces and domain theory. Munich, May 1997. Third
Workshop on Domains.
- PCF extended with real numbers: A domain-theoretic approach to
higher-order exact real number computation. Brighton, May
1997. University of Sussex, Department of Computer Science.
- PCF extended with real numbers (a survey).
Department of Computer Science, University of Edinburgh, June 1997.
- Injective spaces and function spaces. London, June 1997. Queen Mary
and Westfield College, University of London.
- Induction and recursion on the partial real line via
biquotients of bifree algebras. Warsaw, June 1997. Twelfth Annual
IEEE Symposium on Logic in Computer Science (LICS).
- Exact real number computation.
Birmingham University, September 1997. MATHFIT Summer school on
New Paradigms for Computation on Classical Spaces.
- Is parallelism unavoidable in exact real number computation?
Birmingham University, September 1997. Third Computation and
Approximation Workshop (Comprox).
- Real number computation, domain theory, and
PCF. Cambridge University, Department
of Computer Science, 1997.
- Injective spaces via the filter monad. 12th Summer
Conference on General Topology and its Applications, North Bay,
Canada, August 1997. Invited participant at special session on
Topology and Computer Science.
- Introduction to exact real number computation.
University of Edinburgh, February 1998. Computer Science Colloquium.
- Introduction to Real PCF (invited speaker). Universite Pierre et
Marie Curie, Paris, March 1998. Third Conference on Real Numbers and
Computers (RNC3).
- Injectivity, projectivity and denotational semantics.
University of Edinburgh, March 1998. Semantics Club talk.
- On extensions of the programming language PCF with real
numbers data types. Indianapolis, June 1998. Tutorial
Workshop/Summer Schooon Real Number Computation preceding the IEEE
Symposium on Logic in Computer Science (LICS).
- Computação exata com números reais:
teoria e prática. Porto Alegre, Brasil, July
1998. Pontifícia Universidade Católica, Departamento de
Matemática.
- Computação exata com números reais via
programação funcional. Porto Alegre, Brasil, July
1998. Pontifícia Universidade Católica, Departamento de
Computação.
- Effective and sequential definition by cases on the reals via
infinite signed-digit numerals. Pisa, September 1998. First
Workshop on Applied Semantics (APPSEM).
- Introduction to exact numerical computation.
February 1999, School of Mathematical and Computational Sciences, St Andrews
University.
- A point-free construction of the patch topology (invited
speaker). University of Connecticut at Stamford, April 1999. Fifth
Northeastern Conference on Topological Methods in Computer
Science.
- Injective spaces, semantic domains and monads.
University of Connecticut at Stamford, April 1999. Fifth
Northeastern Conference on Topological Methods in Computer
Science.
- Injective spaces, semantic domains and monads.Tulane University,
New Orleans, May 1999. Fifteenth Conference on Mathematical
Foundations of Programming Semantics (MFPS).
- On the compact-regular coreflection of a stably compact locale.
Tulane University, New Orleans, May 1999. Fifteenth Conference on
Mathematical Foundations of Programming Semantics (MFPS).
- A metric model of PCF.
University of Edinburgh, May 1999. Semantics Club talk.
- Introduction to exact real number computation.
University of Edinburgh, May 1999. Informatics Jamboree.
- Higher-order exact real number computation via domain theory.
University of St Andrews, June 1999. Computer Algebra Group meeting.
- A metric model of PCF.
Workshop on Realizability Semantics and Applications,
June 30 1999 (associated to the Federated Logic Conference,
held in Trento, June 29-July 12, 1999).
- Topological methods in computer science. University of St
Andrews, 7 October 1999, Theory Lunch talk.
- In analysis there are singularities and in computation there
is non-termination. Séminaire PPS, University of Paris VII, 3
February 2000.
- Lawson computability. Séminaire PPS, University of Paris
VII, 3 February 2000.
- (In)equality tests in exact real number
computation.Research Institute for Symbolic Computation, Linz,
Austria, 9 February 2000.
- On topologies for general function spaces. Colloquium at the Mathematics Department of Tulane University, New Orleans, 18 February 2000.
- Continuous lattices in Topology and Analysis I. Informal
Analysis Seminar at the School of Mathematics and Statistics of St
Andrews University, 29 February 2000.
- Continuous lattices in Topology and Analysis II. Informal
Analysis Seminar at the School of Mathematics and Statistics of St
Andrews University, 7 March 2000.
- Lawson Computability. Seminar at the Department of
Computer Science of the University of Manchester, 10 March 2000.
- Continuous lattices in Topology and Analysis III.
Informal Analysis Seminar at the School of Mathematics and Statistics
of St Andrews University, 14 March 2000.
- Applied and theoretical aspects of exact real number
computation. Seminar at the Department of Computer Science of the
University of Manchester 15 May 2000.
- Injective spaces, function spaces, perfectly embedded
subspaces and the patch frame. Informal talk the Department of
Computer Science of the University of Manchester, 16 May 2000, to a
group organized by David Rydeheard and Harold Simmons.
- Exact real number computation via free mid-point algebras. Computer algebra group meeting, School of Computer Science, St Andrews University, 2nd June 2000.
- The patch topology. Dagstuhl Seminar
00231, Topology in Computer Science: Constructivity; Asymmetry and
Partiality; Digitization, organized by R. Kopperman (New York),
M. Smyth (London), D. Spreen (Siegen), 4th-9th June 2000.
Invited participant.
- Continuity, topology and the theory of computation.
School of Computer Science,
Birmingham University, 20th June 2000.
- Hausdorff compactifications of topological function spaces via the theory of continuous lattices.
MFCSIT 2000, University College Cork, Ireland, 20th July 2000.
- Introduction to exact numerical computation.
ISSAC 2000 tutorial, St Andrews, 6th July 2000.
- Pataraia's fixed-point theorem. Theory Lunch talk, School
of Computer Science, University of Birmingham, 27th October 2000.
- The frame of Scott continuous nuclei on a locale.
74th Peripatetic Seminar on Sheaves and Logic (PSSL),
Centre for Mathematical Sciences, Cambridge, 4th November 2000.
- Function-space compactifications of function spaces.
Analytic Topology Seminar, Mathematical Institute, Oxford University,
20th November 2000.
- Higher-order exact real-number computation with Real PCF.
Computer Science Colloquium, University of Wales Swansea, 28th
November 2000.
- Computational aspects of the notion of compactness.
Department of Mathematics and Computer Science,
University of Leicester, 2nd March 2001.
- A computational reading of the notion of compactness. Third Appsem workshop, Darmstadt, Germany, 19-22 March 2001.
- A metric model of PCF. Theory lunch talk,
School of Computer Science, University of Birmingham, 20 April 2001.
- Compactly generated spaces and locales. The Summer Conference Series in
Topology and its Applications XVI, July 18-21, 2001.
City College of New York, NY USA.
- Various notions of compactly generated space. Invited Keynote Lecture at the International Conference on Applicable General Topology, Ankara, Turkey, August 12--18, 2001.
- The unit interval. Contributed talk at
the International Conference on Applicable General Topology, Ankara,
Turkey, August 12--18, 2001.
- Real PCF. Invited lecture at the 2nd International
Symposium on Domain Theory (ISDT'01), Sichuan University, Chengdu,
China, October 22--26, 2001. Unfortunately, for bureaucratic reasons
beyond my control (not the Chinese' fault, I must say), I couldn't
attend this conference and deliver the talk. However, Achim Jung
kindly delivered it for me, using overheads prepared by
myself. Thanks, Achim!
- "The" unit interval. (Based on joint paper with Alex Simpson,
A universal characterization of the Euclidean unit interval.)
Computability and Complexity in Analysis,
11-16 November 2001, Dagstuhl Schloss, Germany. Dagstuhl seminar.
- A universal characterization of [0,1]. Theory lunch talk,
School of Computer Science, University of Birmingham, 22 Nov 2001.
- Abstract data types for constructive real numbers. Logic computer science seminar, BRICS, Arhus, Denmark,
1st Feb 2002.
- On the computational content of the notion of compactness - or:
topology via functional programming. Theoretical Computer Science
Seminar, School of Computer Science, University of Birmingham, 18 Feb 2002.
- Compactly generated locales. Invited talk at the Second workshop on
formal topology, Auditorium S. Margherita, Campo S. Margherita,
Venice, April 4-6, 2002.
- Compactly generated regular locales. Mathematical Structures for Computable Topology and Geometry. 26 May 2002, Dagstuhl Schloss, Germany. Dagstuhl seminar.
- Applications of the lambda-calculus to general topology.Mathematical Structures for Computable Topology and Geometry. 31 May 2002, Dagstuhl Schloss, Germany. Dagstuhl seminar.
- General topology via Church's calculus of functions. Seminar talk at the Department of Pure Mathematics, Open University, 11 June 2002.
- Interactions between domain theory and topology. Invited
talk at the Workshop on
Domain Theory in Honour of Dana S. Scott's 70'th birthday, July
20-21, 2002, affiliated with FLoC'02.
- Topologies on spaces of continuous functions.
Topology and Computer Science
Seminar, School of Computer Science, University of Birmingham, 8th November
2002.
Slides available in the following formats:
Slides available in the following formats:
pdf,
ps,
dvi.
- Topology via the lambda-calculus. Analytic Topology
Seminar, Mathematical Institute, Oxford University, 2nd December
2002.
- Data types as topological spaces. Christmas seminars,
Midlands Graduate School
in the Foundations of Computer Science.
University of Birmingham, 17th December 2002.
- Lawson computability. MFPS XIX,
special session on domain theory, 19th March 2003, Montreal,
Canada.
Slides available in the following formats:
pdf,
ps,
ps (8 slides per page),
ps.gz,
dvi,
dvi.gz.
- Mathematical foundations of functional programming with real
numbers. Four-lecture course in the Midlands Graduate School in the
Foundations of Computer Science, Leicester, Mar 31, Apr 1, 2003.
Scanned handwritten notes available in
pdf (warning: this is a very large file: 5134859 bytes.)
- Function-space compactifications of function spaces.
Galway topology colloquium affiliated to the 55th British Mathematical
Colloquium, Birmingham University, 7-10 Apr 2003.
Slides available in the following formats:
pdf,
ps,
ps (8 slides per page),
ps.gz,
dvi,
dvi.gz.
- Topology of data types and computability concepts. Three two-hour
lectures at the Bellairs Workshop
Domain Theoretic Methods in Probabilistic Processes, 21-25 Apr 2003,
at McGill's Bellairs Research Institute in Barbados.
Expanded and revised edition of manuscript lecture notes are available:
Download:
pdf,
ps,
ps.gz,
dvi,
dvi.gz.
- Imaginary spaces. Workshop From Sets and Types to Topology and Analysis
Towards Practicable Foundations for Constructive Mathematics, 12--16 May 2003,
Venice International University (VIU), San Servolo, Venice, Italy.
- Topology via the lambda-calculus. Computer Science Seminar, School of Cognitive and Computing Sciences, University of Sussex, 27th June 2003.
- A gentle introduction to locales for topologists.
Topology and Computer Science
Seminar, School of Computer Science, University of Birmingham, 25th July
2003.
- Topology of data types and computability concepts.
LFCS seminar, University of Edinburgh, 14th October 2003.
- Topology of data types, and the computational content of classical topology.
Workshop on Domains, Topology and Constructive Logic,
LMU, Department of Mathematics, University of Munich, 1-2 November 2003.
- Classical and synthetic topology of data types. Research Seminar,
LMU, Department of Mathematics, University of Munich, 4th November 2003.
- Mathematical Foundations of Functional Programming with
Real Numbers. Faculties of Mathematics and of Informatics joint seminar, PUC-RS, Brazil, 10th December 2003.
- Topology of data types and computability concepts. Postgraduate course, Institute of Informatics, UFRGS, Brazil, 11-12 December 2003.
- Topology of data types and computability concepts. Postgraduate course, School of Informatics, UCPel, Brazil, 15-16 December 2003.
- Topology of data types. Postgraduate course,
Midlands Graduate School and Appsem Spring School, 29-30 March 2004.
- Synthetic topology in a topos.
80th Peripatetic Seminar on Sheaves and Logic, 3-4 April 2004, Cambridge, UK.
- An exercise in semantics. Theory lunch talk, School of Computer
Science, University of Birmingham, 14 May 2004.
- Topology via higher-order logic.
Logic seminar, School of Mathematics, University of Leeds, 28 Apr 2004.
- Topology via higher-order logic. Special session on Logical Foundations of Programming Semantics, jointly in 2004 annual meeting of the Association for Symbolic Logic
and 20th workshop on Mathematical Foundations of Programming Seminatics. 24 May 2004
- A computational application of the Tychonoff theorem. 19th 'Summer' Conference on Topology and its
Applications, 5-9 July 2004, Department of Mathematics and Applied
Mathematics, University of Cape Town, South Africa, special session
on Topology and Computer Science.
- A Hausdorff compactification of the Samborski function space.
Dagstuhl seminar 04351
on Spatial Representation vs.
Continuous Computational models, organized by R. Kopperman, M.B.
Smyth, D. Spreen, J. Webster, Dagstuhl Castle, 22-27 Aug 2004,
Germany.
- Finitary approximations of Markov processes. Domains VII workshop.
Continuous Computational models, organized by A. Jung,
Klaus Keimel and Thomas Streicher, Darmstadt, 30 Aug - 2 Sept 2004,
Germany.
- Synthetic topology of data types and classical spaces. Computing Laboratory, Oxford, Seminar on Concepts of space, 22 Oct 2004.
- Operational domain theory and topology of a sequential programming language. Edinburgh, LFCS seminar, 11 Feb 2005.
- Operational domain theory and topology of a sequential programming language. Computer Laboratory, Cambridge, Logic and Semantics Seminar, 4 Mar 2005.
- Synthetic compactess revisited. Theory Lunch talk, School of Computer Science, University of Birmingham, 8 Apr 2005.
- Synthetic topology in probabilistic computation. Workshop on Causality, Spacetime Topology and Domain Theory at the Bellairs Institute of McGill University in Barbados, 25-29 April 2005.
- Operational domain theory and topology of a sequential programming language. 7eme rencontre de l'ACI NIM Geocale Seminar, University of Paris 7, PPS, 20th June 2005.
- Compactness in topology and computation. Invited talk at Satellite Seminar of CCA 2005, August 25-29, 2005, Kyoto, Japan.
- Semantics of exact real-number computation. Invited talk at Small TYPES workshop Constructive analysis, types and exact real numbers. Nijmegen, the Netherlands, 3-4 October 2005.
- Operational domain theory and topology. Seminar at UFRGS, Brazil, 13 December 2005.
- Semantics of exact real number computation. Seminar at PUCRS, Brazil, 14 December 2005.
- Excursions on exact real number computation. Departmental talk, Cambridge, Computer Science, 8th Feb 2006.
- Domain-theoretic approximation of Markov processes. Talk at the workshop "Probabilistic transition systems" of the Geocal'06 meeting, Marseille, France, Feb-Mar 2006.
- Operational domain theory and topology. Midlands Graduate School, 8-12 April, Leicester, UK.
- Stably compact spaces.Invited talk at workshop Modal Logic, Stone Duality and Coalgebras, 12-13 June 2006, Leicester University.
- Synthetic topology.Workshop
Trends in Constructive Mathematics, Frauenwoerth (Chiemsee, Bavaria, Germany),
19-23 June 2006.
- Topology in the theory of computation. Invited talk at the Summer Conference on Topology and its Applications to be held at Georgia
Southern University (Statesboro, GA) July 6-9, 2006.
- Infinite spaces that admit fast exhaustive search. Computational Structures for Modelling Space, Time and Causality, Dagstuhl seminar 06341, Germany, 20-25 Aug 2006.
- Infinite spaces that admit fast exhaustive search. LFCS seminar, School of Informatics, University of Edinburgh, 5th September 2006.
- Topology, logic and computation.
Invited talk at
CSL 2006 conference
(European Association for Computer Science Logic),
25 - 29 September 2006, University of Szeged, Hungary.
- Domain theory and denotational semantics. Midlands Graduate School in the Foundations of Computing Science, Nottingham, 16-20 April 2007.
- Algorithmic topology of program types. Invited Tutorial at 3rd Workshop on Formal Topology, Padua 8-12 May 2007.
- Algorithmic topology of program types. Invited talk at Wollic'07, 2-5 July 2007.
- Infinite sets that admist exhaustive search I. Invited talk at a joint special session of LICS/ASL, (Logic Colloquium), 14-19 July 2007, Wroclaw, Poland.
- Infinite sets that admit exhaustive search II, LICS 07, 10-14 July 2007, Wroclaw, Poland.
- Infinite sets that admit fast exhaustive search. Invited talk at combined workshops Domains VIII and Computability over continuous data types. Novosibirsk, 11-15 September 2007.
- Computing with infinite objects in finite time (and sometimes fast). Departmental seminar, School of Computer Science, University of Birmingham, UK, 18th October 2007.
- The role of topology in computation with infinite objects. Analytic Topology seminar, Department of Mathematics, Oxford University, UK, 7th November 2007.
- Denotational semantics. Midlands Graduate School in the Foundations of Computing Science, Birmingham, 14-18 April 2008.
- Infinite sets that admit exhaustive search in finite time. Joint Queen Mary/Imperial Seminar Queen Mary, 28th May 2008.
- Compactly generated spaces in higher type computation. Three invited tutorial talks at the summer conference on topology and its applications, Mexico City, 29 July-1st August 2008.
- Exhaustible sets in higher-type computation. Invited talk at the Computability and Complexity in Analysis (CCA) conference, Hagen, 21-24 August 2008.
- Computability of continuous solutions of higher-type equations. Domains Workshop, Sussex, 22-24 September 2008.
- A Monad for Exhaustively Searching Infinite Sets in Finite Time. LFCS seminar Edinburgh, 19th of February 2009.
- The Peirce translation. LFCS talk Edinburgh, 20th of February 2009.
- Semantics. Midlands Graduate School in the Foundations of Computing Science, Leicester, UK
Monday 30th March to Friday 3rd April 2009.
- On semi-decidability of may, must and probabilistic testing in a higher-type setting. Accepted paper for MFPS 2009, April, Oxford.
- Understanding bar recursion and exhaustible sets. Seminar at Oxford University Computing Laboratory on 15th May 2009.
- Computability of continuous solutions of higher-type equations. Accepted paper for CiE 2009, July, Heidelberg.
- Theory and practice of higher-type computation. Invited tutorial at CCA 2009, August 18-22, Ljubljana, Slovenia.
- Topology, computation, monads, games and proofs. Invited talk at MFPS 2010, May 6-10, 2010, Ottawa, Canada.
- Selection functions in topology, computation, monads, games and proofs. Constructive Mathematics: Proofs and Computation
7-11 June 2010, Benedictine nunnery on Fraueninsel, Chiemsee
- The Peirce translation and the double negation shift. CiE'2010 ,
Ponta Delgada, July 2010.
- Searchable sets, Dubuc-Penon compactness,
Omniscience Principles, and the Drinker Paradox. CiE'2010,
Ponta Delgada, July 2010.
- Topology and computability. Talk at the Analytic Topology in Mathematics and Computer Science seminar , May 19, 2010, Oxford.
- Maybe locales are made of points after all. Talk at 7th CLP'2010 (Categories, Logic and Foundations of Physics workshop), Birmingham 21 September 2010.
- What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common. Invited talk at MSFP'2010 (ACM SIGPLAN Mathematically Structured Functional Programming), Baltimore, Maryland, 25 September 2010, workshop affiliated to ICFP'2010 (International Conference on Functional Programming).
- Selection functions everywhere. Logic and Semantics Seminar, Computer Laboratory, Cambridge, 28th January 2011.
- An amazingly versatile functional. Logic Seminar, Department of Computing, Imperial College, 17th February 2011.
- When can we effectively decide universal quantifications? Logic Seminar, Department of Pure Mathematics, Leeds, 23rd February 2011.
- The ubiquitous selection monad. Wessex Seminar, Swansea, 7 April 2011.
- Game Theory, Topology and Proof Theory
for Functional Programming. Course at MGS'2011, Nottingham University, 11-15 April 2011.
- Programs from proofs. Invited tutorial at MFPS'2011, Carnagie Mellon University, Pittsburgh 25-28 May 2011.
- Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics. Types, 08-11 September 2011, Bergen, Norway.
- A proof of omniscience in Agda. Wessex Seminar, Queen Mary London, 14 September 2011.
- Infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics. Dagstuhl seminar, Germany, 09-14 October 2011.
- Can computers deal with infinite objects in finite time? Lecture at the Invariants Oxford Mathematical Society, 25th October 2011.
- Categorical
axioms for functional real-number
computation. Mathematics: Algorithms and Proofs, invited
tutorial. Lorentz Center, Netherlands, November 28 - December
2, 2011
- The
topology of seemingly impossible functional
programs. Invited tutorial
for POPL'2012. Philadelphia,
28
January 2012.
-
Topology for functional
programming. Invited course
for EWSCS'2012. Palmse,
Estonia,
26 Feb - 2 Mar 2012.
- Computing with Infinite Objects. Course at the Midlands Graduate School, University of Birmingham, UK, 23-27 April 2012.
- Searchable sets and ordinals in system T. SAS seminar (Semantics and Syntax: A Legacy of Alan Turing) at the Newton Institute, Cambridge, Thursday 31 May 2012.
- The intrinsic topology of a Martin-Lof universe, with an application to Rice's theorem for the universe. Invited talk at the special session Computability on Continuous Data of MFPS (Mathematical Foundations of Programming Semantics), Bath, Friday 8th June 2012.
- The intrinsic topology of the universe in intuitionistic type theory. Invited Keynote speaker at 8th International Workshop on Developments in Computational Models (DCM), Corpus Christi College, Cambridge, 17 June 2012.
- The intrinsic topology of a Martin-Loef universe. Fourth Workshop on Formal Topology, Ljubljana University, 19th June 2012.
- Continuity of Goedel system T functionals. Talk at Nottingham University's Functional Programming Lab, 9th November 2012.
- Constructive instances of excluded middle. 18th Wessex Seminar, Southampton, 15th January 2013.
- The universe is indiscrete. Seminar at the IAS (Institute of Advanced Studies), Univalent Foundations Programme, Princeton, 22 February 2013.
- An introduction to topological ideas in computation. Graduate course at phdopen, University of Warsaw, 23-35 May 2013.
- Continuity of Goedel's system T definable functionals via effectful forcing. MFPS (Mathematical Foundations of Programming Semantics), New Orleans, 23 June 2013.
- Interactions between topology and computation. Invited tutorial (three lectures) at BLAST, Chapman University, Orange, LA, 5-7 August 2013.
- Interactions between topology and computation. Invited talk at the Colloquium Aveiro, Departamento de Matematica, University of Aveiro, 20th September 2013.
- Topological phenomena in Martin-Loef Type Theory. Bellairs workshop on duality, March 14-21 2014, barbados.
- Continuity in Type Theory, workshop Semantics of Proofs and Programs, during the Semantics of proofs and certified mathematics trimester at the Institute Henri Poincare, Paris, 10-13 June 2014.
- Continuity in constructive dependent type theory, invited talk at Fifth Workshop on Formal Topology, Institut Mittag-Leffler, Djursholm, Stockholm, 8-10 June 2015
- The geometry of constancy (in HoTT and cubicalTT), Workshop on Homotopy Type Theory / Univalent Foundations, June 29–30, 2015, Warsaw, Poland, Collocated with RDP/TRA/TLCA 2015.
- Searchable types in constructive dependent type theory. Invited talk at Continuity, Computability, Constructivity – From Logic to Algorithms, (CCC 2015)
Schloss Aspenstein, Kochel am See, near Munich, 14-18 September 2015.
- Voevodsky's Univalence Axiom. Analytic topology Seminar, University of Oxford, Department of Mathematics, November 2015.
- Infinite types that satisfy the principle of omniscience, invited talk at Computational Aspects of Univalence Workshop
Bergen University, January 20-22, 2016.
- When the principle of omniscience just holds, invited talk at 27th Nordic Congress of Mathematicians, Institut Mittag-Leffler, Logic Session, Department of Mathematics, Stockholm University, March 19th 2016.
- Mathematical degrees of existence in type theory, The Stockholm Logic Seminar, Stockholm University, 22 March 2016.
- Voevodsky's Univalence Axiom. Department of Mathematics, Charles University, Prague.
- Compact types and ordinals in univalent type theory, 2nd HoTT Workshop, FSCD, Porto, 25-26 June 2016.
- Continuity in constructive dependent type theory.Mathematical foundations of computation Seminar, Bath University, 1st November 2016.
- On the versatile selection monad, with applications to proof theory, Leeds Logic Seminar, 9th November 2016.
- Partial elements and recursion in univalent type theory. Workshop on Foundations for the practical formalization of mathematics (FPFM), Nantes, France, April 2017.
- Infinite sets that satisfy the principle of omniscience in constructive type theory, Arvutiteaduse teooriaseminar, Tallinn, May 2017.
- The frame of Scott continuous nuclei on a preframe, invited talk at TACL 2017, Prague, June 2017
- Logic in univalent type theory, invited talk at the Isaac Newton Institute, Cambridge, July 2017
- Univalent Foundations, lecture at the UniMath School, Birmingham, UK, December 2017.
- Topological and Constructive Aspects of Higher-Order Computation, Nordic Logic Summer School, Stockholm, August 7-11 2017.
- Constructive Mathematics in Univalent Type Theory, lecture at the Summer School on Types, Sets and Constructions, May 3-9, 2018, Hausdorff Research Institute for Mathematics, Bonn.
- Injective types and searchable types in univalent mathematics. Invited talk at Workshop on Homotopy Type Theory/ Univalent Foundations, July 7-8, 2018, Oxford.
- Univalent Mathematics at Work, invited speaker for the special session Proof Theory and Constructivism at the Logic Colloquium, July 23-28, 2018 at the University of Udine, Italy.
- Continuity in constructive mathematics using Agda, Autumn school Proof and Computation, 16th to 22nd September 2018, Fischbachau near Munich.
- Univalent Type Theory in Agda, Midlands Graduate School
in the
Foundations of Computing Science,
University of Birmingham, UK, 14 - 18 April, 2019.
- Injective types in univalent mathematics, Center for Advanced study, Oslo, April 2019,
- Compact, totally separated and well-ordered types in univalent mathematics, Types 2019, Centre for Advanced Study, Oslo, Norway, 11-14 June 2019
- Compact, totally separated and well-ordered types
in univalent mathematics, Mathematical Logic and Constructivity:
The Scope and Limits of Neutral Constructivism,
Department of Mathematics, Stockholm University, August 20–23, 2019.
- Equality of mathematical structures, CCC 2019: Computability, Continuity, Constructivity - from Logic to Algorithms,
Ljubljana, 2-6 September 2019
- Equality of mathematical structures, XII Portuguese Category Seminar, Department of Mathematics of the University of Coimbra on September 17, 2019.
- The Cantor-Schröder-Bernstein Theorem for ∞-groupoids. Theory Group Lab Lunch, School of Computer Science, University of Birmingham, UK, 6th February 2020.
- Universe oddities. Workshop Foundations and Applications of Univalent mathematics, 18-20 December 2019, Herrsching, Germany.
- Equality of mathematical structures. University of Wisconsin Logic Seminar, 1st December 2020.
- Equality of mathematical structures. 23rd YaMCATS, online, hosted by the University of Leeds, 5th February 2021.
- Seemingly impossible programs and proofs. Invited talk at CSL'2022, online, hosted by Goettingen University, 19th February.
- There are more groups in the next universe. Workshop in honour of Thierry Coquand's 60th birthday, 24-26 August 2022, Gothenburg.
- Compact totally separated types in constructive univalent mathematics. At The Topos Intitute Colloquium, 28th April 2022.
- Searchable types in HoTT/UF. At Foundations seminar, University of Ljubljana, Faculty of Mathematics and Physics, 26th May 2022.
- Totally separated types. At Types, Thorsten and Theories. A workshop on type theopry in honour of Thorsten Altenkirch's 60th birthday, 12 October 2022, Nottingham.
- Playing rationally against irrational players. At 2º Encontro Brasileiro em Teoria das Categorias, 20-24 March 2023,IME-USP. A video is available.
- Compact ordinals in HoTT/UF. At CIRM Conference 2319 Type Theory, Constructive mathematics and Geometric Logic, Luminy, 1-5 May 2023. A video is available.
- Topology in constructive mathematics and computation. Invited talk at LICS'2024, 8-11 July, Tallinn. A video is available.