Bologna Workshop
24-26 March 1997

Contents:

• Accomodation.
• Workshop.
• How to reach ...
• List of Participants.
• Programme.
• Abstracts of the talks.

Accomodation.

Workshop.

How to reach...

• Getting From the Airport to the City Center.
• General Informations on Busses.
• Residenza Universitaria "S.Giovanni in Monte".
• Dipartmento di Matematica.

• Special "Aerobus" service. The bus runs from 06.30 to 23.20 at about 30-minute intervals and makes only 4 stops in the city center (including the train station) and continues on to the trade fair district. Tickets may be purchased on board.
  In order to reach the "Residenza Universitaria", the best is to stop in Piazza Maggiore, i.e. the very center of Bologna (ask the driver). Then either walk (~10 m.), or get the bus n.13. Leave the bus at its second stop (just after P.zza S.Stefano). Coming back along Via S.Stefano, you immediately find Via Cartoleria. Take it; the first road on your right is Via de'Chiari.
• Regular city bus service. Bus 91B leaves from the airport arrival area and follows a course similar to that of the Aerobus, except making far more frequent stops.
• Taxi. The trip takes around 15 minutes (barring traffic jams) and should cost around 25000 Lire.

List of Participants.

Programme.

• Monday
  
  
  • 9.00 Welcome.
  • 9.10 - 9.50 G.Boudol. The pi-calculus in direct style.
  • 9.50 - 10.30 J.Parrow. Pieces of pi: substitution and scoping.
    
    
  • 11.10 - 11.50 M.Hennessy. A denotational Model for a subset of Core Facile.
  • 11.50 - 12.30 U. Nestmann. Encoding Mixed-guarded Choice.
    
    
  • 14.30 - 15.10 R.Amadio. An asynchronous model of locality, failure, and process mobility.
  • 15.10 - 15.50 J.Riely. Distributed Processes and Location failures.
    
    
  • 16.30 - 17.10 G.Ferrari. Locality based Linda: programming with explicit localities.
  • 17.10 - 17.50 P.Gardner. From Action Calculi to Linear Logic.
  
  
  
• Tuesday
  
  
  • 9.10 - 9.50 J.W.Klop. Sequentiality in lambda calculus and PCF via origin tracking.
  • 9.50 - 10.30 P.Mellies. A Factorisation Theorem for external derivations
    
    
  • 11.10 - 11.50 R.Bruni. Zero Safe Nets.
  • 11.50 - 12.30 O.H.Jensen. Graph rewriting and labelled transition semantics.
    
    
  • 14.30 - 15.10 P.Sewell. Local Channel Typing for a distributed pi-calculus.
  • 15.10 - 15.50 D.Sangiorgi. Interpreting Typed Object calculi into typed pi-calculus.
    
    
  • 16.30 - 17.10 D.Remy. Implicit typing a la ML for the join calculus.
  • 17.10 - 17.50 L.Maranget. The implementation fo the join calculus.
  
  
  
• Wednesday
  
  
  • 9.10 - 9.50 V.Danos. Distributed functional evaluation.
  • 9.50 - 10.30 L.Regnier. GOI and coherent semantics
    
    
  • 11.10 - 11.50 P.Baillot. AJM game semantics for classical LL.
  • 11.50 - 12.30 A.Asperti. P = NP, up to sharing.

Abstracts of the talks.

• Peter Sewell. "Local Channel Typing for a Distributed pi-calculus".
  Abstract:
  In the distributed setting there are essential differences (in performance and failure behaviour) between local and global communication. Nonetheless, as far as possible, a programming language for distributed migratory computation should allow the two to be accessed uniformly.
  I'll give a distributed pi-calculus, which might be used as a partial basis for a distributed Pict-like language, and its structural congruence/reduction semantics. It integrates location and migration primitives, based on those of the Distributed Join Calculus, with asynchronous pi. I'll go on to give a type system in which the input and output capabilities for channels may be either global or constrained to be local. This allows optimization, e.g. for communication on channels whose receivers are constrained to be at the same location as the channel. Subtyping allows communication to be accessed uniformly.
  
  
