Christian Retore | 6 Oct 11:17 1993

non-commutative tensor

During the summer there was a discussion on calculi 
involving both commutative and non-commutative connectives.
I mentionned the work I did on this topic, 
but there was nothing available by ftp.

I partly fixed this trouble by putting the 
english introduction of my thesis 
called:                    intro.dvi 
on the ftp site: 
under the directory:       pub/papers/retore

The paper on this ordered calculus will soon be available
on the same ftp directory, with the name pomset.dvi 

Lawrence C Paulson | 5 Oct 15:05 1993

paper available

The following report is available by anonymous ftp from the University
of Cambridge.
						Larry Paulson

    Set Theory for Verification: II. Induction and Recursion

A theory of recursive definitions has been mechanized in Isabelle's
Zermelo-Fraenkel (ZF) set theory.  The objective is to support the
formalization of particular recursive definitions for use in
verification, semantics proofs and other computational reasoning.

Inductively defined sets are expressed as least fixedpoints,
applying the Knaster-Tarski Theorem over a suitable set.  Recursive
functions are defined by well-founded recursion and its derivatives,
such as transfinite recursion.  Recursive data structures are
expressed by applying the Knaster-Tarski Theorem to a set that
is closed under Cartesian product and disjoint sum.

Worked examples include the transitive closure of a relation, lists,
variable-branching trees and mutually recursive trees and forests.
The Schr\"oder-Bernstein Theorem and the soundness of
propositional logic are proved in Isabelle sessions.

FTP Instructions:

* Connect to host []
* Use login id "ftp" with your internet address as password
* put ftp in BINARY MODE ("binary") 
* go to directory reports (by typing "cd reports")
(Continue reading)

Radu Grosu | 12 Oct 19:45 1993

subtyping variants

What is the current state of art in (sub)typing variants?
For example consider the following data type declaration:

data I1 = Xcoord | Ycoord | Mv(Real,Real)

I would like to write something like

data I2 = Color | I1

instead of

data I3 = Color | Coerce(I1)

If one considers only non-recursive (polymorphic) data type 
declarations then:

1) Are type reconstruction algorithms awailable to compute 
   the principal type of functions defined by using the 
   constructors of I2?

2) Is there any functional of the form:

   I2-w :: x -> (I1 -> x) -> I2 -> x

   I2-w (a)(f)(x) = case x of
      Color     => a
      otherwise => f x

   corresponding to the functional obtained for I3:
(Continue reading)

Thomas Streicher | 13 Oct 14:07 1993

proof terms for classical logic in natural deduction formulation


In this note we will define a proof term calculus for First Order
Classical Logic (CL) in a Natural Deduction Formulation (as can be
found in several recent papers of Michel Parigot). But instead of
using Parigot's mu-calculus we stick to a more traditional language
for proof terms, namely a fragment of Martin-Loef's Type Theory.
Actually it is a rather poor fragment. Besides \-calculus we simply
use the pairing function <_,_> (which is a constructor) and
Martin-Loef's eliminator pattern-matching. It is just the operator
defined by the semantics :

          p => <a,b>  e[a,b/x,y] => c
           E(p , (x,y) e) => c

