headers
ctrs90 | 1 May 1990 13:28
Picon
Picon

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.)

               June 11-14, 1990, Montreal, Canada

                         Sponsored by
           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

Concordia University, Montreal, Quebec, Canada

The CTRS Workshop will take place at the downtown Sir George
(Continue reading)

Permalink | Reply | 0 comments |
headers
jean | 2 May 1990 18:54

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.

Please, REGISTER AS SOON AS POSSIBLE (and send your check)!

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
			   Philadelphia, PA

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

Permalink | Reply | 0 comments |
headers
Pierre-Louis Curien | 4 May 1990 07:44
Picon

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

Permalink | Reply | 0 comments |
headers
Pierre-Louis Curien | 4 May 1990 07:47
Picon

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

Permalink | Reply | 0 comments |
headers
Larry Paulson | 9 May 1990 17:43
Picon

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.

For more information about Isabelle, consult the following:
(Continue reading)

Permalink | Reply | 0 comments |
headers
ctrs90 | 12 May 1990 18:04
Picon
Picon

CTRS '90, reservation date change

               NOTICE ON REGISTRATION FOR CTRS90

             THE SECOND INTERNATIONAL WORKSHOP ON 
            CONDITIONAL AND TYPED REWRITING SYSTEMS

              June 11-14, 1990, Montreal, Canada

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@...
Permalink | Reply | 0 comments |
headers
David.Wolfram%prg.oxford.ac.uk | 16 May 1990 12:42
Picon

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

Permalink | Reply | 0 comments |
headers
Larry Paulson | 23 May 1990 04:52
Picon

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
Permalink | Reply | 0 comments |
headers
Fritz Henglein | 23 May 1990 04:53
Picon

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

Permalink | Reply | 0 comments |
headers
ap%computer | 23 May 1990 20:59
Picon

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

Permalink | Reply | 0 comments |

Gmane