Entrance hall of the ICMS

Mathematical Theories of Abstraction, Substitution and Naming in Computer Science

May 26, 2007 - May 28, 2007

ICMS, 14 India Street, Edinburgh

Organisers

Name Institution
Fernandez, Maribel King's College London
Pitts, Andrew University of Cambridge
Stark, Ian University of Edinburgh

Short Report

Mathematical treatments of concrete syntax (using strings, trees and directed graphs) have always been a central concern for that part of computer science to do with symbolic computation, programming language implementation and computer-aided reasoning. However, it has proved much harder to find useful theories of abstract syntax which address the structural properties common to all high-level semantics of formal languages, especially those properties that have to do with substituting structures for variables, delimiting the scope of names, and sharing common substructures. The workshop brought together a varied group of 38 researchers, some of whom have recently created new mathematical models for abstract syntax, substitution and naming (using various kinds of category theory, set theory and computational logic) and some of whom are building computer systems for symbolic computation and proof based on those theories.

The workshop was 86% funded by ICMS (EPSRC and LMS grants) and 14% funded by the EPSRC project Computational Applications of Nominal Sets (CANS), run jointly by Cambridge and King's College London.

Participants list and links to available presentations are further down this page.

Download the pdf file of the full report

Original Details

The main purpose of the workshop is to bring together researchers who are applying logic, category theory and set theory to the study of the abstract syntax and semantics of computer languages and systems for symbolic computation and proof. We are particularly keen to present and compare the presheaf and the nominal sets approaches to abstraction, substitution and naming. We aim to have graduate-level tutorials on each approach and to stimulate a better understanding of the relationships between them. We also hope to stimulate discussion of the following specific topics:

  1. Enriched Lawvere theories involving namebinding, the equational part of nominal logic and extensions of Plotkin-Turi functorial SOS to encompass binders.
  2. The relationship of nominal and presheaf models to the logic of bunches, and to logical frameworks and dependent types.
  3. Denotational semantics (particularly game semantics) using presheaf categories and using nominal sets.
  4. The relationship of nominal and presheaf techniques to work on computational models that take haring into account, e.g. term graphs and bigraphs.

We will also address the strengths and weaknesses of these works for various application domains: computational logic, program language design, and mechanised theorem proving.

Arrangements

Venue
The Workshop will be held at the head-quarters of ICMS at 14 India Street. This house is the birthplace of James Clerk Maxwell and is situated in the historic New Town of Edinburgh, very near the centre. The seminar room is fully equipped with large whiteboards, overhead and data projectors. Other facilities include PCs, wireless network and rooms suitable for small discussion meetings.

The ICMS travel pages show the location of India St and have links to pages with advice on how to get to Edinburgh and travel around once here.

Registration etc
Registration will be from 15.30-17.30 on Friday 25, followed by a reception with wine and nibbles. The talks will start at 09.00 on Saturday 26 and the workshop will end at 17.00 on Monday 28.

Accommodation
ICMS will arrange rooms in local guest houses for those who require it. Participants are also free to make their own arrangements and may claim back the cost, with receipts, up to a maximum of £55 per night for bed and breakfast. A list of Edinburgh accommodation of various sorts and prices is available here. Sections 1-3 are particularly relevant.

Meals and Refreshments
Morning and afternoon refreshments will be provided throughout the Workshop. A sandwich lunch will be supplied on Saturday, Sunday and Monday. There will be a wine reception on Friday evening and the Workshop Dinner at 20.30 on Saturday evening.

Under the terms of our EPSRC funding we are required to charge a £30 registration fee to cover costs not admissible under the grant. This is usually payable during the meeting and a receipt will be provided.

Further information will be provided in the Invitation Letter.

Programme

Untitled Document Friday 25 May 2007
15.30-17.30 Registration desk open
17.30-19.00 Reception with wine and nibbles

Saturday 26 May 2007

08.55-09.00 Welcome
09.00-10.30 Marcelo Fiore (University of Cambridge)
A mathematical theory of substitution and its applications to syntax and semantics (tutorial)
10.30-11.15 Coffee
11.15-11.45 Dale Miller (École Polytechnique)
Bindings, mobility of bindings and the nabla quantifier Presentation
11.50-12.20 Ulrich Schoepp (LMU München)
Categories with binding structure Presentation
12.25-12.55 Sam Staton (University of Cambridge)
Models of substitution and models of structural operational semantics
12.55-14.30 Lunch
14.30-15.30 Jean-Pierre Jouannaud (École Polytechnique)
Confluence properties of higher-order rewriting relations (invited talk)
15.30-16.15 Tea
16.15-16.45 Gilles Dowek (École Polytechnique)
Super-consistency, normalization and cut elimination Presentation
16.50-17.20 Vincent van Ostrom (Universiteit Utrecht)
Names and higher-order rewriting Presentation
20.30 Workshop dinner, First Coast, Dalry Road

Sunday 27 May 2007

