Vaughan Pratt | 1 Jun 04:06 1993

Portable par

Out of the past 4000 retrievals of Latex files from Boole.Stanford.EDU
(abstracts in /pub/ABSTRACTS), I have had hardly any complaints about
incompatibilities with anyone's Latex environment.  (All /pub files on
Boole are archived in both .tex and .dvi form; current retrieval
preference is running 7:1 for Latex over DVI.)  Naturally this requires
sticking to stock standard Latex, which rules out custom fonts like
stmary, and custom .sty files are explicitly inserted in each file to
be exported.

My preferred source of inverted ampersands has therefore been the
75-line sprite definition (anonymous? from McGill?) rather than one of
the metafont versions.  However it has turned out that quite a few
sites do not have sprite.sty, generating several complaints, the only
ones I've gotten in recent memory.  I've been dealing with this by
including sprite.sty itself in the .tex file, the total then coming to
140 lines.

Needing an excuse this weekend not to work on whatever it was I was
supposed to be working on, I had a hack attack which yielded the
following 6-line Tex macro package implementing a \draw command
intended mainly for drawing character-sized objects.  This allows
inverted ampersand (and any other character that might take your fancy)
to be implemented in two lines, with a drawing (hence initialization)
time of around 0.3 seconds on a 10-Mips machine (the sprite version
takes 8 seconds to initialize), plus an additional line defining a
boxed version rendering in < .02 second (the sprite boxed version is
~0.1 second).  Furthermore the boxed version uses some tricky coding to
get the bare minimum of typesetting commands per character, permitting
up to 300 of the fast boxed characters per page, compared with
(Continue reading)

Anne S. Troelstra | 7 Jun 10:28 1993

natural deduction for linear logic; corrections;bibliography

The following is the abstract of a paper delivered on occassion of
Dirk van Dalen's 60th birthday, in april.


Natural deduction for intuitionistic linear logic 
by A.S. Troelstra

The paper deals with two versions of the fragment with unit, tensor,
linear implication and storage operator (the exponential !) of
intuitionistic linear logic. The first version, ILL, appears in a
paper by Benton, Bierman, Hyland and de Paiva; the second one, ILLP,
is described in this paper. ILL has a contraction rule and an
introduction rule !I for the exponential; in ILLP, instead of a
contraction rule, multiple occurrences of labels for assumptions are
permitted under certain conditions; moreover, there is a different
introduction rule for the exponential, !I+, which is closer in spirit
to the necessitation rule for the normalizable version of S4 discussed
by Prawitz in his monograph ``Natural Deduction''.

It is relatively easy to adapt Prawitz's treatment of natural
deduction for intuitionistic logic to ILLP; in particular one can
formulate a notion of strong validity (as in Prawitz's ``Ideas and
Results in Proof Theory'') permitting a proof of strong normalization.

The conversion rules for ILL explicitly mentioned in the paper by
Benton et. al. do not suffice for normal forms with subformula
property, but we can show that this can be remedied by addition of a
single conversion rule.
(Continue reading)

Laneve Cosimo | 1 Jun 15:59 1993

Interaction Systems 1

Several people has asked to us the first part of our work
on Interaction Systems:


			Interaction Systems I
                 The Theory of Optimal Reductions

          Andrea Asperti                   Cosimo Laneve

      Department of Mathematics,       INRIA - Sophia Antipolis,
      University of Bologna,           2004, Route des Lucioles,
      Piazza Porta S. Donato 5,        B.P.93 - 06902,
      40127 Bologna, Italy.            Sophia Antipolis, France.
      asperti@...	       cosimo <at>


A new class of higher order rewriting systems, called Interaction
Systems, is introduced. From one side, Interaction Systems provide the
intuitionistic generalization of Lafont's Interaction Nets (recall
that Interaction Nets are linear). In particular, we keep the idea of
binary interaction, and the syntactical bipartition of operators into
constructors and destructors. From the other side, Interaction Systems
are the subsystem of Klop's Combinatory Reduction Systems where the
Curry-Howard analogy still ``makes sense''. This means that we can
associate with every IS a suitable logical (intuitionistic) system:
constructors and destructors respectively correspond to right and left
introduction rules, interaction is cut, and computation is
(Continue reading)

Claudia Casadio | 11 Jun 09:55 1993


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

Dear colleagues,
We send the program of a workshop to be held
in Rome at the end of June.
Best regards,

Michele Abrusci
(University of Rome)
Claudia Casadio
(University of Chieti)

  Extensions and Linguistic Applications
  Dipartimento di Studi Filosofici ed Epistemologici
     Universita' di Roma - "la sapienza"
         June 28 - 30, 1993

The aim of this workshop is to address a set of relevant topics
concerning the interrelations between Linear Logic and Lambek Calculus
in the perspective of a formal theory of language developing the
principles of categorial grammar and lexical semantics. The workshop
is intended as an inter- disciplinary effort aimed at exchanging
scientific results and drawing attention to developments in the area
(Continue reading)

Thomas Streicher | 2 Jun 17:53 1993

Krivine's Machine with Control from a Continuation Semantics

Does anybody know whether the following derivation of Krivine's  
Machine with Control from a Continuation Semantics is known to the  

The new(?) continuation semantics given subsequently arises from
Girard's improved translation of classical logic to intuitionistic
logic when one restricts one's attention to the implicative fragment
and to formulae of negative polarity. It essentially uses the

  ~ A -> ~ B  =  ~ ( ~ A /\ B)

In a syntactic guise these ideas have originally been introduced by  
Y. Lafont.

Krivine's Machine with Control