• Gerard Boudol. "The pi-calculus in direct style".
  Abstract:
  Our work is concerned with the foundations of higher-order concurrent programming. We focus on languages based on Milner's pi-calculus. Motivated by the observation that an indirect style of programming, where one explicitly manages "result channels", is enforced in such languages, we aim at designing a similar, but more flexible model for higher-order concurrency.
  We introduce a calculus which is a direct extension of both the lambda and the pi calculi. We give a simple type system for it, that encompasses both Curry's type inference for the lambda-calculus, and Milner's sorting for the pi-calculus as particular cases of typing. We observe that the various continuation passing style transformations for lambda-terms, written in our calculus, actually correspond to encodings already given by Milner and others for evaluation strategies of lambda-terms into the pi-calculus. Furthermore, the associated sortings correspond to well-known double negation translations on types. Finally we provide an adequate CPS transform from our calculus to the pi-calculus. This shows that the latter may be regarded as an ``assembly language'', while our calculus seems to provide a better programming notation for higher-order concurrency.
  
  
• Andrea Asperti. "P=NP, up to sharing".
  Abstract:
  We prove that we can compute the normal form of each term of the simple typed lambda-calculus (up to eta equivalence) in a polynomial number of sharable reductions (where the notion of sharing is Levy's "optimal" one). As a simple corollary, we get that P=NP, up to (the cost of) sharing.
  
  
• Paul-Andre Mellies. "A factorisation theorem for external derivations"
  Abstract:
  Among all the possible computations from a term, some are better than others. In my PhD, I give an algebraic characterisation of the << good >> ones, for instance the leftmost outermost reductions of the lambda-calculus: a derivation e: M -> P is << external >> if e.f: M -> Q is standard for any standard derivation f: P -> Q.
  In this short talk, I will show that every derivation d: M -> Q can be factorised as an external derivation e: M -> P followed by an << internal >> derivation f: P -> Q. Moreover, this epi-mono factorisation is functorial (i.e there is a nice diagram) in the sense of Freyd-Kelly.
  Conceptually, the factorisation result means that the good part in a computation can always be separated from the junk. Technically, it is the key step towards the description of stability (semantics) as a syntactic phenomenon. In fact, contrary to usual derivation spaces (see Levy's PhD), external derivation spaces enjoy meets.
  
  
• Philippa Gardner. "From Action Calculi to Linear Logic"
  Abstract:
  Action calculi, introduced by Milner, provide a framework for investigating models of interactive behaviour. In this talk, I'll give a type-theoretic interpretation of action calculi, using a general notion of natural deduction rule due to Aczel. I will also discuss two extensions: the higher-order extension which corresponds to a call-by-value lambda-calculus based on Moggi's commutative computational lambda-calculus, and the linear extension which corresponds to the linear type theories of Barber and Benton. The aim of this work is to isolate what is distinctive about action calculi, and to investigate the potential of action calculi as an underlying framework for many kinds of computational behaviour.
  This talk describes joint work with Andrew Barber, Masahito Hasegawa and Gordon Plotkin, and relies on recent work by John Power.
  
  
• Matthew Hennessy. "A Denotational Model for a subset of Core Facile"
  Abstract:
  To be announced.
  
  
• J.W.Klop. " Sequentiality in lambda calculus and PCF via origin tracking"
  Abstract:
  We give a new proof of a classical theorem in lambda calculus, namely Berry's Sequentiality Theorem. The proof is based on the syntactic technique of 'origin tracking', and employs infinitary lambda calculus. An extension of BST is given that yield more nondefinability results.
  
  
• Vincent Danos. "Distributed functional evaluation"
  Abstract:
  We describe a graphical implementation of Girard's execution formula that maps easily to a vectorial algorithm.
  
  
• Ole Hoegh Jensen."Graph rewriting and labelled transition semantics".
  Abstract:
  This talk presents a way of extending graph rewriting systems to labelled transition systems similar in spirit to those of process calculi such as CCS and pi-calculus. Graphs are equipped with a notion of interface through which composition with other graphs can take place. This enables a definition of labelled transitions where a label is, roughly, a piece of graph context that participates in forming a redex for a rewrite. The resulting strong bisimulation equivalence is a congruence with respect to all operations definable via the prescribed notion of interface.
  
  
• Roberto Amadio. "An asynchronous model of locality, failure, and process mobility"
  Abstract:
  We present a model of distributed computation which is based on a fragment of the pi-calculus relying on asynchronous communication. We enrich the model with the following features: the explicit distribution of processes to locations, the failure of locations and their detection, and the mobility of processes. Our contributions are two folds. At the specification level, we give a synthetic and flexible formalization of the features mentioned above. At the verification level, we provide original methods to reason about the bisimilarity of processes in the presence of failures.
  
  
• Laurent Regnier. "Geometry of interaction and coherent semantics"
  Abstract:
  We show how one can caracterize the coherent semantics of a proof-nets as a fix-point of the geometry of interaction. To do so one has to make the operators of the goi act on coherent spaces; this goes by building some intermediate spaces that are similar to games quotiented by the order of moves.
  
  
• Patrick Baillot. "AJM game semantic for classical linear logic (MELL0)"
  Abstract:
  We give an interpretation of MELL proof-nets in a category of games saturated strategies which models reduction without erasure. This model can be mapped ( intuitively by forgetting time ) onto a variant of coherent spaces.
  
  
• Davide Sangiorgi. "Interpreting Typed Object Calculi into Typed pi-calculus"
  Abstract:
  To be announced.
  
  
• Gianluigi Ferrari. "Locality based Linda: programming with explicit localities"
  Abstract:
  We investigate the issue of defining a programming calculus which supports programming with explicit localities. We introduce a language which embeds the asynchronous Linda communication paradigm extended with explicit localities in a process calculus. We consider multiple tuple spaces that are distributed over a collections of sites and use localities to distribute/retrieve tuples and processes over/from these sites. The operational semantics of the language turns out to be useful for discussing the language design, e.g. the effects of scoping disciplines over mobile agents which maintain their connections to the located tuple spaces while moving along sites. A type assignment system that permits statically checking access rights violations of mobile agents is also presented. Types are used to describe processes intentions (read, write, withdraw, execute, ...) relatively to the different localities with which they are willing to interact or at which they want to migrate. The type system is used to determine the operations that processes want to perform at each locality, to check whether they comply with the declared intentions and whether they have the necessary rights to perform the intended operations at the specific localities.
  
  
• Roberto Bruni. "Zero Safe Nets"
  Abstract:
  We propose a refinement model for Petri nets based on the notion of zero-safe place, i.e. a place containing 0 tokens in any reachable marking. Firings in a zero safe net consist of "atomic" firing sequence which respect the zero-safe requirement. This simple notion is the key to define an abstraction/refinement approach to concurrent system and it can be rephrased as an atomic synchronization mechanism among transitions. The algebraic structure of atomic firings is stressed out and the notion of "horizontal composition" among transition is proposed to represent atomic synchronizations. For each zero safe net, we characterize a corresponding "abstract net" whose correctness and adequacy are proved by means of a universal property. More precisely, we demonstrate the existence of a coreflection between the category of Petri nets with net morphisms and the category of zero-safe nets and abstraction morphisms. Finally we show how the semantics of zero safe nets can be understood in terms of monoidal double categories in a rather natural way.
  
  
• Uwe Nestmann. "Encoding Mixed-Guarded Choice"
  Abstract:
  To be announced.
  
  
• James Riely. "Distributed Processes and Location Failures"
  Abstract:
  Site failure is an essential aspect of distributed systems; nonetheless its effect on programming language semantics remains poorly understood. To model such systems, we define a process calculus in which processes are run at distributed locations. The language provides operators to kill locations, to test the status (dead or alive) of locations, and to spawn processes at remote locations. Using a variation of bisimulation, we provide alternative characterizations of strong and weak barbed congruence for this language, based on an operational semantics that uses configurations to record the status of locations. We then derive a second, symbolic characterization in which configurations are replaced by logical formulae. In the strong case the formulae come from a standard propositional logic, while in the weak case a temporal logic with past time modalities is required. The symbolic characterization establishes that, in principle, barbed congruence for such languages can be checked efficiently using existing techniques.
  
  
• Luc Maranget. "To be announced"
  Abstract:
  To be announced.
  
  
• Didier Remy. "Implicit typing a la ML for the join-calculus"
  Abstract:
  We adapt the Damas-Milner typing discipline to the join-calculus. The main result is a new generalization criterion that extends the polymorphism of ML to join-definitions. We prove the correctness of our typing rules with regards to a chemical semantics. We also relate typed extensions of the core join-calculus to functional languages.
  
  
• Joachim Parrow. "Pieces of pi: Substitution and Scoping"
  Abstract:
  We consider a more fundamental version of the pi-calculus with only one binding operator, called _scoping_. This is neither abstraction nor restriction; it neither implies a way to instantiate the scoped name nor forbids any such instantiation. It is symmetric in relation to the input-output polarity. The ordinary pi-calculus comes out as an asymmetric subcalculus. The price to be paid is a new kind of action: "substitution" actions
  P -{x/y}-> Q
  meaning P becomes Q upon the global substitution of all x for y, in Q, and in its environment.