1 May 13:28 1990

### CTRS '90 (Program)

Date: Mon, 30 Apr 90 23:57:46 -0400

THE SECOND INTERNATIONAL WORKSHOP ON
CONDITIONAL AND TYPED REWRITING SYSTEMS
(CTRS '90)

THIRD ANNOUNCEMENT
(Information on program, accomodation, registration, etc.)

Centre de recherche informatique de Montreal
and
Concordia University

with support from
Natural Sciences and Engineering Research Council of Canada

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

TIME

June 11-14, 1990, beginning at 9:30 A.M. on June 11.

PLACE

The CTRS Workshop will take place at the downtown Sir George


2 May 18:54 1990

### LICS '90, EARLY REGISTRATION DEADLINE

Date: Wed, 02 May 90 07:46:52 -0400

This is a reminder that the deadline for
early (and cheaper!) registration for LICS '90 is  5/11/90.

LIMITED funding is still available for exceptional cases,
with priority given to students. Send mail to:

jean@...

---------------------------------------------------------------
Fifth Annual IEEE Symposium on Logic in Computer Science

June 4-7, 1990

IEEE Technical Committee on Mathematical Foundations of Computing
in cooperation with
Association for Computing Machinery -- SIGACT
Association for Symbolic Logic
European Association for Theoretical Computer Science

INQUIRIES:
---------

Email registration forms followed by regularly posted checks will be
gratefully received.  Further travel information will be sent by email


4 May 07:44 1990

### Conference on CATEGORY THEORY AND COMPUTER SCIENCE

Date: Wed, 2 May 90 22:58:13 +0200

CATEGORY THEORY AND COMPUTER SCIENCE

(first announcement and call for papers)

3-6 September 1991
Ecole Normale Superieure, Paris

The Fourth of the biennial Summer Conferences on Category
Theory and Computer Science will be held in Paris. The main purpose of
these conferences is to link research in category theory with computer
science. The importance of categories in understanding basic issues in
computer science is now well established. Other structures in logic,
algebra and topology are also seen as fundamental and the scope of the
conference is to cover applications of these structures as well.
Papers are welcome in any of the following, non-exhaustive, list of
topics :

% Semantics of Programming Languages    % Categorical Logic
% Program Logics and Specification      % Semantics of Concurrency
% Type Theory                           % Linear Logic

It is intended to publish the proceedings as Springer Lecture Notes.

Organizing and Program Committee Samson Abramsky, Pierre-Louis Curien,
Peter Dybjer, Giuseppe Longo, John Mitchell,David Pitt, Andrew Pitts,
Axel Poign, David Rydeheard, Don Sannella, Eric Wagner.

Important Dates


4 May 07:47 1990

### On confluence of simply typed Beta

Date: Wed, 2 May 90 22:50:08 +0200

I would like to communicate the following proof of confluence of Beta
in the simply typed Lambda-calculus, which makes use of weak
normalization only. It stands as a nice curiosity between the proofs
which mimick the proof of untyped Beta+Eta confluence, and those which
rely on strong normalization. It is an illustration of the following
general technique to transfer confluence from a system to another.

Let me first explain the general technique. One may establish the
confluence of a system A, by making use of a translation of A into a
system B via a mapping G s.t.

A1) B is confluent
A2) A is weakly normalizing
A3)  If a -> a' in A, then G(a) and G(a')  are B-interconvertible
A4) G translates A-normal forms injectively to B-normal forms.

It is easy to see that A1-A4 entail the confluence of A.