The components of Krivine's machine are given by the following  
inductive definition

	t : Terms := x | lambda x. t | t t | C t
	e : Environments ::= Variables --> Closures  
                              (finite functions)
	c : Closures : = < t , e > | ret(k)
	k : Continuations ::= stop | < c, k >

Transition Rules

	< <x, e >, k >  -->  < e(c), k >    if  x  is in  dom(e)
(Continue reading)

John.Greiner | 2 Jun 18:55 1993

SML weak types paper available

The following paper on the soundness of SML "weak" types is now
available via anonymous ftp from

This is a reworking of an incorrect version previously announced on
the SML mailing list.  It has also been submitted to the Journal of
Functional Programming.


             Standard ML Weak Polymorphism Can Be Sound
                             John Greiner

Adding ML-style references to a Hindley-Milner polymorphic type system
is troublesome because such a system is unsound with naive polymorphic
generalization of reference types.  Tofte introduced a distinction
between imperative and applicative type variables, such that
applicative type variables are never in reference types, that provides
a simple static analysis of which type variables may be
polymorphically generalized.  MacQueen's weak type variables
generalize imperative type variables with a counter called a strength.
The finer distinction allows a more accurate analysis of when a
reference may be created, and thus which type variables may be

Unfortunately, weak polymorphism has been presented only as part of
the implementation of the SML/NJ compiler, not as a formal type
(Continue reading)

Andrzej Borzyszkowski | 4 Jun 15:45 1993

MFCS'93 information booklet, plain text.

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

The following contains the MFCS'93 information booklet

   l.  19   General information
   l. 553   Registration form
   l. 610   The abstracts of the talks

                        Call for Participation
                      and Preliminary Programme
                     18th International Symposium
             Mathematical Foundations of Computer Science
                           Gdansk, Poland
                    30 August -- 3 September, 1993


The MFCS symposia have been organized in Poland and Czecho-Slovakia
since 1972. Their purpose is to encourage high-quality research in
all branches of Theoretical Computer Science, in particular
   concurrency, lambda calculus, semantics and logics of programs,
   specification, complexity, algorithms, automata theory.
(Continue reading)

Dr G Bellin tel 2-76933 | 9 Jun 02:37 1993

Preliminary Announcement

                      SLICING THE ADDITIVE BOXES 

                       Preliminary Announcement

                   Gianluigi Bellin and Janice Hudgings

                          (Oxford University)

Abstract: In Multiplicative and additive linear logic (without
constant) the problem of deciding whether an arbitrary family of
slices is the slicing of a sequent derivation, is polynomial in the
size of the the data.

Comments: Slices for MALL- (MALL without weakening for \bottom) are
defined like multiplicative proof-structures, but with `plus' links
and *one-premise* `with' links.

                                Part (i) 

Given a sequent derivation D in MALL- (or the corresponding proof-net
with additive boxes) we can associate a set Sl(D) of additive slices;
such a representation of MALL- proofs satisfies the Church-Rosser
property. E.g.,

           |- A,-A  |- A,-A     |- A,-A  |- A,-A  
         & ----------------   & ----------------  
               |- A&A, -A          |- A, -A&-A     
           cut -------------------------------
(Continue reading)

Joe Wells | 16 Jun 03:04 1993

result announcement: 2nd-order Lambda Calculus Typability Undecidable

This message is the announcement of a result and a forthcoming paper.

                       TYPABILITY AND TYPE-CHECKING


                               J. B. Wells
                          Computer Science Dept
                            Boston University

      We consider the problems of typability[1] and type checking[2] in
      the Girard/Reynolds second-order polymorphic lambda calculus, which
      we will call System F, which we use in the "Curry style" where types
      are assigned to pure lambda terms.  These problems have been
      considered and proven to be decidable or undecidable for various
      restrictions and extensions of System F and other related systems,
      and lower-bound complexity results for System F have been achieved,
      but they have remained "embarrassing open problems"[3] for System F

      The typability problem is to decide, given an (untyped) lambda term
      M, whether there exists a type t and a type assignment[4] A such
      that there exists a valid derivation in system F for the
      assertion[5] A |- M : t.  The closely related type-checking problem
      is to decide, given a lambda term M, a type t, and a type assignment
      A, whether there is a valid derivation in system F for the assertion
      A |- M : t.
(Continue reading)

odersky | 23 Jun 22:55 1993

CFP: Special Issue of LASC

                          Call for papers

        Lisp and Symbolic Computation Special Issue on 

                   "State in Programming Languages"

Papers are solicited for a special issue of the Journal of Lisp and
Symbolic Computation (LASC) on state in programming languages.

Programming languages have been state-based since their inception.
After a period of relative unpopularity, when research focused on
declarative languages, interest in the treatment of state has been
renewed.  This is not a backlash against declarative programming.
Rather, it is an attempt to find a symbiotic relationship between the
semantic foundations of declarative languages and the pragmatic
handling of state in more conventional languages.  This special issue
is a followup to SIPL '93, the first ACM SIGPLAN Workshop on State in
Programming Languages held in late spring in Copenhagen, Denmark.

It will be edited by Ian A. Mason (Stanford University) and Martin
Odersky (Yale University).  The range of topics includes operational
and denotational models of state, assignment and references, semantics
of object-oriented programming, linear type systems, effect systems,
monads, calculi of state and methods to reason about state.

Submissions are due Dec 21 1993.  Authors should submit a full paper
plus a 1-2 page extended abstract summarizing the main contributions.
Submissions are expected to be of journal quality, and will undergo
the normal review process of LASC.
(Continue reading)