09.00-10.30 James Cheney (University of Edinburgh)
Reasoning and programming with nominal logic (tutorial) Presentation
10.30-11.15 Coffee
11.15-11.45 Alwen Tiu (Australian National University)
Proof systems for reasoning about generic judgements Presentation
11.50-12.20 David Baelde (École Polytechnique)
Bedwyr, a proof-search approach to model-checking Presentation
12.25-12.55 Jamie Gabbay (Heriot-Watt University)
Names, computations, logics the hole story Presentation
12.55-14.30 Lunch
14.30-15.00 Stefan Berghofer (TU Munich)
An overview of the nominal datatype package in Isabelle/HOL Presentation
15.05-15.35 Christian Urban (TU Munich)
Formalizations using the nominal datatype package Presentation
15.35-16.20 Tea
16.20-16.50 Aad Mathijssen (Eindhoven University of Technology)
A formal calculus for informal equality with binding Presentation
16.55-17.25 Ranald Clouston (University of Cambridge)
Nominal equational logic Presentation

Monday 28 May 2007

09.00-09.30 François Pottier (INRIA)
Static name control for FreshML Presentation
09.35-10.05 Martin Hyland (University of Cambridge)
Comparing generalised algebraic structure
10.05-10.45 Coffee
10.45-11.15 Ian Mackie (École Polytechnique and King's College London)
Graph representations of binders Presentation
11.20-11.55 Marino Miculan (University of Udine)
Bigraphical models of calculi with names Presentation
12.00-12.30 Nikos Tzevelekos (University of Oxford)
Full abstractions for nominal general references tzevelekos.pdf
12.30-14.30 Lunch
14.30-15.30 Gordon Plotkin (University of Edinburgh)
An algebraic framework for logics and type theories (invited talk) Presentation
15.30-16.15 Tea
16.20-16.50 Nick Benton (Microsoft Research Limited)
High level types and low level logic
17.00 Finish

Presentations:

Presentation Details
Baelde, David
Bedwyr, an proof-search approach to model-checking
View Abstract Down
Benton, Nick
High level types and low level logic
View Abstract Down
Berghofer, Stefan
An overview of the nominal datatype package in Isabelle/HOL
View Abstract Down
Cheney, James
Reasoning and programming with nominal logic
View Abstract Down
Clouston, Ranald
Nominal equational logic
View Abstract Down
Dowek, Gilles
Super-consistency, normalization and cut elimination
View Abstract Down
Gabbay, Jamie
Names, computations, logics: the hole story.
View Abstract Down
Jouannaud, Jean-Pierre
Confluence properties of higher-order rewriting relations
View Abstract Down
Mackie, Ian
Graph representations of binders
View Abstract Down
Mathijssen, Aad
A formal calculus for informal equality with binding
View Abstract Down
Miculan, Marino
Bigraphical models of calculi with names
View Abstract Down
Miller, Dale
Bindings, mobility of bindings, and the nabla-quantifier
View Abstract Down
Plotkin, Gordon
An algebraic framework for logics and type theories
View Abstract Down
Pottier, François
Static Name Control for FreshML
View Abstract Down
Schoepp, Ulrich
Categories with Binding Structure
View Abstract Down
Staton, Sam
Models of Substitution and Models of Structural Operational Semantics
View Abstract Down
Tiu, Alwen
Proof Systems for Reasoning about Generic Judgments
View Abstract Down
Tzevelekos, Nikos
Full abstraction for nominal general references
View Abstract Down
Urban, Christian
Formalisations using the nominal datatype package
View Abstract Down
van Oostrom, Vincent
Names and higher-order rewriting
View Abstract Down

Participants

Name Institution
Baelde, David École Polytechnique
Benton, Nick Microsoft Research Limited
Berghofer, Stefan TU Munich
Calves, Christophe King's College London
Cheney, James University of Edinburgh (local participant - attending talks only)
Clouston, Ranald University of Cambridge
Crole, Roy University of Leicester
Dowek, Gilles École Polytechnique
Fernandez, Maribel King's College London
Fiore, Marcelo University of Cambridge
Gabbay, Jamie Heriot-Watt University
Hind, Ianthe Heriot-Watt University
Hyland, Martin University of Cambridge
Jouannaud, Jean-Pierre École Polytechnique
Lakin, Matthew University of Cambridge
Mackie, Ian Ecole Polytechnique and King's College London
Mathijssen, Aad Eindhoven University of Technology
Miculan, Marino University of Udine
Miller, Dale École Polytechnique
Mogelberg, Rasmus University of Edinburgh
Momigliano, Alberto University of Edinburgh
Pitts, Andrew University of Cambridge
Plotkin, Gordon University of Edinburgh
Pollack, Randy University of Edinburgh
Pottier, François INRIA
Power, John University of Edinburgh
Price, Mark University of Bath
Pym, David HP Labs
Sato, Shinya King's College London
Schoepp, Ulrich LMU München
Schuermann, Carsten IT University of Copenhagen
Stark, Ian University of Edinburgh
Staton, Sam Computer Laboratory, University of Cambridge
Tiu, Alwen Australian National University
Turner, David University of Cambridge
Tzevelekos, Nikos University of Oxford
Urban, Christian TU Munich
van Oostrom, Vincent Universiteit Utrecht