87.4% of statistics are made up on the spot.
Talks
2022
The semitopology of heterogeneous consensus
20221101-socom
1 November 2022,
Online Social Choice and Welfare Seminar.
The semitopology of heterogeneous consensus
20221101-socom
A mathematical notion of consensus in a heterogeneous permissionless environment. 'Permissionless' means that participants are free to join or leave the network without permission from a central authority; 'heterogeneous' means that participants may have different goals and beliefs.
1 November 2022
Online Social Choice and Welfare Seminar
An overview of my claimed proof of consistency of Quine's New Foundations (ConNF)
20220329-lfcs
29 March 2022,
LFCS, Edinburgh, UK.
An overview of my claimed proof of consistency of Quine's New Foundations (ConNF)
20220329-lfcs
As the title suggests. The claimed proof is here.
29 March 2022
LFCS, Edinburgh, UK
Thanks to the LFCS seminar series. Video online here.
The Cairo Test Suite Workshop
20220316-matchbox
An online presentation of my Cairo property-based and unit test suite (also on GitHub).
16 March 2022
Matchbox DAO, online.
Thanks to Matchbox DAO for the kind invitation to speak.
2021
The Design of the Nominal Datatypes Package in Haskell
20210529-huawei
29 April 2021,
Huawei-Edinburgh Joint Lab, Edinburgh, UK
Video.
Video.
The Design of the Nominal Datatypes Package in Haskell
20210529-huawei
Introducing: a Nominal monad
29 April 2021
Huawei-Edinburgh Joint Lab, Edinburgh, UK
Video
Video
Thanks to the Huawei-Edinburgh Joint Lab. Semiar details and video here.
Equivariant ZFA and the foundations of nominal techniques
20210210-verao
10 February 2021,
XIII Summer Workshop in Mathematics.
Equivariant ZFA and the foundations of nominal techniques
20210210-verao
On the foundations of nominal techniques
10 February 2021
XIII Summer Workshop in Mathematics
Thanks to the summer school organisers.
2020
A semi-topological view of real-world consensus
20201007-galois
7 October 2020,
Galois Tech Talk series, USA.
A semi-topological view of real-world consensus
20201007-galois
Consensus = Topology
7 October 2020
Galois Tech Talk series, USA
Thanks to the Galois talk organisers. Video online here.
A semi-topological view of real-world consensus
20200904-frida
4 September 2020,
FRIDA workshop (7th Workshop on Formal Reasoning in Distributed Algorithms).
A semi-topological view of real-world consensus
20200904-frida
Consensus = Topology
4 September 2020
FRIDA workshop (7th Workshop on Formal Reasoning in Distributed Algorithms)
Thanks to the FRIDA organisers.
What is an EUTxO blockchain?
20200806-galois
A revised and expanded exploration of a new and simple mathematical model of blockchains
6 August 2020
Galois Tech Talk series, USA
Thanks to the Galois talk organisers. Video online here.
What is an EUTxO blockchain?
20200623-lfcs
An exploration of a new and simple mathematical model of blockchains
23 June 2020
LFCS seminar series, Edinburgh, UK
Thanks to Ohad Kammar. See the LFCS Seminar series vidoes online.
2019
Programming with nominal techniques
20190813-dagstuhl
13 August 2019,
Metaprogramming summer school 2019, Dagstuhl, Germany.
Programming with nominal techniques
20190813-dagstuhl
Outline of a nominal datatypes package
13 August 2019
Metaprogramming summer school 2019, Dagstuhl, Germany
Thanks to the summer school organisers. See the summer school webpage.
Nominal techniques: past and future
20190711-icalp
An observation of nominal techniques is that names are a datatype
11 July 2019
ICALP 2019, Patras, Greece
Thanks to the ICALP organisers. See the ICALP programme.
2018
The language of stratified sets, Quine's NF, rewriting, and higher-order logic
20180508-fata
8 May 2018,
FATA seminar, Department of Computer Science, Glasgow University.
The language of stratified sets, Quine's NF, rewriting, and higher-order logic
20180508-fata
A somewhat meandering tour of some elementary and not-so-elementary results
8 May 2018
FATA seminar, Department of Computer Science, Glasgow University
Thanks to Jessica Ryan. See the announcement and abstract.
Topological nominal semantics
20180420-topns
20 April 2018,
OASIS seminar, Department of Computer Science, Oxford.
Topological nominal semantics
20180420-topns
Stone duality in a nominal universe.
20 April 2018
OASIS seminar, Department of Computer Science, Oxford
Thanks to Dan Marsden and Luke Ong. I outline two papers on algebraic and topological semantics for the lambda-calculus and first-order logic. See the announcement and abstract.
Equivariant ZFA with Choice (EZFAC)
20180413-arw
13 April 2018,
Automated Reasoning Workshop, Computer Lab, Cambridge.
Equivariant ZFA with Choice (EZFAC)
20180413-arw
I argue for EZFAC as a foundation for nominal techniques.
13 April 2018
Automated Reasoning Workshop, Computer Lab, Cambridge
Thanks to the organisers for this lovely event.
Here are the ARW conference proceedings, my poster, and my slides.
A longer paper is here.
Here are the ARW conference proceedings, my poster, and my slides.
A longer paper is here.
2017
Imaginary groups
20171101-imag
I visit the maths department.
1 November 2017
Maximals seminar, Heriot-Watt, Edinburgh
Thanks to the Maximals seminar series.
Technical writing
20170929-tecw
A seminar given to local MSc students, on technical writing.
9 September 2017
MSc course, Heriot-Watt, Edinburgh
2016
Consistency of Quine's NF using nominal techniques
20161109-conqnf
9 November 2016,
SPLS, University of Strathclyde, Glasgow.
Consistency of Quine's NF using nominal techniques
20161109-conqnf
Just a lovely, friendly event.
9 November 2016
SPLS, University of Strathclyde, Glasgow
Thanks to the SPLS, and to the Departmental Seminar series of Strathclyde.
Consistency of Quine's NF using nominal techniques
20160908-conqnf
8 September 2016,
Highlights Conference, Brussels.
Consistency of Quine's NF using nominal techniques
20160908-conqnf
My first time in Brussels. It seemed an extremly nice place and was surprisingly laid-back. The Highlights Conference was lovely and I will go next year (in London) if I can.
In spite of the similar title, this talk was not a pure repeat of my talks at the Logic Colloquium in August (see below).
8 September 2016
Highlights Conference, Brussels
In spite of the similar title, this talk was not a pure repeat of my talks at the Logic Colloquium in August (see below).
Thanks to the Highlights Conference 2016, and to Slawomir Lasota for inviting me to speak in his session.
Consistency of Quine's NF using nominal techniques
20160805-conqnf
5 August 2016,
Logic Colloquium, Leeds.
Consistency of Quine's NF using nominal techniques
20160805-conqnf
This was the second of two connected presentations; see next talk.
5 August 2016
Logic Colloquium, Leeds
Thanks to the Logic Colloquium, and to Nicola Gambino for being a gentleman.
What are variables of first-order logic and the lambda-calculus?
20160801-whavfo
1 August 2016,
Logic Colloquium, Leeds.
What are variables of first-order logic and the lambda-calculus?
20160801-whavfo
What a nice event the Logic Colloquium was. What a treat to be surrounded by people who care so much about logic I learned a lot.
1 August 2016
Logic Colloquium, Leeds
Thanks to the Logic Colloquium.
Nominal techniques and consistency of Quine's NF
20160531-lfcs
31 May 2016
LFCS, Edinburgh
Thanks to the LFCS Seminars series.
Nominal: the big picture
20160429-birmingham
29 April 2016
Birmingham University
Thanks to the Birmingham Theory Seminars.
Nominal foundations of mathematics
20160330-hw
30 March 2016
Heriot-Watt University, Edinburgh
Thanks to the Heriot-Watt Computer Science Seminar Series.
Consistency of Quine's NF using nominal techniques
20160224-kings
24 February 2016,
King's College London.
Consistency of Quine's NF using nominal techniques
20160224-kings
24 February 2016
King's College London
Thanks to the King's College London Informatics Research Colloquium Series.
2015
Consistency of Quine's NF using nominal techniques
20151028-manchester
28 October 2015,
University of Manchester.
Consistency of Quine's NF using nominal techniques
20151028-manchester
28 October 2015
University of Manchester
Thanks to the Manchester Logic Seminar series.
Consistency of Quine's NF using nominal techniques
20150529-logas
29 May 2015,
University of Cambridge.
Consistency of Quine's NF using nominal techniques
20150529-logas
29 May 2015
University of Cambridge
Thanks to the Logic and Semantics seminar series.
2014
Consistency of Quine's NF using nominal techniques
20141022-leeds-2
22 Oct 2014,
University of Leeds.
Consistency of Quine's NF using nominal techniques
20141022-leeds-2
See the announcement.
22 Oct 2014
University of Leeds
Thanks to the Leeds Logic Group.
What sequent quantifier rules tell us about nominal semantics for logic
20141022-leeds-1
22 Oct 2014,
University of Leeds.
What sequent quantifier rules tell us about nominal semantics for logic
20141022-leeds-1
A precis of parts of nominal semantics for predicate logic and semantics out of context.
22 Oct 2014
University of Leeds
Thanks to the Leeds Logic Group.
2013
Nominal duality theory for new, forall, and lambda
20131015-dagstuhl
15 Oct 2013,
Schloss Dagstuhl, Germany.
Nominal duality theory for new, forall, and lambda
20131015-dagstuhl
I was privileged to be invited to the rather wonderful Dagstuhl seminar 13422 on Nominal Computation Theory in Dagtuhl, Germany.
15 Oct 2013
Schloss Dagstuhl, Germany
Thanks to the organisers for this great event. Shall we do another one?
A (partial) survey of nominal techniques
20130918-strathclyde
18 Sep 2013,
University of Strathclyde, UK.
A (partial) survey of nominal techniques
20130918-strathclyde
Just as the title says!
18 Sep 2013
University of Strathclyde, UK
Thanks to Neil Ghani and his lively and interesting group for the very enjoyable afternoon.
An overview of nominal algebra, lattice, representation and dualities for computer science foundations
20130702-cambridge
2 Jul 2013,
Cambridge University, UK.
An overview of nominal algebra, lattice, representation and dualities for computer science foundations
20130702-cambridge
Presentation at the Logic and Semantics Seminar in the Computer Lab, Cambridge. I discuss how nominal algebra and powersets naturally model first-order logic with equality and the lambda-calculus. We can base theories of lattices, algebra, and topology on these observations, extending the familiar style of Boolean and Heyting algebras and their representations and topologies.
2 Jul 2013
Cambridge University, UK
Thanks to Jonathan Hayman.
Denotation of Contextual Modal Type Theory
20130701-cambridge
Presentation at the Programming Research Group Seminar in the Computer Lab, Cambridge. See also the associated paper Denotation of ... (a prize for the reader who guesses the rest of the title).
1 Jul 2013
Cambridge University, UK
Many thanks to Alan Mycroft and his team for being delightful and enthusiastic hosts.
Semantics of FOL and lambda-calculus using nominal techniques
201305-abramsky
30 May 2013,
Oxford University, UK.
Semantics of FOL and lambda-calculus using nominal techniques
201305-abramsky
Presentation at the Samson@60 conference in honour of Samson Abramsky.
30 May 2013
Oxford University, UK
Getting to this event was unusually challenging and so I have an unusually long list of kind, generous, and efficient people to thank for my being able to attend: thanks to Luke Ong, Prakash Pananganden, Dave Corne, and Destiny Chen.
An informal survey of nominal techniques
20130424-imdea
24 May 2013,
IMDEA, Madrid.
An informal survey of nominal techniques
20130424-imdea
I sketch recent activity in nominal techniques and speculate on how nominal techniques could be useful in verification. The talk was aimed especially those *not* familiar with nominal techniques. I gave the talk without slides.
24 May 2013
IMDEA, Madrid
Denotation of Contextual Modal Type theory
20130423-imdea
Nanevski in his PhD thesis introduced and studied Contextual Modal Theory Theory. This is a lambda-calculus based via the Curry-Howard correspondence on an extension of the modal logic S4 with multiple modalities, one for each variable. The application is to meta-programming, where the intuitive denotation of Box A is "syntax of type A".
The language itself is pretty, and we developed a denotational semantics with interesting properties. I will give a tour of the system and discuss future work. See also the paper on Denotations of CMTT.
23 May 2013
IMDEA, Madrid
Thanks to César Sánchez and Aleksandar Nanevski, and thanks to Paola Huerta for the calm and efficient rescue from that first hotel.
2012
Stone duality for first-order logic, a nominal approach
201208-duality
16 Aug 2012,
Oxford University, UK.
Stone duality for first-order logic, a nominal approach
201208-duality
Presentation at the Workshop on Duality Theory in Algebra, Logic and Computer Science in the Mathematical Institute, Oxford. See also the associated paper Stone duality for first-order logic: a nominal approach to logic and topology. This was a particularly nice do, and a lovely chance for me to rub shoulders with a new community.
16 Aug 2012
Oxford University, UK
One particular pleasure of the workshop was meeting a Polish academic who as a young man had studied with Mostowski. He told me some stories about the great man, and said how nice it was to see this mathematics being used.
Three semantics for logic out of context
20120711-thrslo
It is common to reason about semantics in a context. This context may be a valuation (assigning denotations to variables) or a typing context (assigning types to variables), or a memory state (enumerating known memory), and so on. I will outline a nominal approach to semantics which subsumes context into a more abstract nominal notion of support. Using this we can give three semantics to (first-order) logic: in lattices, sets, and algebras.
The full details are technical and in this talk I will try to bring out the non-technical “meaning of it all”, with an emphasis (necessarily speculative, but realistic) on practical implications to logic, specification, and programming.
11 Jul 2012
UPM, Madrid, Spain
The full details are technical and in this talk I will try to bring out the non-technical “meaning of it all”, with an emphasis (necessarily speculative, but realistic) on practical implications to logic, specification, and programming.
The algebraisation of logic using nominal techniques
20120620-tel-aviv
20 Jun 2012,
Tel-Aviv University, Israel.
The algebraisation of logic using nominal techniques
20120620-tel-aviv
Over the past five years a number of systems, such as first-order logic and the lambda-calculus, have been algebraically axiomatised using nominal techniques. A next step is to relate these (equational) axiomatisations to order-theoretic notions such as complemented bounded lattices (a.k.a. Boolean algebras). I will talk about recent progress here, giving an order-theoretic account of first-order logic: the punchline is that it will correspond to a complemented finitely fresh-complete lattice with a substitution—wait for the talk or see my recent paper with Dowek Nominal semantics for predicate logic: algebras, substitution, quantifiers, and limits.
20 Jun 2012
Tel-Aviv University, Israel
Israel has a tradition in logical foundations. Fraenkel--the Fraenkel of Zermelo-Fraenkel and Fraenkel-Mostowski set theory--was Dean of Jerusalem University. So it was special while visiting the logic community in Israel to discover not only that they already knew the background to what I was talking about, but that also, their research had anticipated much of what I was about to say. Special thanks here to Arnon Avron.
The application of symmetry to computing and meta-mathematics
20120617-bar-ilan
17 Jun 2012,
Bar-Ilan University, Tel-Aviv, Israel.
The application of symmetry to computing and meta-mathematics
20120617-bar-ilan
Symmetry has long been recognised as important in mathematics and physics, but its importance has been less appreciated in theories of logic and computation. In this (mathematically oriented, but non-technical) talk I describe what symmetry means in logic and computation, examine the benefits we can obtain by considering logic and computation as inherently “symmetric” mathematical entities, and relate this back to traditional foundations based on sets and functions.
17 Jun 2012
Bar-Ilan University, Tel-Aviv, Israel
Special thanks here to Stuart Margolis and the remarkable Plotkin family.
Nominal semantics for predicate logic
20120607-cilc
Presentation at the 9th Italian Convention on Computational Logic (CILC'2012) in Rome, Italy. See also the associated paper, which is called Nominal semantics for predicate logic.
7 Jun 2012
CILC, Rome, Italy
You are not a number: how nameless foundations took over the world and made us think we have only numbers, and no names.
20120229-aberdeen
29 Feb 2012,
University of Aberdeen, UK.
You are not a number: how nameless foundations took over the world and made us think we have only numbers, and no names.
20120229-aberdeen
Seminar at the School of Natural and Computing Sciences at the University of Aberdeen. I describe the nature of and motivation for nominal research.
29 Feb 2012
University of Aberdeen, UK
On proof-search
20120210-stp
Talk given at the mathematically structured programming group as part of the STP (Scottish Theorem Provers) meeting. I describe upcoming research to give a semantics to meta-variables in proof-search and theorem-proving.
10 Feb 2012
University of Strathclyde, UK
2011
Stone duality for first-order logic, a nominal approach
20111221-barringer
21 Dec 2011,
University of Manchester, UK.
Stone duality for first-order logic, a nominal approach
20111221-barringer
Given at the Howard Barringer workshop. Not a repeat of my talks at Paris or Edinburgh (see below), because I only had 20 minutes. Few technical details, much more discussion of the "conceptual stack" of nominal techniques and how I plan to develop the field. A very nice and interesting event with many varied speakers. The Festschrift is where the accompanying paper appears.
21 Dec 2011
University of Manchester, UK
Stone duality for first-order logic, a nominal approach
20111214-paris-gdt
14 Dec 2011,
INRIA, Paris, France.
Stone duality for first-order logic, a nominal approach
20111214-paris-gdt
A talk given at the work group on Types and Realisability / Théorie des types et réalisabilité". A repeat of my talk of the previous week in Edinburgh, but to a different audience (and getting a different set of very constructive comments). Interesting to present the same work to two different audiences and see the responses.
14 Dec 2011
INRIA, Paris, France
Stone duality for first-order logic, a nominal approach
20111206-edinburgh-lfcs
6 Dec 2011,
LFCS Edinburgh, UK.
Stone duality for first-order logic, a nominal approach
20111206-edinburgh-lfcs
Part of the LFCS seminar series in Edinburgh University. A brand-new duality result between appropriate nominal notions of topological space, and the nominal algebra axiomatisation of first-order logic from One-and-a-halfth order logic and Permissive-nominal logic.
6 Dec 2011
LFCS Edinburgh, UK
Getting to the Box of it: proof-theory for meta-programming and modal type theory
20111118-st-andrews
18 Nov 2011,
St Andrews University, UK.
Getting to the Box of it: proof-theory for meta-programming and modal type theory
20111118-st-andrews
Talk given at the wonderful Roy Dyckhoff retirement event. I present new work with Aleksander Nanevski to give a denotational semantics to Contextual Modal Type Theory (CMTT).
18 Nov 2011
St Andrews University, UK
Are all substitutions invertible; are all monoids groups?
20110923-areasi-birmingham
23 Sep 2011,
Birmingham University, UK.
Are all substitutions invertible; are all monoids groups?
20110923-areasi-birmingham
Talk given as part of the theoretical computer science seminars discussing how to injectively turn an arbitrary monoid into a group. Joint work with Peter Kropholler.
23 Sep 2011
Birmingham University, UK
Nominal semantics of the simply-typed lambda-calculus
20110826-nomhs-lfmtp
26 Aug 2011,
Nijmegen, Netherlands.
Nominal semantics of the simply-typed lambda-calculus
20110826-nomhs-lfmtp
Talk given at the 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011). Joint work with Dominic Mulligan.
26 Aug 2011
Nijmegen, Netherlands
An overview of nominal techniques, semantics, and logic
20110628-ovents-barcelona
28 Jun 2011,
IIIA, Barcelona, Spain.
An overview of nominal techniques, semantics, and logic
20110628-ovents-barcelona
Given at the Artificial Intelligence Research Institute (IIIA) in Barcelona, Spain. Does what it says on the tin. I gave the talk on the whiteboard; there are no slides.
28 Jun 2011
IIIA, Barcelona, Spain
Metamathematics based on nominal terms: first-order logics over nominal sets
20110419-metbnt-bctcs
19 Apr 2011,
Birmingham University, UK.
Metamathematics based on nominal terms: first-order logics over nominal sets
20110419-metbnt-bctcs
A talk given at British Colloquium for Theoretical Computer Science (BCTCS 2011) in Birmingham, UK. I discuss the application of nominal sets to designing metamathematical syntaxes.
19 Apr 2011
Birmingham University, UK
Metamathematics based on nominal terms and nominal logic: foundations of a nominal theorem-prover
20110411-metbnt-arw
4 Apr 2011,
ARW, Glasgow University, UK.
Metamathematics based on nominal terms and nominal logic: foundations of a nominal theorem-prover
20110411-metbnt-arw
A talk given in the Automated Reasoning Workshop in Glasgow University, UK. I describe permissive nominal terms and their application in logic and algebra.
4 Apr 2011
ARW, Glasgow University, UK
Nominal techniques: a success story of the continued relevance of mathematical foundations to computer science
20110323-nomtss
23 Mar 2011,
Glasgow University, UK.
Nominal techniques: a success story of the continued relevance of mathematical foundations to computer science
20110323-nomtss
A talk given at Glasgow University maths department. I discuss nominal techniques from a foundational point of view.
23 Mar 2011
Glasgow University, UK
A gentle introduction to the shape of nominal techniques
20110311-genisn
11 Mar 2011,
Strathclyde University, UK.
A gentle introduction to the shape of nominal techniques
20110311-genisn
The same beginner-friendly talk I gave in February. I gave the talk on the whiteboard; there are no slides.
11 Mar 2011
Strathclyde University, UK
A gentle introduction to the shape of nominal techniques
20110222-genisn
22 Feb 2011,
Glasgow University, UK.
A gentle introduction to the shape of nominal techniques
20110222-genisn
A beginner-friendly talk given at the University of Glasgow, UK on nominal techniques. The abstract and announcement are here. I gave the talk on the whiteboard; there are no slides.
22 Feb 2011
Glasgow University, UK
Nominal techniques, 2006-2011
20110216-nomt
16 Feb 2011,
Tel-Aviv Uni, Israel.
Nominal techniques, 2006-2011
20110216-nomt
Given at Tel-Aviv university. I broadly survey of the development of nominal terms in logic since 2006 when I last visited the department, discussing permissive-nominal algebra and permissive-nominal logic. I gave the talk on the whiteboard; there are no slides.
16 Feb 2011
Tel-Aviv Uni, Israel
2010
Tattered type theories: type theories with holes
20101124-stattt
24 Nov 2010,
University of Strathclyde, Glasgow, UK.
Tattered type theories: type theories with holes
20101124-stattt
Part of the fun in the afternoon series of meetings. I describe current work with Dominic Mulligan on representing incompleteness in theorem-provers.
24 Nov 2010
University of Strathclyde, Glasgow, UK
Thanks to Conor McBride.
Nominal techniques: logique, algèbre, calcul
20101116-nomtla
A talk given at the 16th meeting on Logic, Algebra, and Calculus at PPS in Paris, France. I talk about applications of nominal rewriting, algebra, and permissive-nominal logic to specifying and reasoning about logic, algebra, and calculus.
16 Nov 2010
PPS, Paris, France
Thanks to Delia Kesner and DIGITEO.
Nominal sets and the NEW-quantifier
20101007-nomsnq
A talk given at the Typical Seminar at the École Polytechnique in Paris, France. I describe recent work on a representation theorem for the NEW-quantifier.
7 Oct 2010
LIX, Paris, France
Thanks to Gilles Dowek and DIGITEO.
Permissive nominal logic and all that
20100903-pernla
Given at the 2010 British Logic Colloquium in Birmingham, UK. I describe in broad terms names and their symmetry properties.
3 Sep 2010
BLC, Birmingham, UK
Thanks to Eike Ritter.
Closed nominal rewriting and efficiently computable nominal algebra equality
20100714-clonre
14 Jul 2010,
LFMTP, Edinburgh, UK.
Closed nominal rewriting and efficiently computable nominal algebra equality
20100714-clonre
A talk given at the 5th International Workshop on Logical Frameworks and Meta-languages (LFMTP 2010) in Edinburgh, UK. I discuss the connection between nominal rewriting and nominal algebra. Joint work with Maribel Fernández.
14 Jul 2010
LFMTP, Edinburgh, UK
Kripke-style models in which logic and computation have equal standing
2010062-scott-in-scotland
29 Jun 2010,
Edinburgh University, UK.
Kripke-style models in which logic and computation have equal standing
2010062-scott-in-scotland
I discuss Kripke models of the untyped lambda-calculus at the lovely and exciting meeting in honour of Dana Scott.
29 Jun 2010
Edinburgh University, UK
PNL: Permissive-nominal logic
20100604-pernl
Given as part of the Computer Science Seminars in Leicester, UK. I discuss permissive-nominal logic; an extension of first-order logic with names and binding.
6 Jun 2010
University of Leicester, UK
Thanks to Alexander Kurz.
2009
Permissive nominal terms
20091120-pern
20 Nov 2009,
University of Edinburgh, UK.
Permissive nominal terms
20091120-pern
A talk given at the Scottish Theorem Proving meeting in Scotland, UK. I discuss permissive nominal terms. I used the whiteboard; there are no slides.
20 Nov 2009
University of Edinburgh, UK
Thanks Grant Passmore.
Names: I denote, therefore I am
20091111-namidt
A talk given at the SICSA Complex Systems Engineering Joint THREADSS/SEMANTICS Meeting in Scotland, UK. I discuss in general (philosophical?) terms some of the ideas and motivations underlying my research.
11 Nov 2009
Heriot-Watt University, Edinburgh, UK
Thanks to Phil Trinder.
Permissive nominal terms
20091020-pernt
20 Oct 2009,
IMDEA, Madrid, Spain.
Permissive nominal terms
20091020-pernt
A 30 minute ‘theory lunch’ seminar given at IMDEA in Madrid, Spain. I discuss permissive nominal terms. I used the whiteboard; there are no slides.
20 Oct 2009
IMDEA, Madrid, Spain
Thanks to Alejandro Sanchez.
Nominal techniques: a theory of names and binding
20091006-nomttnb
6-22 October 2009,
UCM, Madrid, Spain.
Nominal techniques: a theory of names and binding
20091006-nomttnb
A series of three 90 minute talks on nominal techniques given at the Universidad Complutense in Madrid, Spain. I used the whiteboard; there are no slides.
6-22 October 2009
UCM, Madrid, Spain
Thanks to Yolanda Ortega Mallen.
Permissive nominal terms and their unification
20090629-perntu
29 Jun 2009,
Università degli Studi di Ferrara, Italy.
Permissive nominal terms and their unification
20090629-perntu
A talk given at CILC09, the 24th Italian Conference on Computational Logic in Ferrara, Italy. See also the associated paper.
I discuss permissive-nominal terms, which are similar to nominal terms but with properties more like those of first-order syntax. In particular, permissive-nominal terms lack freshness contexts, have inherent notions of alpha-equivalence and ‘free atoms of’, and the notion of solution of a unification or matching problem is based just on substitution.
29 Jun 2009
Università degli Studi di Ferrara, Italy
I discuss permissive-nominal terms, which are similar to nominal terms but with properties more like those of first-order syntax. In particular, permissive-nominal terms lack freshness contexts, have inherent notions of alpha-equivalence and ‘free atoms of’, and the notion of solution of a unification or matching problem is based just on substitution.
Semantic Nominal Terms
20090322-taasn
A talk given at the 2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming in York, UK (a satellite event of ETAPS 2009). See also the associated paper. I discuss a semantics for nominal terms unknowns as ‘infinite streams of distinct atoms’. This reconciles atoms-abstraction with nominal terms. I also describe a form of substitution that is both capturing (as in nominal terms) and capture-avoiding (as in first-order syntax with binding) — at the same time.
22 Mar 2009
University of York, UK
2008
The laws of writing a good dissertation
20081022-lawwgd
22 Oct 2008,
Heriot-Watt University, Edinburgh, UK.
The laws of writing a good dissertation
20081022-lawwgd
I discuss technical writing for an audience of fourth year undergraduates, on Wednesday 22 October at 13:15. Oh, what are the laws of writing a good dissertation? Read the slides and find out, with examples!
22 Oct 2008
Heriot-Watt University, Edinburgh, UK
The nature of sets in computer science
20080929-natscs
A talk given at King's College as part of their Advanced Programming Techniques seminar series, on Monday 29 September at 12:00. I show how from a belief in the empty set and in ordinals we can construct a mathematical universe large enough that mathematical objects (in particular, numbers, rationals, and reals) can be interpreted in it. In response to questions from the audience I discuss the difference between structure (which exists in the model) and meaning (which exists in our own minds). It was a pretty good audience!
29 Sep 2008
King's College, London, UK
Nominal terms and one-and-a-half level Curry Howard
20080926-curhid
26 Sep 2008,
Cambridge University, UK.
Nominal terms and one-and-a-half level Curry Howard
20080926-curhid
A talk given at the Cambridge University computer lab as part of their Logic and Semantics seminar series, on Friday 26 September at 2pm. Joint work with Dominic Mulligan.
26 Sep 2008
Cambridge University, UK
Two-and-a-half order lambda-calculus
20080704-twoaah-wflp
Talk given on Friday 4 July in the WFLP 2008 in Italy at 10:00. I describe two-and-a-half order lambda-calculus, a two-level lambda-calculus. Normally, the lambda-calculus has a capture-avoiding substitution. The two-level lambda-calculus is actually two lambda calculi, with distinct namespaces for variable symbols of `strong' and `weak' variables, but sharing a common application operator. Substitution for a strong variable does not avoid capture by lambda-abstraction for a weak variable. This leads to interesting and unusual phenomena.
4 Jul 2008
University of Udine, Italy
Nominal Algebra
20080630-pisa
Talk given on Monday 30 June in the Pisa University Department of Informatics Seminar series in Italy at 17:30. I describe nominal algebra, a nominal algebraic reasoning language.
30 Jun 2008
Università di Pisa, Italy
Substitution for Fraenkel-Mostowski Foundations
20080404-aisb
Talk given on Friday 4 April in the AISB conference in Aberdeen at 17:30. I describe a substitution action defined for the atoms on Fraenkel-Mostowski sets (the general set theory version of nominal sets). In the original Gabbay-Pitts ‘nominal’ approach to modelling syntax, the atoms in Fraenkel-Mostowski set theory were used to model variable symbols. Since they have a substitution action, it may be that they can be used to model variables, as well. Joint work with Michael Gabbay.
The associated paper is here.
4 Apr 2008
Aberdeen University, UK
The associated paper is here.
One-and-a-halfth order Curry Howard: Incomplete Derivations
20080304-curhid
4 Mar 2008,
LIX, Paris, France.
One-and-a-halfth order Curry Howard: Incomplete Derivations
20080304-curhid
A talk given at the École Polytechnique on Tuesday 4 March at 11am. Joint work with Dominic Mulligan.
4 Mar 2008
LIX, Paris, France
Two-and-a-halfth order lambda-calculus: a calculus of the informal meta-level
20080207-twoaah-dsg
7 Feb 2008,
Heriot-Watt University, Scotland, UK.
Two-and-a-halfth order lambda-calculus: a calculus of the informal meta-level
20080207-twoaah-dsg
A talk given in the DSG (Dependable Systems Group) meeting. Joint work with Dominic Mulligan.
7 Feb 2008
Heriot-Watt University, Scotland, UK
Arbitrary objects in mathematics and semantics
20080228-arboms-arche
Talk delivered by Michael Gabbay in the Paris Arché workshop on abstract objects in semantics and the philosophy of mathematics on Thursday February 28. This talk was delivered by my co-author Michael Gabbay; a photo of Michael delivering the talk is online here. We connect relatively recent developments in Fraenkel-Mostowski sets and nominal style semantics, with existing philosophical thinking on arbitrary-ness and unknown entities in language, mathematics, and semantics. Joint work with Michael Gabbay.
The associated paper is here.
28 Feb 2008
Paris, France
The associated paper is here.
Strange but true! Second year undergraduates chat all night online about logic course
20080111-strbts
11 Jan 2008,
Heriot-Watt University, Scotland, UK.
Strange but true! Second year undergraduates chat all night online about logic course
20080111-strbts
A talk given as part of the Flexible Learning Talks series in Heriot-Watt University on Friday 11 January. Thanks to Nicole Cargill-Kipar.
11 Jan 2008
Heriot-Watt University, Scotland, UK
Semantics of names and binding
20080114-semnb-kings
A King's College London departmental colloquium given on January 14 at noon. I gave this talk the old-fashioned way on the blackboard; hence, no pdf slides online. It was good fun.
14 Jan 2008
King's College, London, UK
Thanks to Iman Poernomo.
2007
Nominal techniques: present, and future prospects
200711-tue
Given in the Prose seminar series at TU/e in Eindhoven on November 14 at 15:30. I talk about where I think things should be going.
14 Nov 07
TU/e, the Netherlands
The lambda context calculus
200707-lfmtp
Given at LFMTP, part of CADE07 near Bremen on July 15 at 17:00. Joint work with Stéphane Lengrand".
15 Jul 07
LFMTP, Bremen, Germany
a-logic with arrows
200706-wflp
Given at WFLP, part of RDP07 in Paris on June 25 at 11:00. Joint work with Michael Gabbay.
25 Jun 07
RDP, Paris, France
Resourceful truth: elementary models of resource-sensitive logics
200706-rest-2
15 Jun 07,
Edinburgh University, UK.
Resourceful truth: elementary models of resource-sensitive logics
200706-rest-2
A talk given at the LFCS logic and semantics club in Edinburgh University on June 15 at 13:00. Thanks to Bartek Klin.
15 Jun 07
Edinburgh University, UK
Resourceful truth: elementary models of resource-sensitive logics
200706-rest
4 Jun 07,
QMW, London, UK.
Resourceful truth: elementary models of resource-sensitive logics
200706-rest
A talk given at Queen Mary and Westfield New College on June 4 at 15:30. Thanks to Hongseok Yang.
4 Jun 07
QMW, London, UK
Names, computations, logics: the hole story.
200705-mattas
Given at the Mathematical Theories of Abstraction, Substitution and Naming in Computer Science in ICMS, Edinburgh on May 27 at 12:05. Thanks to the organisers Fernández, Pitts, and Stark. I describe my current take on ‘nominal techniques’.
27 May 07
ICMS, Edinburgh, UK
Strange but true! 2nd year undergraduates chat all night online about logic course.
20070518-strbts
18 May 07,
Heriot-Watt University, Edinburgh, UK.
Strange but true! 2nd year undergraduates chat all night online about logic course.
20070518-strbts
A talk given at the Flexible Learning Conference in Edinburgh at Heriot-Watt on May 18 at 14:05. I discuss my experience teaching the F22HO2 ‘formal specification’ course, and in particular the success of a message board I set up for the course, which attracted 1600 posts in five weeks and which remains active today. The video is the worst video in the history of worst videos. Sorry that I put the camera on the projector so it picked up the noise from the fan.
18 May 07
Heriot-Watt University, Edinburgh, UK
Fraenkel-Mostowski atoms model variables as well as names
200703-spls
8 Mar 07,
Edinburgh University, UK.
Fraenkel-Mostowski atoms model variables as well as names
200703-spls
A talk given at SPLS in Edinburgh on March 8 at 14:30. In this non-technical talk, we discuss a recent paper in which I exhibit a capture-avoiding substitution action on the Fraenkel-Mostowski sets universe. This suggests a new view of variables as denotational objects (names with a substitution action). Thanks to Kenneth MacKenzie.
8 Mar 07
Edinburgh University, UK
Names and variables
200702-city
A talk given at City University on February 27 at 12:00. We discuss our research intentions to investigate denotations in which names are first-class denotational citizens; why one might want to do this, and how we are doing it. Thanks to Artur Garcez.
27 Feb 07
City University, London, UK
Fraenkel-Mostowski atoms model variables as well as names
200702-hw
20 Feb 07,
Heriot-Watt University, Edinburgh, UK.
Fraenkel-Mostowski atoms model variables as well as names
200702-hw
A talk given at Heriot-Watt University on February 20 at 14:00. We discuss a recent paper in which I exhibit a substitution action on the Fraenkel-Mostowski sets universe. Thanks to Pierluigi Frisco.
20 Feb 07
Heriot-Watt University, Edinburgh, UK
2006
Boxology
2006-st-andrews
Given at St Andrew's University on December 19 at 11:00. We discuss boxology and hierarchical nominal techniques. Thanks to Kevin Hammond.
19 Dec 06
St Andrew's Uni, UK
Nominal Algebra: a NEW mathematics of variables
200612-lmu
A talk given at the LMU Institut für Informatik in Munich on December 6 at 16:00. We describe nominal algebra, its use to naturally represent meta-level reasoning on theories with binding, then concentrate on a nominal algebra axiomatisation of substitution and argue that ‘variable’ can be modelled as a ‘name plus substitution action’. Thanks to Martin Hofmann.
6 Dec 06
LMU, Munich, Germany
Substitution in Fraenkel-Mostowski sets
2006-cameleon
Given at the Centre for Mathematical Studies as part of the Cameleon meeting on December 2 at 16:00. We show how the model of names given by atoms in Fraenkel-Mostowski sets can be extended with a substitution action to a model of variables. Thanks to Thomas Forster.
2 Dec 06
Cambridge University, UK
Nominal Logic
2006-bath-noml
A talk given at the University of Bath Computer Science Department on November 13 at 11:15. We discuss nominal logic and the slogans ‘logic with names’ versus ‘logic with variables’. Thanks to Mark Price and Alessio Guglielmi.
13 Nov 06
University of Bath, UK
Logic of names and freshness (splitting the atom)
2006-dsg-lognfs
27 Oct 06,
Heriot-Watt University, Edinburgh, UK.
Logic of names and freshness (splitting the atom)
2006-dsg-lognfs
A talk given at the Dependable Systems Group weekly seminar at Heriot-Watt on October 27 at 14:15. We discuss what happens to the lambda binder in the presence of a hierarchy of variables.
27 Oct 06
Heriot-Watt University, Edinburgh, UK
The lambda-calculus
2006-lamc
A brief talk-ette (talk-chen, talk-ino) presented to test my presentation skills as part of the PGCAP course.
Oct 06
Heriot-Watt University, Edinburgh, UK
Nominal Algebra
2006-noma
Presented by my PhD student Aad Mathijssen in the 18th Nordic Workshop on Programming Theory (NWPT06) at Reykjavík University in Iceland. The corresponding abstract is here.
18 Oct 06
Reykjavík University, Iceland
Nominal techniques: evolving the atom
2006-stp-evoa
A talk given at the Scottish Theorem Proving meeting in the School of computer science. We give a position talk on nominal techniques considered useful as a means to generalise compositionality. Thanks to Phil Trinder and Rob Rothenberg.
13 Oct 06
University of St Andrews, UK
Incomplete objects using the NEW calculus of contexts
2006-dream-incoun
31 Aug 06,
Edinburgh University, UK.
Incomplete objects using the NEW calculus of contexts
2006-dream-incoun
Given at the DREAM workshop of the mathematical reasoning group at Edinburgh University on August 31. We speculate on higher-order logic in the NEW calculus of contexts.
31 Aug 06
Edinburgh University, UK
Hierarchical nominal rewriting
2006-lfmtp-hienr
Kindly presented on my behalf by James Cheney at LFMTP06 in Seattle, USA on Wednesday 16 August 2006 at 10:30.
16 Aug 06
LFMTP, Seattle, USA
One-and-a-halfth-order-logic
200607-oneaah
Presented at PPDP06 in Venice, Italy on Tuesday 11 July 2006 at 16:30.
11 Jul 06
PPDP, Venice, Italy
Concrete models of nominal algebra substitution
20060622-conmna
22 Jun 06,
CANS, King's College, London, UK.
Concrete models of nominal algebra substitution
20060622-conmna
Presented at the CANS seminar on Thursday 22 June 2006 at 3pm. Thanks to Maribel Fernández.
22 Jun 06
CANS, King's College, London, UK
Concrete models of nominal algebra substitution
20060613-conmna
13 Jun 06,
Edinburgh University, UK.
Concrete models of nominal algebra substitution
20060613-conmna
Presented at the CISA/LFCS seminar at Edinburgh University on Tuesday 13 June 2006 at 4pm in room 4.03. Thanks to Lucas Dixon. (See also a revised and extended version.)
13 Jun 06
Edinburgh University, UK
Evolved logic: the next step
2006-evoltn
Presented at the programming languages group in Tel-Aviv University at 14:00 on Sunday 28 May. Thanks to Mooly Sagiv.
28 May 06
Tel-Aviv University, Israel
Fraenkel-Mostowski sets and the new model of abstraction
2006tau4
28 May 06,
Tel-Aviv University, Israel.
Fraenkel-Mostowski sets and the new model of abstraction
2006tau4
Presented as part of a course in Tel-Aviv University at 12:00 on Sunday 28 May.
28 May 06
Tel-Aviv University, Israel
A NEW calculus of contexts
2006tau3
Presented as part of a course in Tel-Aviv University in 210 Schreiber at 12:00 on Sunday 14 May. Also see gabbay:newcc.
14 May 06
Tel-Aviv Univesity, Israel
On substitution
2006tau2
Presented as part of a course in Tel-Aviv University in 210 Schreiber at 10:30 on Thursday 11 May. Also see gabbay:capasn and gabbay:subaan.
11 May 06
Tel-Aviv University, Israel
Nominal algebra with applications
2006tau1
Presented as part of a course in Tel-Aviv University in 210 Schreiber at 10:30 on Thursday 4 May. Thanks to Nachum Dershowitz. Presented again at the Tel-Aviv University computer science departmental seminar at 10:00 on Tuesday 9 May. Only got half way through thanks to dilligent questioning; I will deliver the second half at 10:00 on Tuesday 16 May.
See papers gabbay:noma for the first half, and gabbay:onaah for the second.
9 & 11 May 06
See papers gabbay:noma for the first half, and gabbay:onaah for the second.
Nominal: an overview
200603-nomo
Presented at the Departmental Seminar at the Universidad Politecnica de Madrid on March 31. We give an overview of (one large part of) our research, focussing on ‘nominal’. Thanks to Manuel Hermenegildo, Juan-Jose Moreno, and Jim Lipton for the invitation to visit.
31 Mar 06
UPM, Madrid, Spain
Functional programming and unification with meta-variables
200603-funpum
31 Mar 06,
UPM, Madrid, Spain.
Functional programming and unification with meta-variables
200603-funpum
A research seminar given with the Babel group at the Universidad Politecnica de Madrid on March 31. We discuss our recent axiomatisation of substitution, and the NEW calculus of contexts, suggesting connections with logic programming and describing what we think might naturally be done next in this area. Thanks to Julio Marino.
31 Mar 06
UPM, Madrid, Spain
A concrete model of linearity and separation
200603-conmls
17 Mar 06,
Heriot-Watt University, Edinburgh, UK.
A concrete model of linearity and separation
200603-conmls
Presented at the Scottish Theorem Proving Meeting at Heriot-Watt University on March 17. We describe what we think is probably a uniform sets-based semantics for linear logic and bunched implications. Thanks to Andrew Ireland.
I repeated this talk as a research seminar with the Babel group at the Universidad Politecnica de Madrid on March 28 with title "A concrete semantics for truth in bunched implications and linear logic?". Thanks to Julio Marino.
17 Mar 06
Heriot-Watt University, Edinburgh, UK
I repeated this talk as a research seminar with the Babel group at the Universidad Politecnica de Madrid on March 28 with title "A concrete semantics for truth in bunched implications and linear logic?". Thanks to Julio Marino.
Is substitution an abstract notion?
200603-substitution
Departmental colloquium of March 13. We describe an axiomatisation of substitution in ‘nominal style’ and discuss its set-based semantics. Thanks to Iman Poernomo.
13 Mar 06
King's College, London, UK
Separation
200603-hw-separation
Departmental seminar given at Heriot-Watt on March 6. We report on joint work with Joe Wells in which we consider semantics for multiplicative and additive implication. Thanks to Lilia Georgieva.
6 Mar 06
Heriot-Watt University, Edinburgh, UK
A NEW semantics of substitution
200603-NEWss
Report on joint research carried out with two students, Samuel Rota Bulo and Andrea Marin, in the framework of a course taught in the University of Venice. Presented by the students on March 1. Thanks to their tutor Simonetta Balsamo.
1 Mar 06
Venice University, Italy
The NEW calculus of contexts
200602-spls
Talk given at the Scottish Programming Languages Seminar on February 1. We describe the NEW calculus of contexts, a lambda-calculus which tries to understand the meta-level/object-level split. Thanks to Edwin Brady. (I gave similar talks in Turin, Italy and at PPDP05.)
1 Feb 06
Glasgow University, Scotland, UK
Nominal techniques and the meta-level
200601-nomtml
Talk given at Venice University on January 24. In reaction to the question “So what is it that you do?”, I give an initially non-technical description of the motivations (as I see them) for that part of my work to date which has to do with nominal techniques. Thanks to Annalisa Bossi.
24 Jan 06
Venice University, Italy
Nominal Rewriting
200601-nomr
Talk given at the computational logic colloquium at Innsbruck University on January 23. We describe nominal rewriting as a meta-level framework for specifying rewriting, which accurately reflects the instantiation behaviour of meta-level variables with respect to object-level binding. We then expatiate way over the time limit on the general context of our research. Thanks to Aart Middeldorp for inviting me and to Georg Moser for making it happen.
23 Jan 06
Innsbruck University, Austria
The NEW calculus of contexts
200601-newcc
Talk given at the Turin workshop on implicit computational complexity on January 19. We describe the NEW calculus of contexts, a lambda-calculus which tries to understand the meta-level/object-level split. Thanks to Simona Ronchi della Rocca. (A corrected and slightly modified version of a talk given at PPDP05.)
19 Jan 06
Turin University, Italy
The Frankel-Mostowski (FM) model of abstraction applied to name-generation
200601-framma
9 Jan 06,
Heriot-Watt University, Edinburgh, UK.
The Frankel-Mostowski (FM) model of abstraction applied to name-generation
200601-framma
Given at the ULTRA group seminar at Heriot-Watt on January 9. We discuss the FM model of abstraction, and briefly suggest its usefulness for both inductive and coinductive types. Thanks to Lilia Georgieva.
9 Jan 06
Heriot-Watt University, Edinburgh, UK
2005
Automating first-order logic
200512-kings-autfol
Given at the second CANS meeting on December 6. We present Nominal Algebraic Specifications, a theory of universal algebra based on Nominal Terms and thus able to algebraically specify, in a suitable sense, theories-with-binding. We show how an algebraic theory of first-order logic leads to "one-and-a-halfth-order logic", which is above first-order logic and slightly to the side of second-order logic. We discuss proof-methods for the system and possible extensions. Thanks to Maribel Fernández.
6 Dec 05
King's College, London
One-and-a-halfth-order logic
200512-utrecht-oneaah
Given at the Institute for Logic, Language, and Computation, in their colloquium on mathematical logic. We present one-and-a-halfth-order logic, which is a logic somewhere above first-order logic and slightly to the side of second-order logic. It satisfies cut-elimination, has an algebraic presentation, and allows to quantify over all predicates in an interesting and unusual way. Thanks to Benedikt Loewe.
2 Dec 05
Utrecht University, Netherlands
Nominal Logic and FM techniques: reasoning about binding without pain
200511-radboud-noml
29 Nov 05,
Radboud University, Nijmegen, Netherlands.
Nominal Logic and FM techniques: reasoning about binding without pain
200511-radboud-noml
Given at the Foundations Group seminar of the Brouwer Institute in Radboud University in Nijmegen on November 29. We give a relatively technical sketch of FM techniques, Nominal Logic, and their application to reasoning on syntax-with-binding. Thanks to Henk Barendregt and Bas Spitters.
I gave the same talk at the Logic and Semantics Group Joint Theory seminar (‘Joint’ between Queen Mary and Westfield College and Imperial College) at Queen Mary and Westfield College on December 7 under the name "Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction". Thanks to Peter O'Hearn.
One member of the audience in Nijmegen then kindly invited me to give the talk again at the Theoretical Computer Science department in the Vrije Universiteit Amsterdam on December 12 (I used the original title). Thanks to Jan-Willem Klop and Femke van Raamsdonk.
29 Nov 05
Radboud University, Nijmegen, Netherlands
I gave the same talk at the Logic and Semantics Group Joint Theory seminar (‘Joint’ between Queen Mary and Westfield College and Imperial College) at Queen Mary and Westfield College on December 7 under the name "Fraenkel-Mostowski Techniques, a NEW model of freshness and abstraction". Thanks to Peter O'Hearn.
One member of the audience in Nijmegen then kindly invited me to give the talk again at the Theoretical Computer Science department in the Vrije Universiteit Amsterdam on December 12 (I used the original title). Thanks to Jan-Willem Klop and Femke van Raamsdonk.
a-logic
200511-amsterdam-alogic
Talk given in the Logic Tea series at the University of Amsterdam on November 22. We discuss a-logic, a first-order logic with a predicate atom which is true of variable symbols and false of non-variable symbol terms. We axiomatise the untyped lambda-calculus by way of example and discuss what models look like, some possible future work, and the design decisions (and some of the sins) hidden in the paper. Thanks to Johan van Benthem and Olivier Roy.
22 Nov 05
Amsterdam University, Netherlands
Nominal algebraic specifications
200511-nomas
Talk given at London South Bank University on November 8 and at University College London on November 9. We discuss Nominal Algebraic Specifications, an algebraic framework tailored to axiomatising systems-with-binding such as the lambda-calculus and logic. Thanks to Jonathan Bowen and Robin Hirsch.
8 Nov 05
South Bank University, London, UK
Nominal terms with a hierarchy of variables
200510-nomthv
Bleeding-edge talk given in Eindhoven in a group workshop on 31 October 2005. We give a speculative account of an algebraic version of the NEW calculus of contexts.
31 Oct 05
TU Eindhoven, Netherlands
Nominal Rewriting. Or ... talking about functions, without functions
200510-nomr
6 Oct 05,
Tel-Aviv University, Israel.
Nominal Rewriting. Or ... talking about functions, without functions
200510-nomr
Talk given at Tel-Aviv University on 6 October 2005. We give a non-technical account of Nominal Rewriting. Thanks to Arnon Avron and Nachum Dershowitz.
6 Oct 05
Tel-Aviv University, Israel
Nominal Rewriting
200508-nomr
Talk given at Leicester University on 9 August 2005. We discuss Nominal Rewriting and suggest why it and the methods underlying it are of interest.
9 Aug 05
Leicester University, UK
a-logic, the lambda-calculus, and internalising meta using names and binding
200507-munich
26 Jul 05,
LMU, Munich, Germany.
a-logic, the lambda-calculus, and internalising meta using names and binding
200507-munich
Talk given at LMU in Munich on 26 July 2005. We give a broad view of our research, mentioning a-logic and a whole load of other stuff.
26 Jul 05
LMU, Munich, Germany
Restart: a natural rule
200507-resnr
Talk given at South Bank University in London on 25 July 2005. We discuss Restart, a Natural Deduction rule which turns intuitionistic logic into classical logic, without affecting proof-normalisation.
25 Jul 05
South Bank University, London, UK
A NEW calculus of contexts
200507-newcc
Talk given at PPDP05 in Lisbon on 10 July 2005. We discuss a lambda-calculus with a hierarchy of variables of different ‘strengths’ (corresponding roughly to increasingly ‘meta’ variables). We find it to be remarkably expressive, and suggest that we can encode records, modules, objects, dynamic binding and rebinding, and many other constructs involving non-capture-avoiding substitution.
10 Jul 05
PPDP, Lisbon, Portugal
Extended Nominal Rewriting: two models of binding
200507-extnrt
Talk given at PPDP05 in Lisbon on 10 July 2005. We discuss two notions of binding which exist side-by-side in Extended Nominal Rewriting; one modelling lambda-calculus-like abstraction, the other modelling pi-calculus-like restriction. Some typos fixed with respect to the similar talk in Paris, and only 30 minutes long.
10 Jul 05
PPDP, Lisbon, Portugal
Extended Nominal Rewriting: two models of binding
200505-extnrt
Talk given at LIX, Ecole Polytechnique, France, on 24 May. Thanks to Dale Miller. We discuss two notions of binding which exist side-by-side in Extended Nominal Rewriting; one modelling lambda-calculus-like abstraction, the other modelling pi-calculus-like restriction.
24 May 05
LIX, Paris, France
Is there a quick way to get names and binding in some nominal sense up and running in Isabelle/HOL polymorphically on the type-class ‘type’, without having to rewrite the whole thing from scratch — yes or no?
200504-istqwt
24 Apr 05,
JAIST, Ishikawa, Japan.
Is there a quick way to get names and binding in some nominal sense up and running in Isabelle/HOL polymorphically on the type-class ‘type’, without having to rewrite the whole thing from scratch — yes or no?
200504-istqwt
Talk given at the Binding Challenges workshop in JAIST, Ishikawa, Japan. Thanks to Rene Vestergaard. We speculate on an interesting way in which it may be possible to encode syntax-with-binding in a higher-order logic based theorem-proving environment.
24 Apr 05
JAIST, Ishikawa, Japan
Aspects of Nominal Rewriting
200503-aspnr
Slides of a talk given at the CWI in Amsterdam on 2 March, and TUE in Eindhoven on 3 March. Thanks to Anton Wijs and MohammadReza Mousavi.
2 Mar 05
CWI, Amsterdam, Netherlands
A NEW calculus of contexts
200502-newcc
Slides of a talk given in INRIA Rocquencourt Paris, on 21 February, and PPS Paris, on 22 February. Thanks to James Leifer, Russ Harmer, and the people of PPS and INRIA.
21 Feb 05
Paris, France
<2005
One quantifier for forall and exists and generic elements or ... unknowns are data
200424-oneqfe
24 Nov 04,
King's College, London, UK.
One quantifier for forall and exists and generic elements or ... unknowns are data
200424-oneqfe
Slides of a talk given at the departmental colloquium on 24 November 2004.
24 Nov 04
King's College, London, UK
Nominal Unification
200409-nomu
Slides of a talk given in Imperial College, London, on 10 September 2004. Thanks to Stephen Muggleton.
10 Sep 04
Imperial College, London, UK
Nominal Rewriting Systems
20040826-nomr
Slides of a talk at PPDP04 on joint work with Maribel Fernández and Ian Mackie, given in Verona, Italy, on 26 August 2004. See also the paper.
26 Aug 04
PPDP, Verona, Italy
A Sequent Calculus for Nominal Logic
20040715-seqcnl
Slides of a talk at LICS04 on joint work with James Cheney, given in Turku, Finland, on 15 July 2004. See also the paper.
15 Jul 04
Turku, Finland
Fresh Logic
20040514-frelog
We discuss Fresh Logic (joint work with James Cheney) and consider its relation to FOLN a logic by Miller and Tiu, especially in the light of insights from implementation. Talk given to the PARCIFAL group at LIX on 14 May 2004.
14 May 04
LIX, Paris, France
Nominal Terms, Existential Variables, and Mathematics
20040504-nomtev
Talk given at PPS on 4 May 2004.
4 May 04
PPS, Paris, France
Extensions of Nominal Terms
20040311-extnt
We discuss extensions of Nominal Terms (see the paper on Nominal Unification). Lots of blue sky, but pretty.
11 Mar 04
Nominal Rewriting
200402-nomr
We present Nominal Rewriting, an essentially first-order rewriting system with inbuilt support for alpha-equivalence. See also "Incomplete lambda-terms" below. Talk given in LRI in their seminar series (27/2/2004, 10:30am).
27 Feb 04
LRI
Incomplete lambda-terms
200402-lamti
We use Nominal Rewriting to specify and discuss a lambda-calculus with meta-variables and explicit substitution. Talk given in LIX as part of a series of informal talks on meta-variables.
Feb 04
LIX, Paris, France
Restart as a Computational Rule
1203-restart
Talk given on applying the Curry-Howard correspondence to a novel Restart Logic. Given in the Workshop on Lambda Calculus, Type Theory, and Natural Language in King's College London, on 9 December at 12:00 on work.
9 Dec 03
King's College, London, UK
Fresh Logic: Vanilla First-Order Logic with FM?
0603-semantics-lunch
2 Jun 03,
Cambridge University, UK.
Fresh Logic: Vanilla First-Order Logic with FM?
0603-semantics-lunch
Talk given on Fresh Logic (a first-order logic for the NEW-quantifier with proof-normalisation) on 2 June at the local group's weekly Semantics Lunch. See also an abstract.
2 Jun 03
Cambridge University, UK
FM binding for pi-calculus transitions
0503-Lisbon-pi
Talk given on May 30 at Fundacao da Faculdade de Ciencias e Tecnologia / University of Lisbon. Thanks to Luis Caires and his department. See also an abstract.
30 May 03
Lisbon University, Portugal
FreshML: programming with binders made easy
0503-Lisbon-FreshML
28 May 03,
Lisbon University, Portugal.
FreshML: programming with binders made easy
0503-Lisbon-FreshML
Talk given on May 28 at Fundacao da Faculdade de Ciencias e Tecnologia / University of Lisbon. Thanks to Luis Caires and his department. See also an abstract.
28 May 03
Lisbon University, Portugal
FM and the pi-calculus
0303-Lyon
I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 20 at the ENS Lyon, France. Thanks to Daniel Hirschkoff. See also an abstract.
20 Mar 03
ENS Lyon, France
FM for Higher-Order Abstract Syntax
0303-manchester
I investigate what happens if we consider an FM-like category of objects with a finite name-for-name renaming action (possibly non-injective maps between names) rather than a finite name-for-name permutation action as is the case for FM sets. I obtain a category similar to Schan, but which supports a natural interpretation of weak HOAS. Talk given on March 13 in Manchester University, thanks to Peter Aczel. See also an abstract.
13 Mar 03
University of Manchester, UK
Restriction, binding, and three presentations of the pi-calculus
feb-sem-lunch
2 Mar 03,
Cambridge University, UK.
Restriction, binding, and three presentations of the pi-calculus
feb-sem-lunch
I've been using FreshML to program a pet interest of mine; transition systems and bisimulation checkers for the pi-calculus (see [gabbay:thempc]).
I'll show excerpts from the programs I've written and talk about what writing them has taught me about another interest of mine; finding a semantics for restriction as distinct from binding. The sourcecode discussed is the pi-ltsb series of programs above, see [pi-ltsb] above.
2 Mar 03
Cambridge University, UK
I'll show excerpts from the programs I've written and talk about what writing them has taught me about another interest of mine; finding a semantics for restriction as distinct from binding. The sourcecode discussed is the pi-ltsb series of programs above, see [pi-ltsb] above.
FM for Names and Binding
200212-jaist
Talk given on 11/12/2002 at the Japan Advanced Institute of Science and Technology, Ishikawa, on 14/12/2002 at MLG 2002 in Kinosaki, and on 16/12/2002 at ALGI in Kyoto. Thanks to René Vestergaard.
11 Dec 02
JAIST, Japan
Models of pi-calculus behaviour using FM techniques
200212-pisa
Talk given in Pisa on 2/12/2002. Thanks to Ugo Montanari.
2 Dec 02
Pisa University, Italy
Theory and Models of the pi-calculus using Fraenkel-Mostowski Generalised
200211-thempc
11 Nov 02,
Cambridge University, UK.
Theory and Models of the pi-calculus using Fraenkel-Mostowski Generalised
200211-thempc
Talk given in Cambridge on 11/11/2002 at the local group's “Semantics Lunch”.
11 Nov 02
Cambridge University, UK
FM Techniques for Syntax-with-Binding
200210-mpi
Talk given at the Max-Planck Institute, Saarbrücken, Germany.
24 Oct 02
MPI, Saarbrücken, Germany
FM Techniques for Syntax-with-Binding
200210-France
Talk given at INRIA Rocquencourt France 11/10/02 and Université Paris VII France 14/10/02. Thanks to Gilles Dowek and Pierre-Louis Curien.
11 & 14 Oct 02
INRIA, Paris, France
FM Techniques for Syntax-with-Binding
200210-IBM
Talk given at IBM Research, Haifa, Israel 2/10/02. Thanks to Cindy Eisner.
2 Oct 02
IBM Research, Haifa, Israel
FM-HOL
fmhotn
Contributed talk at Workshop on Thirty Five years of Automath, Informal Proceedings, Heriot-Watt University, Edinburgh, Scotland, April 2002.
Apr 02
Heriot-Watt University, UK