11 Dec 1990 16:50

### A little linear logic observation about Petri Nets

Date: Tue, 11 Dec 90 13:57:43 GMT

A little linear logic observation about Petri Nets

Carolyn Brown (from Edinburgh) was here (Imperial College, London) last week
talking about her categories of Petri nets based on Valeria de Paiva's
"dialectica categories" (Carolyn presented her work at LiCS this year).
Afterwards, Carolyn and I tried but failed to make sense of an idea of mine
that Petri nets were "internal categories" in some context in which Valeria's
construction provided the "sets".  However we did come up with a cute little
formula for sequences of actions which has a linear logic interpretation.
For those who are confused by the many different understandings of linear
logic in Petri Nets, let me just point out that what follows depends only on
the "trivial" observation that markings are additive, whereas Valeria &
Carolyn's work involves amuch more suble tensor.

I have in mind Petri nets which
*	at first require at most one token from each place for an event,
*	in the second case require an arbitrary natural number of them,
*	and in the general case the input (and similarly the output) is an
element of a complete ordered monoid, or even a monoidal category.
First I'll phrase my argument in the "natural numbers" case.  I want to
find the pre- and postconditions of the sequence $e;f$ in terms of those
of the events $e$ and $f$.

For each place $b\in B$, clearly we need at least $pre(e,b)$, else we
couldn't perform $e$. Then we need no more if $post(e,b)\geq pre(f,b)$,
but otherwise $pre(f,b)-post(e,b)$ in addition. Likewise the output is
at least $post(f,b)$, but there may be a left-over $post(e,b)-pre(f,b)$
in addition if this is nonnegative.


21 Dec 1990 22:47

### Summerschool on Lambda Calculus, Jul 8-12, 91

Date: Fri, 21 Dec 90 18:39:19 +0100

FIRST ANNOUNCEMENT

The Research Institute for Declarative Systems, Nijmegen University,
organises a

S U M M E R S C H O O L

on

L A M B D A   C A L C U L U S

Dates:  July 8-12, 1991
Place:  Nijmegen University, The Netherlands

One week before the Logic in Computer Science meeting (Amsterdam, July 15-17,
1991) there will be a summerschool on lambda calculus (typed and untyped)
held in Nijmegen.

There will be three courses.

1.  Introduction to lambda calculus.
Syntax of terms, conversion, fixed points, reduction,
Church-Rosser theorem, representation of recursive functions,
Boehm trees, simple lambda models, types.

2.  Advanced lambda calculus.
The theory of constructions and its fine structure,
logics as type systems, proofs of strong normalisation,