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:
- Enriched Lawvere theories involving namebinding, the equational part of nominal logic and extensions of Plotkin-Turi functorial SOS to encompass binders.
- The relationship of nominal and presheaf models to the logic of bunches, and to logical frameworks and dependent types.
- Denotational semantics (particularly game semantics) using presheaf categories and using nominal sets.
- 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 200715.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 | |
Benton, Nick | |
High level types and low level logic | |
View Abstract | |
Berghofer, Stefan | |
An overview of the nominal datatype package in Isabelle/HOL | |
View Abstract | |
Cheney, James | |
Reasoning and programming with nominal logic | |
View Abstract | |
Clouston, Ranald | |
Nominal equational logic | |
View Abstract | |
Dowek, Gilles | |
Super-consistency, normalization and cut elimination | |
View Abstract | |
Gabbay, Jamie | |
Names, computations, logics: the hole story. | |
View Abstract | |
Jouannaud, Jean-Pierre | |
Confluence properties of higher-order rewriting relations | |
View Abstract | |
Mackie, Ian | |
Graph representations of binders | |
View Abstract | |
Mathijssen, Aad | |
A formal calculus for informal equality with binding | |
View Abstract | |
Miculan, Marino | |
Bigraphical models of calculi with names | |
View Abstract | |
Miller, Dale | |
Bindings, mobility of bindings, and the nabla-quantifier | |
View Abstract | |
Plotkin, Gordon | |
An algebraic framework for logics and type theories | |
View Abstract | |
Pottier, François | |
Static Name Control for FreshML | |
View Abstract | |
Schoepp, Ulrich | |
Categories with Binding Structure | |
View Abstract | |
Staton, Sam | |
Models of Substitution and Models of Structural Operational Semantics | |
View Abstract | |
Tiu, Alwen | |
Proof Systems for Reasoning about Generic Judgments | |
View Abstract | |
Tzevelekos, Nikos | |
Full abstraction for nominal general references | |
View Abstract | |
Urban, Christian | |
Formalisations using the nominal datatype package | |
View Abstract | |
van Oostrom, Vincent | |
Names and higher-order rewriting | |
View Abstract |
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 |