4 May 15:40 1993

### paper available via ftp


The following paper is available via ftp from Imperial College.
The procedure follows the title and abstract

A Semantics for Evaluation Logic
Eugenio Moggi
DISI, Univ. of Genova
viale Benedetto XV 3, 16132 Genova, ITALY
moggi@...

Abstract

This paper proposes a topos-theoretic semantic for the
modalities and evaluation predicate of Pitts' Evaluation Logic, and
introduces several predicate calculi (ranging from Horn sequents to
Higher Order Logic), which are sound and complete w.r.t. natural classes
of models.  It is shown (by examples) that many computational monads
satisfy the additional properties required by the proposed semantics.

------------------

ftp theory.doc.ic.ac.uk
cd /theory/papers/Moggi
binary
get ELT.dvi.Z
-or-
get ELT.ps.Z



4 May 20:10 1993

### (unknown)

[Since it is clearly relevant, I am distributing this conference
announcement to types.  General conference announcements should go to
the Theory-A list.  -- Philip Wadler, moderator, Types Forum.]

ACM SIGPLAN Workshop on State in Programming Languages
June 12, 1993
Copenhagen, Denmark
(in conjunction with FPCA and PEPM)

-----------------------------------------------------

Since the conference building will not open until 8.30 on Saturday,
registration for SIPL will start at 8.30 instead of 8.00, as was
previously announced. Of course, participants can also register when
they register for FPCA.

8.30 - 9.30 Registration

8.30 - 9.30: Tutorial -- Matthias Felleisen (Rice University)
and Paul Hudak (Yale University):
Expressing and Reasoning about State''

9.30 - 10.45 -- Reasoning about Imperative Programs
Chairman: Ian Mason

