7 Jan 1994 21:14

### Two papers on higher-order polymorphism and subtyping


Two new papers combining higher-order polymorphism and subtyping are
now available for anonymous FTP.  Beginning from a common foundation,
both use proof-theoretic techniques to obtain related -- but
independently derived -- decidability results, one [Steffen and
Pierce] for the pure system FomegaSub of higher-order bounded
quantification, the other [Compagnoni] for FomegaSub enriched with
intersection types, FomegaMeet.  Abstracts and FTP instructions
follow.

Enjoy,

Benjamin Pierce     (bcp@...)
Martin Steffen      (mnsteffe@...)

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

Subtyping in FomegaMeet is decidable

Combining intersection types with higher-order subtyping yields a
typed model of object-oriented programming with multiple inheritance
[CompagnoniPierce93].  The target calculus, FomegaMeet, a natural
generalization of Girard's system Fomega with intersection types and
bounded polymorphism, is of independent interest.  We prove that
subtyping in FomegaMeet is decidable, which yields as a corollary the
decidability of subtyping in FomegaSub, its intersection free
fragment, because FomegaMeet subtyping system is a conservative


14 Jan 1994 09:08

### ABSTRACT


NEW LINEAR LOGIC PROOF THEORY AND SEMANTIC, II .
by
Aldo Ursini

Dipartimento di Matematica
via del Capitano 15
53100 SIENA
Italy
tel.(577)286244
fax.(577)270581
e-mail: ursini@...,it

-extended abstract-
Abstract of the abstract.

We give a different presentation of phase semantic for linear
logics.First of all this allowed us to understand the PAR
connective.Secondly it runs very smoothly in all existing
directions: commutative, non commutative, classic, intuitionistic.
So, as the II-nd paper of the series, this is devoted to
"truth semantic" of linear logics.Since we are in no way
pupils able to overcome their master, in the classical commutative case
when exponetials come to the limelight.In all other cases there
seems to be some real surplus over existing semantics.In a
different paper the method will be tested for LC and LU.

***********************



15 Jan 1994 08:27

### A flaw in the proof of Fermat's theorem

[This message is not strictly relevant to the Types Forum.  But I am
circulating it anyway, as a matter of general interest.  Replies by
e-mail to Mamede please.  Mamede, could you please post a summary or
pointer to your final article, for those of us that are interested?
-- Philip Wadler, moderator, Types Forum]

Please, whoever  knows  anything  about A FLAW  IN THE RECENT PROOF OF
FERMAT'S LAST THEOREM:

We need to write a report on the situation to a Brazilian magazine and
we are looking for fresh news.

Thanks a lot,

Mamede Lima-Marques
Center for Logic and Epistemology
UNICAMP
Campinas  -  Brazil


11 Jan 1994 10:48

### BRA project Types for Proofs and Programs'


INFORMAL PROCEEDINGS of the

BRA TYPES FOR PROOFS AND PROGRAMS' WORKSHOP


18 Jan 1994 10:17

### CORRECTION


DEAR LINEAR COSTUMER
PLEASE NOTICE THAT IN THE ABSTRACT :
New Linear Logic Proof Theory and Semantic, II
WICH IS TODAY IN YOUR E-MAIL THERE IS AN ERROR IN THE ITEM (*)
SECTION 2, RELATING PHASE SPACES AND PHASOIDS.

THE  CORRECT  FORMULA  IS :
(*)  x R y     iff  xy does not belong to BOTTOM.

Omnia munda mundis
Aldo Ursini

Aldo Ursini
Universita' di Siena
Dipartimento di Matematica
Via del Capitano 15
53100 Siena - Italy
ph: 577-286244
fax: 577-270581
email: ursini@...


20 Jan 1994 23:24

### categorical treatment of F_omega?


1. Could someone send me a good reference for a categorical treatment
of the Girard / Reynolds F_2 polymorphic type system?  That is,
polymorphic functions as (some form of) natural transformations?

2. More importantly, has there been a categorical treatment of
Girard's F_omega type system?

David


20 Jan 1994 19:31

### paper announcement


There is a (somewhat) new paper available by anonymous ftp in the
file ftp.ai.mit.edu:/pub/dam/strong.ps

Here is a title and abstract

A Proof of Strong Normalization for $F_2$, $F_\omega$, and Beyond.

by D. McAllester, J, Kucan, and D. Otth
(dam@..., kucan <at> theory.lcs.mit.edu, Otth <at> theory.lcs.mit.edu)

{\abstract{ We present a new kind of proof of strong normalization for
$F_2$. The proof establishes invariants of the inference rules by
defining an appropriate semantics for the type assertions and showing
that the inference rules are sound relative to this semantics.  Strong
normalization is then a simple corollary of soundness. The proof
easily generalizes to more complex typing systems like $F_\omega$. We
also explore extensions of $F_\omega$ for which the proof holds. We
argue that the new proof technique is more natural and can be more
easily used as a general method for proving properties of reduction in
a variety of typing systems. }}



Gmane