headers
Benjamin Pierce | 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,

        Adriana Compagnoni  (abc@...)
        Benjamin Pierce     (bcp@...)
        Martin Steffen      (mnsteffe@...)

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

                 Subtyping in FomegaMeet is decidable

                        Adriana B. Compagnoni

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

Permalink | Reply | 0 comments |
headers
URSINI | 14 Jan 1994 09:08
Picon

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
        the advantage is admittedly rather thin, and is only visible
        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.

                      ***********************
(Continue reading)

Permalink | Reply | 0 comments |
headers
Mamede Lima Marques - POS_MAT | 15 Jan 1994 08:27
Picon
Favicon

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:

Please inform us! 

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
Permalink | Reply | 0 comments |
headers
Herman Geuvers | 11 Jan 1994 10:48
Picon
Picon

BRA project `Types for Proofs and Programs'


		INFORMAL PROCEEDINGS of the 

	BRA `TYPES FOR PROOFS AND PROGRAMS' WORKSHOP
Permalink | Reply | 0 comments |
headers
URSINI | 18 Jan 1994 10:17
Picon

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@...
Permalink | Reply | 0 comments |
headers
David Espinosa | 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
Permalink | Reply | 0 comments |
headers
David McAllester | 20 Jan 1994 19:31
Picon
Picon

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. }}
Permalink | Reply | 0 comments |

Gmane