Jonathan Eifrig, Scott Smith, Valery Trifonov, Amy Zwarico (Johns


5 May 11:33 1993

### FPCA/SIPL/PEPM advance program and registration information (update)

[Since it is clearly relevant, I am distributing this conference
announcement to types.  General conference announcements should go to
the Theory-A list.  -- Philip Wadler, moderator, Types Forum.]

----------  Updated advance program and registration information  ------------

***********************************************
FPCA/SIPL/PEPM:
COPENHAGEN PROGRAMMING LANGUAGE CONFERENCE WEEK
***********************************************
June 9-16, 1993, Copenhagen, Denmark

FPCA '93: Conference on Functional Programming Languages and Computer
Architecture (*), June 9-11, 1993

SIPL '93: Workshop on State in Programming Languages (**), June 12, 1993

PEPM '93: Symposium on Partial Evaluation and Semantics Based
Program Manipulation (**), June 14-16, 1993

------------------------------------------------------------------------------
IMPORTANT NOTES:

guaranteed hotel room reservations for FPCA, SIPL and PEPM is
May 7th -- register now! (Registration forms are included at the end.)

(2) 	Note that PEPM has been moved from Gothenburg to Copenhagen
in spite of what the CACM calendar of events may say!



11 May 00:36 1993

### paper on FTP


A paper on categorical theory of proofs

MAPS II:
CHASING PROOFS IN THE LAMBEK-LAWVERE LOGIC
by Dusko Pavlovic

is available by anonymous FTP from triples.math.mcgill.ca . It is in
the directory pub/pavlovic , in the files called mapsII : there are
-A4 and -US formats; .dvi and .ps versions of both. All are
compressed.

-- Regards, Dusko

Abstract

In the Lambek-Lawvere logic, propositions and proofs are presented as
objects and arrows in a category. It is the categorical embodiment of
the strong constructivist paradigms of propositions-as-types and
proofs-as-constructions, which lie in the foundation of computational
logic. But a third paradigm arises here, not available elsewhere: the
idea of logical-operations-as-adjunctions. It opens a possibility of
genuinely categorical proof theory.

In the present paper, we study the Lambek-Lawvere version of regular
logic: the $\{\wedge,\exists\}$-fragment of the first order logic with
equality. The corresponding categorical structure is regular
fibration. The examples include stable factorisations, sites,
triposes. Regular logic is exactly what is needed to talk about maps,
as total and single-valued relations. However, when enriched with


10 May 17:03 1993

### Announcement of Summer School


Tempus Summer School for Algebraic and Categorical Methods

in Computer Science

Second Announcement

Brno, June 28 - July 3, 1993

Sponsored  by the European Community TEMPUS office the organizers

are pleased to announce an intensive course designed to serve its

students as a forum for exchange of ideas between the disciplines

of mathematics and computer science.

Courses:

P. J. Freyd (Philadelphia), Cartesian Logic and Cartesian

Categories

Y. Lafont (Paris), Linear Logic

J. Lambek (Montreal), Categories and Deductive Systems

C. P. Stirling (Edinburgh), Modal and Temporal Logics for
Processes



13 May 11:39 1993

### Questions on LU and ITT


(This message was earlier posted to the logic mailing
list, but no responses were received.)

logic and LU.

1.  Has a sequent presentation of Martin-Lo"f Intuitionistic Type Theory been
published?

2.  The next pair of questions are about the Intuitionistic fragments of LU
and their relation to the traditional sequent calculi for Intuitionistic
logic.

From my undersanding of Girard's paper on LU, the translation of the
intuitionistic fragments of LU into the traditional sequent calculi for
intuitionistic logic are straightforward, but the other way things may
be more delicate.  Has someone proven a result showing that cut-free
(resp. not necessarily cut free) intuitionistic proofs translate into
cut-free (resp. not necessarily cut free) proofs within the intuitionistic
fragment of LU (i.e. with sequents maintaining the specified restrictions
at each stage in the proof).

I would appreciate any information on the connections between LU's
intuitionistic fragment and usual calculi for intuitionistic logic.

Thanks,
Sanjiva					(sanjiva@...)

Sanjiva Prasad,  Guest Magus				E-mail: sanjiva@...


16 May 14:19 1993

### IL -- LU -- LL


In his message to the Linear mbox of Thu, 13 May 93, Sanjiva Prasad writes:

linear logic and LU.
[ ............. ]
I would appreciate any information on the connections between LU's
intuitionistic fragment and usual calculi for intuitionistic logic"

The paper "On the linear decoration of intuitionistic derivations" (joint
work of V.Danos, J.B. Joinet and myself) might be of help in gaining some
insight. It is available by anonymous ftp from "gentzen.logique.jussieu.fr".
You will find it in the directory pub/scratch as Noble1.dvi'. There's
also a compressed file, Noble1.dvi.Z'.
In the paper we mention e.g. how one can transform a given derivation in
the (implicational fragment of) usual sequent calculus for intuitionistic
logic into a derivation in the (neutral) intuitionistic fragment of LU.

A general hint: if you have some experience with linear logic, think of the
intuitionistic/classical LU-fragments via their linear interpretation':
write !p for positive atoms p, ?n for negative atoms n, x for neutral atoms x,
and use the linear definitions of the connectives (you then will find that
"formula F is positive" corresponds to "its linear interpretation [F] has
the property that [F] <=> ![F] is provable in linear logic", and, dually, for
"formula F is negative" we have "[F] <=> ?[F] is provable in LL").

Harold Schellinx

(NB.: You might also be interested in a second paper, related to the one
mentioned above. It is called "The Structure of Exponentials: Uncovering


13 May 18:53 1993

### Re: Questions on LU and ITT


> logic and LU.
>
> 1.  Has a sequent presentation of Martin-Lo"f Intuitionistic Type Theory been
>     published?

My 1990 University of Edinburgh Ph.D. thesis contains, amongst other
things, a sequent calculus for the lambdaPi-calculus, a theory of
first-order dependent function types (just Pi, no Sigma, a fragment of ITT).

This is discussed, as part of a different analysis, in

Proof-search in the $\lambda\Pi$-calculus'', by D.J. Pym and L.A. Wallen.
In: Logical Frameworks, Gerard Huet and Gordon Plotkin (editors),
Cambridge University Press, 1991.

I have just submitted a paper, A Note on the Proof Theory of the
$\lambda\Pi$-calculus'' to a journal. This paper discusses the
sequent calculus for lambdaPi and some resolution calculi that
arise from it.

I am preparing papers on these sorts of issues for Sigma types and
also for PTSs.

>
> (This message was earlier posted to the logic mailing
>  list, but no responses were received.)
>



13 May 15:13 1993

### New book on TERM GRAPH REWRITING


TERM GRAPH REWRITING: theory and practice
-----------------------------------------
eds M.R.Sleep, M.J.Plasmeijer and M.C.J.D. van Eekelen

John Wiley, April 1993. Price approx. 47.95 USD, 29.95 LUK.

TERM GRAPH REWRITING refers to techniques and theories for
representing terms and term rewrite rules as graphs and graph rewrite
rules. Many modern programming paradigms - most notably the functional
and logic paradigms - have term rewriting at their heart, although the
control regimes and semantics are very different. Practical
implementations of these languages share subterms using pointers, and
the machine code for such programs manipulates shared structures
(called in this volume {\em term graphs}).

The operational semantics of the resulting programs may be represented
as a set of term graph rewriting rules. Reasoning about the
correctness and efficiency of such representations relies on our
ability to reason about term graph rewriting systems, and to relate
them to other semantic models.  Used in this way, term graph rewriting
offers a model of computation which is closer to real implementations
than pure term rewriting, but which avoids unnecessary machine detail.

Graph rewriting was the focus of a number of European ESPRIT Basic
Research Actions most notably SEMAGRAPH and COMPUGRAPH. Both projects
led to theoretical and practical advances for term graph rewriting
reflecting the state of the art, and these form the contents of this
book.



13 May 19:55 1993

### Postdoctoral Fellowship


School of Cognitive and Computing Sciences
University of Sussex

Visiting Postdoctoral Fellowship in Theoretical
Computer Science

The School of Cognitive and Computing Sciences contains a strong and
very active research group in Theoretical Computer Science.  Major
areas of research include The Foundations of Distributed Computing,
The Application of Logic to Computer Science, The Semantics of
Programming and Specification Languages, Software Tools for
Verification, Type Systems.

Applications are invited for a one year Visiting Fellowship from
October 1993. Candidates should have recently completed their doctoral
studies and have research interests compatible with those of the
school.  The successful candidate will be expected to carry out a
small amount of tutorial teaching.

Faculty members in Theoretical Computer Science currently include:

Dr Luca Aceto (theories of concurrency)
Dr Carolyn Brown (linear logic, category theory, theories of concurrency)
Prof Matthew Hennessy (theories of concurrency, specification
languages)
Dr Alan Jeffrey (theories of concurrency, functional languages, type
theories)
Dr Xinxin Liu (specification languages, logics)
Dr Sophie Pinchinat (behavioural equivalences, logics for concurrency)
`