Eugenio Moggi | 4 May 15:40 1993
Picon

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
        login: anonymous
        password: <your email address>
        cd /theory/papers/Moggi
        binary
        get ELT.dvi.Z
        -or-
        get ELT.ps.Z

(Continue reading)

odersky | 4 May 20:10 1993
Picon

(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.]
				   

		      Advance Program -- SIPL93
				 	  
	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
(Continue reading)

henglein | 5 May 11:33 1993
Picon

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:	

(1)	Deadline for discounted advance conference registration and 
	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!

(Continue reading)

Dusko Pavlovic | 11 May 00:36 1993
Picon

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
(Continue reading)

TEMPUS | 10 May 17:03 1993
Picon

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

(Continue reading)

Sanjiva Prasad | 13 May 11:39 1993
Picon

Questions on LU and ITT


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

I seem to have evermore questions as I learn more about proof theory, linear
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@...
(Continue reading)

hars | 16 May 14:19 1993
Picon

IL -- LU -- LL


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

  "I seem to have evermore questions as I learn more about proof theory,
   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
(Continue reading)

David J Pym | 13 May 18:53 1993
Picon

Re: Questions on LU and ITT


> I seem to have evermore questions as I learn more about proof theory, linear
> 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.)
>

(Continue reading)

Ronan Sleep | 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.

(Continue reading)

Matthew Hennessy | 13 May 19:55 1993
Picon

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)
(Continue reading)


Gmane