In a more traditional (SML-style notation one could write 

     let  <x,y> = p  in  e    instead of  E(p , (x,y) e)  .

Our proof term assignment is inspired by the negative polarity  
fragment of Girard's LC. This gives rise to the following improved   
~~-translation :

   G(A) := ~ A*

where  (_)*  is defined inductively as follows :

(Continue reading)

Dusko Pavlovic | 13 Oct 17:47 1993

Chu is cofree

A paper on 

	by Dusko Pavlovic

is available by anonymous FTP from The files
chu-{A4,US}.{dvi,ps}.Z are the directory pub/pavlovic. Each of them
contains the whole paper, but in various formats.


We describe a couniversal property of the Chu construction. It induces
a comonad on a category of autonomous categories. *-Autonomous
categories are exactly the coalgebras for this comonad.  The models of
full classical linear logic (with the exponentials) are then obtained
as the coalgebras on the models of intuitionistic linear logic ---
this time for a comonad derived from the Chu construction.  In view of
the computational interpretations of linear logic, these results
suggest an interesting connection of the functional and the concurrent
programming. For this reason, some effort has been spent to make all
the constructions effective.

Serge Vorobyov | 11 Oct 19:32 1993

erratum: Undecidabilty of System F

I am grateful to Henk Barendregt, Martin Hoffmann, and Pawel Urzyczyn
who have pointed out the problem with unjustified "extraction term
from termination proof" trick, which I used to construct the term
$f_p$ in the very end of my proof of undecidability of F published in
the "types" mailing list this summer. Therefore I withdraw my claim
till I find satisfactory reparation or another proof. I am awfully
sorry for creating confusion. I would like to thank Jean-Jacques Levy
and Roberto Amadio for useful discussions.

Sergei Vorobyov


Postscript: here are some explanations

> Henk Barendregt writes:
> You have a term f^ p Q x representing f_p x where Q is a proof of
> Inf(X_p). If X_p is infinite (provably so), then this gives a term
> for f_p. If X_p is not infinite we have nothing, it seems.

> Martin Hoffmann writes:
> The thing I don't understand is how you obtain a lambda term f_p in
> case p does not have a solution. The only thing which comes to mind
> would be to take the lambda term corresponding to \x . mu y>x .
> "enum(y) solves p" where we use some coding of the mu operator. Of
> course this term is not F typable in case p has no solution, but I
> don't see why it should have an F type in case there is such a
(Continue reading)

Petry | 19 Oct 17:23 1993


        Days of Mathematical Logic at W\'egimont Castle,
                december 6th,7th, and 8th  1993.

A three days meeting in Mathematical Logic are set up on december 6th,
7th and 8th december 1993 at W\'egimont Castle . This castle is situated
about fifteen kilometers near from Li\`ege (Belgium).

The programme consists in four basic courses (about 3 hours for each
- F. Honsell (Udine) : Theory and applications of non-well-founded sets.
- R. Kaye (Oxford) : Quantifier complexity and applications to
                     arithmetic and set theory,
- A. Macintyre (Oxford) : Reals with exponentiation and their
                          applications (probable title),
- D. van Dalen (Utrecht) : Intuitionism and constructive mathematics.

A few contributed papers are planned, at the moment :

- O. Chapuis (Paris): D\'ecidabilit\'e et ind\'ecidabilit\'e des
                      th\'eories universelles des groupes r\'esolubles
- F. Koerner (Berlin) : Cofinal indiscernibles and applications to NF.

This meeting is organized by M. Boffa (U.M.H.) and A. P\'etry (I.S.I.L.)
thanks to the support of the Centre National de Recherches de Logique.

It will be possible to have meals and stay in W\'egimont castle.
However the number of rooms is limited.

(Continue reading)

ohearn | 25 Oct 20:19 1993

Parametricity and Local Variables

The following paper is available by anonymous ftp from
in ohearn/plv.dvi

Parametricity and Local Variables
P. W. O'Hearn and R. D. Tennent

We propose that the phenomenon of local state may be understood 
in terms of Strachey's concept of parametric (i.e., uniform) 
polymorphism.  The intuitive basis for our proposal is the following 
analogy: a non-local procedure is independent of locally-declared
variables in the same way that  a parametrically polymorphic function 
is independent of types to which it is instantiated.

A connection between parametricity and representational abstraction
was first suggested by J.\,C.~Reynolds.  Reynolds used logical 
relations to formalize this connection in languages with type 
variables and user-defined types.  We use relational parametricity
to construct a model for an Algol-like language in which interactions 
between local and non-local entities satisfy certain relational 
criteria.  Reasoning about local variables essentially involves 
proving properties of polymorphic functions. The new model supports 
straightforward validations of all the test equivalences that have 
been proposed in the literature for local-variable semantics, 
and encompasses standard methods of reasoning about data 
representations.  It is not known whether our techniques yield fully
abstract semantics.  A model based on partial equivalence relations
on the natural numbers is also briefly examined.

This is an expansion and elaboration of material from
(Continue reading)

lafont | 31 Oct 13:25 1993


Does anybody know the complexity of provability for non commutative  
multiplicative linear logic with units but without atoms?

 The formulae are built from Unit and Bottom using Times and Par.
 The rules are:

                    |- GAMMA, A, GAMMA'    |- DELTA, B, DELTA' 

    -------         ------------------------------------------
    |- Unit         |- DELTA, GAMMA, A Times B, DELTA', GAMMA'

        |- GAMMA, GAMMA'              |- GAMMA, A, B, GAMMA'
    ------------------------         -------------------------
    |- GAMMA, Bottom, GAMMA'         |- GAMMA, A Par B, GAMMA'

 In the Times rule, GAMMA' or DELTA must be empty.

Yves Lafont <lafont@...>.

Allen Stoughton | 28 Oct 16:03 1993

lambda - a program for solving lambda definability problems

An initial release of lambda, a program for solving lambda definability
problems of order at most two, is now available.

The lambda distribution consists of:

* The postscript source for the paper "Mechanizing Logical Relations",
by Allen Stoughton, which describes the theory on which lambda is
based and explains what the program does.  This paper will appear in
the proceedings of the Ninth International Conference on the
Mathematical Foundations of Programming Semantics, LNCS, vol. ?,
Springer-Verlag, 1994, pp. ?-?.  The paper's abstract is:

  We give an algorithm for deciding whether there exists a definable
  element of a finite model of an applied typed lambda calculus that
  passes certain tests, in the special case when all the constants and
  test arguments are of order at most one.  When there is such an
  element, the algorithm outputs a term that passes the tests;
  otherwise, the algorithm outputs a logical relation that demonstrates
  the nonexistence of such an element.  Several example applications of
  the C implementation of this algorithm are considered.

* A short manual page describing lambda.

* The implementation of lambda.  Lambda is written in ANSI C, with the
exception of its lexical analyzer and parser, which are written in lex
and yacc source, respectively.  It uses one UNIX System V system call
(also supported by SunOS Release 4.1).  The C programs that it
generates also conform to the ANSI standard; they use several UNIX
System V system calls (also supported by SunOS Release 4.1) in order
(Continue reading)