*Á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:*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.
- 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.
- 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.

Martin Escardo m.escardo@cs.bham.ac.uk

Last modified: Mon Jun 20:22:50 UTC 2019