home search a-z help
University of Cambridge Andrew Pitts
Recent Talks
Department of Computer Science and Technology > Andrew Pitts > Recent Talks


Locally Nameless Syntax and Semantics. Huawei-Edinburgh University Coffee House Tech talk, 7 November 2023. [pdf]
Locally Nameless Sets. Contributed talk at POPL 2023 [pdf]
Constructive Initial Algebra Semantics. Online Worldwide Seminar on Logic and Semantics (OWLS), 21 April 2021. [pdf] [video]
Unfinity Categories. Logic and Semantics Seminar, Department of Computer Science and Technology, University of Cambridge, 26 March 2021. [pdf] [video]
Quotients in Dependent Type Theory. Invited talk at 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), on-line, 3 July 2020. [slides (pdf)] [abstract (pdf)] [video]
Axiomatizing Cubical Sets Models of Univalent Foundations. Invited talk at Workshop on Homotopy Type Theory/ Univalent Foundations (HoTT/UF 2018), Oxford, UK, 7-8 July 2018 [slides (pdf)]. An updated version of this talk was given as a Homotopy Type Theory Electronic Seminar on 20 September 2018 [video] [slides (pdf)].
Nominal Cubical. Seminars at Aarhus University, October 2017. [part I, part II (pdf)]
Using Agda to Explore Path-Oriented Models of Type Theory. Talk at Newton Institute BigProof programme, 27 June 2017. [slides (pdf)]
On Proofs of Equality as Paths. Invited talk at FOMUS - Foundations of Mathematics: Univalent Foundations and Set Theory, workshop at ZiF Center for Interdisciplinary Research, Bielefeld University, Germany, 18-23 July 2016. [video] [slides (pdf) (updated 2016-10-07)]
Names and Symmetry in Computer Science. Joint invited tutorial at 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS2015) and 42nd International Colloquium on Automata, Languages and Programming (ICALP 2015), Kyoto, Japan, 6-10 July 2015. [slides (pdf)] [abstract (pdf) © 2015 IEEE Computer Society]
Semantics of Local Names. Joint invited talk at Mathematical Foundations of Programming Semantics XXXI (MFPS 31) and 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), Nijmegen, Netherlands, June 2015. [slides (pdf)]
Dependent Type Theory with Abstractable Names. Invited talk at 9th Logical and Semantic Frameworks, with Applications (LSFA 2014), Brasília D.F., Brazil, 8-9 September 2014. [slides (pdf)]
Nominal Sets and Dependent Type Theory. Invited talk at 20th Conference on Types for Proofs and Programs (TYPES 2014), Institut H. Poincaré (IHP), Paris, 12-15 May 2014. [slides (pdf)]
Symmetric Scott. Invited talk at LICS 2013 and MFPS XXIX joint Special Session honouring Dana Scott, New Orleans, USA, 25 June 2013. [slides (pdf)]
Generative Names and Dependent Types. Talk at 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2012), Copenhagen, Denmark, 9 September 2012. [slides (pdf)]
Step-indexed Biorthogonality. Talk at Parametricity Workshop, University of Strathclyde, 2 May 2012. [slides (pdf)]
Nominal Sets and their Applications. Invited lectures at Midland Graduate School (MGS 2011), University of Nottingham, UK, 11-15 April 2011. [slides (pdf)]
Nominal System T. Talk at 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), Madrid, Spain, 17-23 January 2010. [Abstract, slides (pdf), paper (pdf)]
Contextual Equivalence in Higher-Order Typed Languages. Invited talk at European Symposium on Programming (ESOP 2007), Braga, Portugal, 2007. [slides (pdf)]
Generative Unbinding of Names. Talk at 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), Nice, France, 17-19 January 2007. [Abstract, slides (pdf), paper (pdf)]
Lectures on Nominal Syntax and Semantics at International Summer School On Applied Semantics (APPSEM II 2005), Frauenchiemsee, Germany, 8-12 September 2005. [Course web page]
Alpha-Structural Recursion and Induction. Invited talk at 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), Oxford, UK, August 2005. [Abstract, slides (pdf).]
Equivariant and Nominal SOS. Invited talk at SOS 2004 satellite workshop of CONCUR 2004, London, August 2004. [Abstract, slides (pdf).]
Nominal Semantics of Abstraction and Restriction. Invited talk at CTCS 2004, IT University, Copenhagen, August 2004. [Abstract, slides (pdf).]
Equivariant Syntax and Semantics. Invited talk at ICALP 2002, Malaga, Spain, July 2002. [Abstract (pdf), slides (pdf).]
Nominal Logic: A First Order Theory of Names and Binding. Invited talk at TACS 20001, Sendai, Japan, October 2001. [Abstract, slides (pdf), paper (ps) (pdf).] (A preliminary version of this talk was given at the IJCAR 2001 Workshop on MEchanized Reasoning about Languages with variable bINding (MERLIN 2001), Siena, Italy, June, 2001.)
A Fresh Approach to Representing Syntax with Static Binders in Functional Programming. Invited talk at ICFP 2001, Firenze, Italy, September 2001. [Abstract, slides (pdf), (ps).]
Operational Semantics and Program Equivalence. Lectures at the International Summer School On Applied Semantics, APPSEM 2000, Caminha, Minho, Portugal, 9-15 September 2000. [Course web page (These lectures supercede: Operational Semantics for Program Equivalence, an invited talk at MFPS XIII, CMU, Pittsburgh, 23--26 March 1997; the slides for this talk are still available here.)
A Computer Science Application of Permutation Models of Set Theory. Invited talk at British Logic Colloquium 2000, University of East Anglia, Norwich, UK, 7-9 September 2000. [Abstract, slides.]
A Metalanguage for Programming with Bound Names Modulo Renaming. Talk at Mathematics of Program Construction, MPC2000, Ponte de Lima, Portugal, 3-5 July 2000. [Abstract, slides, paper.] (An older version of the talk, putting more emphasis on FreshML examples and less emphasis on FM-sets is here.)
Tripos Theory in Retrospect. Invited talk at Tutorial Workshop on Realizability Semantics and Applications, June 29-July 12, 1999. A workshop associated to the 1999 Federated Logic Conference, Trento, Italy. [Abstract, slides, paper.]
A New Approach to Abstract Syntax Involving Binders. Invited talk at School in Logic and Computation, Heriot-Watt University, Edinburgh, 10-13 April 1999. [Abstract, slides, paper.]
Operational Versus Denotational Methods in the Semantics of Higher Order Languages. Invited tutorial at PLILP/ALP'98, Pisa, Italy, 16-18 September, 1998. [Abstract, slides.]
Parametric Polymorphism and Operational Equivalence. Talk at the 2nd Workshop on Higher Order Operational Techniques in Semantics (HOOTS2), Stanford CA, December 1997. [Abstract, slides, paper.]