headers
Don Sannella | 1 Nov 1990 17:25
Picon

MFCS'91

Date: Wed, 31 Oct 90 20:18:03 GMT

--> --> --> --> --> -->       CALL FOR PAPERS       <-- <-- <-- <-- <-- <--
				       
			16th International Symposium on
		 MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE
				       
				 M F C S ' 9 1
				       
				    Poland
			     9 - 13 September 1991

The symposium will be organized jointly by the Institute of Computer Science
of the Polish Academy of Sciences, the Institute of Informatics of Warsaw
University and the Polish Information Processing Society.

The MFCS symposia have been organized in Poland and Czechoslovakia since 1972
and by now have a long and well-established tradition.  The purpose of the
symposia is to encourage high-quality research in all branches of Theoretical
Computer Science and to provide an opportunity of bringing together specialists
working actively in the area.  Throughout the years MFCS served this purpose
well, and we hope it will do so in the future.

Principal areas of interest of the symposium include:
	software specification and development, parallel and distributed
	computing, semantics and logics of programs, algorithms, complexity and
	computability theory (this is not an exclusive list).

The scientific programme of the symposium will include invited lectures by
J.-L.Lassez (Yorktown Heights), P.Lescanne (Nancy), G.Mints (Tallin),
(Continue reading)

Permalink | Reply | 0 comments |
headers
Samson Abramsky | 7 Nov 1990 00:52
Picon

Computational interpretations of Linear Logic

Date: Tue, 30 Oct 90 18:17:58 GMT

Albert,

I've just completed a paper on this topic. Please put the abstract on any
of the lists (types, concurrency etc.) for which you think it would be
appropriate.

Best wishes,

Samson

=====================================
Computational Interpretations of Linear Logic

Samson Abramsky

Imperial College

We study Girard's Linear Logic from the point of view of giving a concrete
computational interpretation of the logic, based on the Curry-Howard
isomorphism. In the case of Intuitionistic Linear Logic, this leads to
a refinement of the lambda calculus, giving finer control over order
of evaluation and storage allocation, while maintaining the logical content
of programs as proofs, and computation as cut-elimination. In the classical
case, it leads to a concurrent process paradigm with an operational
semantics in the style of Berry and Boudol's Chemical Abstract machine.
This opens up a promising new approach to the parallel implementation of
functional programming languages; and offers the prospect
of typed concurrent programming in which correctness is guaranteed by the
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jonathan P. Seldin | 17 Nov 1990 00:22
Picon
Picon

LaTeX version of article

Date:     Thu, 15 Nov 90 12:14:24 EST

EXCLUDED MIDDLE WITHOUT DEFINITE DESCRIPTIONS IN THE THEORY OF
CONSTRUCTIONS

A LaTeX version of this article, which I circulated on TYPES two
months ago, in now available by anonymous ftp from
clyde.concordia.ca (132.205.1.1); the file is /pub/seldin.dvi.
For those who do not have access to anonymous ftp, I am prepared
to send a uuencoded (or, if you prefer, by tarmail) version of
the file in response to requests by e-mail.

The paper is a response to a posting by Garrel Pottinger a year
ago which shows that excluded middle together with definite
descriptions in the calculus of constructions implies proof
degeneracy:  that any two terms in a small type (a type in Prop)
are equal in the sense of Leibniz equality.  In this paper it is
shown proof-theoretically that excluded middle alone does not
imply proof degeneracy.  This is done by proving consistent a set
of assumptions sufficient for classical arithmetic; since one of
the Peano axioms asserts that zero is not a successor, and since
the numerals involved are all in a small type, this consistency
is incompatible with proof degeneracy.

Jonathan P. Seldin
Internet:				seldin@...
Bitnet:						       seldin <at> conu1
Permalink | Reply | 0 comments |
headers
R.A.G. Seely | 27 Nov 1990 00:18
Picon

Notice of meeting

Return-Path: < <at> mitvma.mit.edu:MT79@...>
Date:        Thu, 22 Nov 90 10:03:14 EST

NOTICE OF MEETING

Date:  June 23--30, 1991

Title: INTERNATIONAL CATEGORY THEORY MEETING

Place: Montreal, Quebec, Canada

Speakers: (The following have accepted)
  S. Abramsky, A. Carboni, J. Isbell, J. Jardine,
  F. Lamarche, G. Meloni, E. Moggi, J. Pelletier,
  A. Pitts, R. Street, V. Trnkova, R. Wood.

Deadline for abstracts: March 15, 1991

Further information: Category Theory 1991
                     Math. Dept., McGill University
                     805 Sherbrooke St. W
                     Montreal, Quebec
                     Canada H3A 2K6

                     Email: mt16@...
Permalink | Reply | 0 comments |

Gmane