ICMS

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 Hide Abstract
Bedwyr is an extended logic programming language that is capable of model-checking based reasoning over syntactic expressions involving bindings. It embodies two important recent observations about proof search: (1) It is possible to formalize both finite success and finite failure in a sequent calculus; proof search in such a proof system can capture both may and must behavior in operational semantics specifications. (2) Higher-order abstract syntax can be supported at a logical level by using term-level lambda-binders, the nabla-quantifier, higher-order pattern unification, and explicit substitutions; these features allow reasoning directly on expressions containing bound variables. Bedwyr was released recently, with examples for several flavours of (finite) pi-calculus (operational semantics, bisimulation, trace analysis, modal logic), lambda-calculus, winning strategies for games, etc.
Benton, Nick
High level types and low level logic
View Abstract Hide Abstract
Abstract to follow
Berghofer, Stefan
An overview of the nominal datatype package in Isabelle/HOL
View Abstract Hide Abstract
The proof assistant Isabelle/HOL has recently been extended with a package allowing the introduction of nominal datatypes. According to the design philosophy of HOL, this introduction is done in a completely definitional way, i.e. the properties of nominal datatypes are derived from already existing concepts, rather than just adding them in an axiomatic way. We give an overview of the architecture of this package and describe its most important features, in particular the derivation of a strong induction rule as well as a the construction of a recursion combinator for defining primitive recursive functions on nominal datatypes. The nominal datatype package is joint work with Christian Urban.
Cheney, James
Reasoning and programming with nominal logic
View Abstract Hide Abstract
Nominal logic is an extension of first-order logic with an axiomatization of alpha-equivalence and freshness constraints which is sufficient for reasoning about abstract syntax trees with both free and bound names as well as name-generation. It therefore provides a rigorous foundation for many informal conventions used by logicians and computer scientists when performing metatheoretic reasoning about object languages. Thus, automated reasoning and programming techniques based on nominal logic, if fully developed, could play a central role in providing rigorous automated support for studying programming languages comparable to that currently provided by computer algebra systems, model checkers, and theorem provers for numerical and algebraic problems. In this tutorial, I will introduce the key concepts of nominal logic from the point of view of mathematical logic, including the proof theory and model theory. I will also show how these concepts provide a solid foundation for logic programming with names, binding, and generativity, including a discussion of key algorithms needed for logic programming and other automated deduction techniques based on nominal logic.
Clouston, Ranald
Nominal equational logic
View Abstract Hide Abstract
Abstract to follow
Dowek, Gilles
Super-consistency, normalization and cut elimination
View Abstract Hide Abstract
Super-consistency is a semantic property of a theory that implies proof normalization and cut elimination. We will present two proofs of cut elimination for super-consistent theories and discuss their differences.
Gabbay, Jamie
Names, computations, logics: the hole story.
View Abstract Hide Abstract
We propose denotations, logics, and systems for computation, with enriched notions of naming. For example; "a name enriched with a substitution action, is a variable". Thus complexity can be added by enriching *names*; as well as by adding term-formers/predicates/connectives. This raises new and interesting mathematical questions, and uncovers new expressivity in old friends in computer science which use names, from unification to lambda-calculi to logic.
Jouannaud, Jean-Pierre
Confluence properties of higher-order rewriting relations
View Abstract Hide Abstract
Abstract to follow
Mackie, Ian
Graph representations of binders
View Abstract Hide Abstract
In this talk I will discuss graph representations of the lambda calculus and extensions to more general systems with patterns. These graphs provide an alternative perspective for reasoning about languages with binders.
Mathijssen, Aad
A formal calculus for informal equality with binding
View Abstract Hide Abstract
In informal mathematical usage one often reasons with binding. This often takes place in an equational setting; examples are (lambda x.t)[y -> u] = lambda x.(t[y -> u]), if x does not occur free in u; P => (forall x.Q) = forall x.(P => Q), if x does not occur free in Q. Here meta-variables t, P and Q occur in a so-called freshness context (``if x does not occur free in''), which makes a direct algebraic treatment impossible. I will present a calculus of equality that allows a direct formalisation of assertions such as the above. Support for binding, meta-variables and freshness is built-in. This is joint work with Murdoch J. Gabbay. Papers and slides of previous talks may be found at http://www.win.tue.nl/~amathijs
Miculan, Marino
Bigraphical models of calculi with names
View Abstract Hide Abstract
Bigraphs are an emerging metamodel for representing and reasoning about various aspects of concurrency. In this talk I will discuss the application of directed bigraphs, a variant of bigraphs previously introduced by the authors, to languages with different kinds of binders. One of the benefits of using the bigraphical metamodel, is that it supports a general and uniform construction of bisimulation, which is guaranteed to be a congruence. We will describe the encoding methodology, by means of some paradigmatic examples such as the lambda-calculus, the fusion calculus and the nu-calculus.
Miller, Dale
Bindings, mobility of bindings, and the nabla-quantifier
View Abstract Hide Abstract
We present a logic that contains a new quantifier $nabla$ and fixed points. We illustrate the uses of this logic and quantifier on some operational semantic specifications, including the specification of the finite $pi$-calculus. The $nabla$ quantifier helps with the delicate issues surrounding the scope of variables within $pi$-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no-side conditions concerning names of bindings while maintaining a completely formal treatment of such bindings; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.
Plotkin, Gordon
An algebraic framework for logics and type theories
View Abstract Hide Abstract
It seems a natural principle to seek logical frameworks that are as simple and as weak as possible while still enabling direct natural representations of a wide variety of formalisms. We present an algebraic framework, which can be considered an extension of multi-sorted equational logic with functionals and dependent types, but with no ability to form compound types (= sorts) and no lambda-abstraction or application. Abstraction enables the representation of binding mechanisms; dependent types enables, for example, the representation of the proofs of a formula. We present the system as a combination of two simpler subsystems: one with only parameterisation and one with only dependent sorts. We conjecture our system (without equations) is equivalent to the system SPar(2) in [Ada]; it is noteworthy that that too has second-order abstraction and dependent types but no lambda-abstraction or application. Regarding comparison with systems of typed lambda-calculi, we conjecture our system is equivalent to restricting lambda_Pi with beta-eta-equality to its second-order fragment , and, in terms of presentation, to such a system with all terms kept in beta-eta-normal form and hereditary substitution replacing reduction, see [Har,Wat]. The restrictions make for a simpler syntactic and also, we conjecture, semantic meta-theory while sacrificing little, if anything, in representational power to lambda_Pi. References [Ada] R. Adams. A Modular Hierarchy of Logical Frameworks. In Stefano Berardi, Mario Coppo, Ferruccio Damiani (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2003 <http://types2003.di.unito.it/>, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. LNCS 3085. Springer, 2004. 1-16. [Har] R. Harper & D. R. Licata. Mechanizing Language Definitions Submitted to J. Functional Programming, 2006. [Wat] K. Watkins, I. Cervesato, F. Pfenning & D. Walker (2002). A concurrent logical framework I: Judgments and properties. Tech. rept. CMU-CS- 02-101. Department of Computer Science, Carnegie Mellon University. Revised May 2003.
Pottier, François
Static Name Control for FreshML
View Abstract Hide Abstract
FreshML extends ML with constructs for declaring and manipulating abstract syntax trees that involve names and statically scoped binders. It is impure: name generation is an observable side effect. In practice, this means that FreshML allows writing programs that create fresh names and unintentionally fail to bind them. Following in the steps of early work by Pitts and Gabbay, I will present Pure FreshML, a subset of FreshML equipped with a static proof system that guarantees purity. Pure FreshML relies on a rich binding specification language, on user-provided assertions, expressed in a logic that allows reasoning about values and about the names that they contain, and on a conservative, automatic decision procedure for this logic. I will argue that Pure FreshML can express non-trivial syntax-manipulating algorithms.
Schoepp, Ulrich
Categories with Binding Structure
View Abstract Hide Abstract
Categories with binding structure are a simple categorical axiomatisation of name binding. The definition of binding structure can be seen as a direct formalisation of the statement: ‘Working with an alpha-equivalence class is the same as working with a freshly named instance.' This statement, which expresses that two modes of working are equivalent, is being formalised directly as an equivalence of categories. Categories with binding structure have rich structure that includes and generalises well-known semantic constructions for name binding. Among the instances of categories with binding structure are the category of nominal sets and the category of species of structures. In the case for nominal sets, binding structure contains a direct universal characterisation of well-known constructions, such as the new-quantifier, abstraction sets and the unique choice of new names. In the case for species of structures, binding structure can be used to model the nabla-quantifier of Miller and Tiu. The purpose of this talk is to introduce categories with binding structure, to explain their structure and how they relate to existing models of name binding.
Staton, Sam
Models of Substitution and Models of Structural Operational Semantics
View Abstract Hide Abstract
Abstract to follow
Tiu, Alwen
Proof Systems for Reasoning about Generic Judgments
View Abstract Hide Abstract
In this talk I will present several systems for encoding and reasoning about object systems with bindings. These systems are extensions of the proof system "FOLD-nabla" of Miller and Tiu, with an induction principle. The logic "FOLD-nabla" is itself an extension of intuitionistic logic with fixed points and a 'generic quantifier', nabla, which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOLDN-nabla with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on nabla, in particular those concerning the permutation and the weakening of the "generic context'' used in FOLDN-nabla. In one of the extensions, I will show that by adopting a notion of generic names and the equivariance principle (i.e., provability is preserved under permutation of names), the presentation of the extended logic can be much simplified. All these extended systems admit cut-elimination. I will illustrate the use of these systems in reasoning about properties of an object logic and a simply typed lambda-calculus.
Tzevelekos, Nikos
Full abstraction for nominal general references
View Abstract Hide Abstract
Game semantics has been used with considerable success in formulating fully abstract semantics for languages with higher-order procedures and a wide range of computational effects. Recently, nominal games have been proposed for modeling functional languages with names. These are ordinary games cast in the theory of nominal sets developed by Pitts and Gabbay. Here we take nominal games one step further, by developing a fully abstract semantics for a language with nominal general references.
Urban, Christian
Formalisations using the nominal datatype package
View Abstract Hide Abstract
Abstract to follow
van Oostrom, Vincent
Names and higher-order rewriting
View Abstract Hide Abstract
Abstract to follow

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	MACS, 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