Here is how I use the technique to show the confluence of Beta
in the simply typed Lambda-calculus. It is rather easy to prove strong
termination of the following restriction of the b- reduction:
(Lambda x.M)N -> M[N/x] only when N is in normal form.  Here
is a short argument, adapted from, say the book of
Girard-Lafont-Taylor, chapter 4: with every term P associate the
multiset of the degrees (i.e. the size of the type A[B of lx.M) of the
redexes (Lambda x.M)N of P. Then the restricted reduction relation
strictly decreases this measure (the fundamental fact being that
created redexes have smaller degrees than the creating redex).


9 May 17:43 1990

### Isabelle available by FTP

Date: Wed, 9 May 90 15:26:02 BST
To: ailist%ai.ai.mit.edu@...,
info-hol%clover.ucdavis.edu@...,
logic@..., proof-sci%cs.chalmers.se <at> nsfnet-relay.ac.uk,
types@...

Theorem Prover ISABELLE now available by FTP

Isabelle is now available for anonymous ftp from princeton.edu and
research.att.com.  It now has a nonrestrictive copyright notice similar to
that of the X Windows system.  This means you do not need to sign a license
to obtain a copy of Isabelle, and you are free to redistribute Isabelle as
long as you retain the copyright notices and permission notice.

Thanks to Andrew Appel and David MacQueen for making Isabelle available by
ftp. Isabelle resides on the same directory as Standard ML of New Jersey.
Note however that Isabelle was developed using a different compiler, called
Poly/ML. Although Isabelle has been tested under SML of New Jersey, the
compilers are not completely compatible. In particular, the Makefiles will
only work for Poly/ML.

Isabelle is a generic theorem prover. It suppports interactive proof in
several formal systems, including first-order logic (intuitionistic and
classical), higher-order logic, Martin-L\"of type theory, and
Zermelo-Fraenkel set theory. New logics can be introduced by specifying
their syntax and rules of inference. Both natural deduction and sequent
calculi are allowed. Proof procedures (tactics and tacticals) can be
expressed using Standard ML.



12 May 18:04 1990

### CTRS '90, reservation date change

               NOTICE ON REGISTRATION FOR CTRS90

THE SECOND INTERNATIONAL WORKSHOP ON
CONDITIONAL AND TYPED REWRITING SYSTEMS

Due to the delay in distributing the third announcement, the due date
for reservation of rooms at the university dormitory has been extended
to May 21.

The program and other information are available upon your request from
ctrs90@...


16 May 12:42 1990

### Clausal Theory of Types'' from Cambridge Univ. Press

Date: Tue, 15 May 90 11:43:15 BST

Cambridge University Press
Cambridge Tracts in Theoretical Computer Science

Forthcoming Title

THE CLAUSAL THEORY OF TYPES

D.A. Wolfram
Oxford University Computing Laboratory
Programming Research Group

This book introduces  a  theoretical  basis  for  resolution
theorem  proving  with  a  lambda  calculus formulation of a
higher-order clausal logic with equality, called the Clausal
Theory  of  Types.   The  fundamental Skolem-Herbrand-Goedel
Theorem and resolution are  generalized to the  higher-order
setting.  Operationally,  this  requires the introduction of
higher-order   equational   unification,   which   builds-in
higher-order equational theories.

When restricted to higher-order Horn clauses,  a  foundation
for  an  expressive  logic  programming language is provided
which has the unique properties of being sound and  complete
with respect to Henkin-Andrews general models, and of treat-
ing functionally equivalent terms as  identical.   Canonical
general  model  theoretic  characterizations of provable and
finitely-failed formulas are  presented for  Clausal  Theory
of  Types  Horn  clauses,  which extrapolate the first-order


23 May 04:52 1990

### what are dependent types??

Date: Mon, 21 May 90 14:34:04 BST

The term "dependent type" was, I think, coined at Cornell to explain the
Pi and Sigma types as generalizations of function and (binary) product types.
The Pi type was called the "dependent function type" and the Sigma type was
called the "dependent product type". This gave the right intuition, but
unfortunately the dependent product type was in fact a sum type.

An alternative terminology is now often seen: the Pi type is called the
"dependent product type" and the Sigma type is called the "dependent sum
type". This avoids the problem with the Cornell terminology, but loses the
original intuition; it is not clear whether "dependent" means anything any
more.

A recent paper combines these terminologies: Pi is called the dependent
function type and Sigma is called the dependent sum type.  This appears to
be an error, but it suggests that the terminology of dependent types is too
confusing to be useful. Why can't Pi and Sigma types just be called Pi and
Sigma types? If a more formal terminology is required, how about "general
product" and "general sum"?

Larry Paulson


23 May 04:53 1990

### Lower bound on System F typability

Date: Tue, 22 May 90 15:40:36 met

A Lower Bound for Full Polymorphic Type Inference:
Girard-Reynolds Typability is DEXPTIME-hard

Fritz Henglein
(Utrecht University)

Abstract:

The typability problem  for the Girard-Reynolds Calculus  (also called
Second Order Lambda  Calculus  or System  F) is   an old and   elusive
problem.  Neither  nontrivial upper nor lower  bounds have been known,
not  even whether the  problem is decidable  or not.  In this paper we
present  the, as  far as we   know, first nontrivial  lower bound  for
Girard-Reynolds  typability.   Expanding on  work   by Kanellakis  and
Mitchell and, in particular, Mairson on ML typability we prove that GR
typability is DEXPTIME-hard.

Mairson's   proof of DEXPTIME-hardness of ML   typability relies on an
encoding of Boolean values by  type schemes with equality between some
components of the type scheme.  This type equality can be forced in ML
due to ML's monomorphic typing rule for lambda-bound variables.  Since
this equality  cannot  be  forced  in  the Girard-Reynolds   Calculus,
Mairson's proof  cannot naively be  transferred to the Girard-Reynolds
typability problem.

We show  that a  conventional (untyped) lambda-calculus representation
of Boolean values,   together with an  analogue of  Mairson's  fan-out
gates, results in    a straightforward simulation  of a  deterministic


23 May 20:59 1990

### Re: what are dependent types??

To: Larry Paulson < <at> nsfnet-relay.ac.uk:lcp@...>
Cc: types@...
Date: Wed, 23 May 90 09:52:56 +0100

Well, in my book (yet to be written!) dependent' types are type
expressions which contain (hence DEPEND on) variables---in contrast
with simple types' (as in "simply typed lambda calculus") which do not.

Within the context of such dependent types, there are sum types
($\Sigma) x\in A.B(x)$) and product types ($\Pi x\in A.B(x)$).  Then
it's a useful short-hand to refer to dependent sum types' and
dependent product types'.

I like the (Cornell?) terminology of dependent product type' for
\Sigma and dependent function type' for \Pi because it reminds you
that in the special case of no dependency (i.e. for simple types) the
notions specialize to the usual binary product and function type.
However, I don't use that terminology because I judge that the use of
the terms dependent sum' and  dependent product' are generally
accepted (and more importantly, generally understood).

Finally, don't forget that

"Exessive concern with terminology gives a subject a bad name."

Anon

Andy Pitts