headers
meyer | 5 Sep 1989 17:17
Picon

Call for Participation: "Types in Logic Programming" Workshop

To: clp@..., types <at> theory.LCS.MIT.EDU
From: Frank Pfenning <Frank.Pfenning@...>
sender: meyer
Reply-To: Frank Pfenning <fp@...>
Date: Wed, 23 Aug 89 11:19:34 EDT

Call for Participation: Special Workshop Session on

		     "Types in Logic Programming"

on Friday, October 20 as part of the North American Conference on Logic
Programming in Cleveland, Ohio.

The role of types in imperative and functional programming is the
subject of much research and often heated debate, yet a relatively
deep understanding of types has been achieved for functional and
imperative languages.  This understanding is embodied in functional
languages such as ML, Miranda, Haskell, and in imperative languages
such as Algol and more recently Forsythe.  Rich type systems have
undeniably had a dramatic impact on the way we think about functional
programming.  But what is the role of types in Logic Programming?  How
do types and logic programming fit?  As in functional programming,
different views of types and their role exist in logic programming,
but the battle-lines are not as clearly drawn and we do not yet have a
deep understanding of the interaction between different views of types
and their possible practical impact.

We are looking for short presentations of approaches to types in logic
programming and their use.  The emphasis is on an exchange of ideas
rather than polished results and we hope to cover a range of topics
(Continue reading)

Permalink | Reply | 0 comments |
headers
N27%TAUNOS.BITNET | 5 Sep 1989 18:23
Picon

JCIT

Date:        Fri,  25 Aug 89 08:05:44 +0200

Mmdf-Warning:  Parse error in original version of preceding line at lcs.mit.edu
To: VARDI@..., HALPERN <at> almvma.lcs.mit.edu,
        MEYER@..., DANDELION!LOTUS!IGREIF <at> EDDIE.MIT.EDU,
        STAN@..., BADLER <at> cis.upenn.edu, BERNARD_GALLER <at> um.cc.umich.edu,
        ULLMAN@..., NSP <at> cis.upenn.edu, FTL <at> BOURBAKI.MIT.EDU,
        JLH@..., AMAREL <at> red.ritgers.edu, CS.AVI <at> r20.utexas.edu,
        FINERMAN@..., ZM <at> sail.stanford.edu, N27 <at> taunos.lcs.mit.edu,
        FRANCEZ@..., DOLEV <at> almvma.lcs.mit.edu,
        SHIMON@..., CHOUEKA <at> bimacs.lcs.mit.edu,
        BEERI@..., dberry <at> techsel.bitnet, dberry <at> cs.ucla.edu,
        SEGALL@..., jacob <at> plex.ai.mit.edu,
        pinter@..., SHAMIR <at> wisdom.lcs.mit.edu,
        SHARIR@..., amir <at> wisdom.lcs.mit.edu, N27 <at> taunos.lcs.mit.edu

Dear Colleague,

The following is a call for papers for The 5th Jerusalem
Conference on Information Technology (JCIT). Please forward
this electronic announcement to as many colleagues of yours
that you believe may be interested in this conference.

Thanks

THE 5th JERUSALEM CONFERENCE ON
INFORMATION TECHNOLOGY (JCIT)

The Technologies of the 90's
(Continue reading)

Permalink | Reply | 0 comments |
headers
tiuryn | 22 Sep 1989 23:44
Favicon

ML Type-Checking is DEXP-complete

Date:  Fri, 22 Sep 89 17:24:16 EDT

To: types@...

A TIGHT LOWER BOUND ON THE COMPLEXITY OF THE TYPABILITY PROBLEM IN ML
               (A.J. Kfoury, J. Tiuryn, and P. Urzyczyn)
                       September 22, 1989

With this note we announce that we have proved that the problem of typability
in ML is EXPTIME hard, thereby improving the PSPACE lower bound given in the
paper by P.C. Kanellakis and J.C. Mitchell "Polymorphic unification and ML
typing" (POPL'89). Thus, putting it together with the known EXPTIME algorithm
that solves the problem, it follows that the problem becomes EXPTIME-complete.

The proof uses two intermediate concepts:
-- a special kind of an automaton with two push-down stores, we refer
   to it as stratified 2pds automaton,
-- a fragment of the semi-unification problem (see our paper of LICS'89 for the
   necessary definitions), to which we refer as acyclic semi-unification 
   problem.

Then the proof breaks into three steps.

1. A polynomial-time reduction of the problem of acceptance of a PSPACE
Alternating Turing Machine to the problem of boundedness of stratified 2pds
automata (an automaton M is bounded iff there is a constant K such that M
can reach at most K different instantaneous descriptions from any given one).

2. A polynomial-time reduction of the problem of boundedness of stratified
2pds automata to the problem of acyclic semi-unification.
(Continue reading)

Permalink | Reply | 0 comments |
headers
tiuryn | 25 Sep 1989 22:10
Favicon

semi-unification is undecidable

Date:  Mon, 25 Sep 89 14:51:12 EDT

          UNDECIDABILITY OF THE SEMI-UNIFICATION PROBLEM
             (A.J. Kfoury, J. Tiuryn, and P. Urzyczyn)
                        September 25, 1989

We are happy to announce the undecidability of the following problem. Given a
finite set of ordered pairs of terms (t1,u1), ..., (tn,un), the terms are over
the language consisting of one binary operation symbol. Are there
substitutions S,R1,...,Rn, such that 

                       Ri(S(ti))=S(ui), holds for every i?

This is the original semi-unification problem, as stated in our LICS'89
paper. The proof of its undecidability procceds as follows.

1. We establish the undecidability of the following problem. Given a 
deterministic Turing machine M, does there exist a constant K such that for 
every instantaneous description, ID, of M the number of different ID's 
reachable from the given one is at most K? The proof of this crucial result 
is obtained by easily adopting the proof of the main result of "The 
undecidability of the Turing machine IMMORTALITY problem", Harvard Ph.D. 
Thesis by Philip K. Hooper, 1965. For the reference to this thesis  we are 
grateful to Albert R. Meyer.

2. We show a recursive reducibility of the above problem to the problem of 
semi-unification.

An immediate consequence of our result is the undecidability of the typability
problem for an extension of ML which allows for a polymorphic recursion. It
(Continue reading)

Permalink | Reply | 0 comments |
headers
Paul Hudak | 27 Sep 1989 15:21
Picon
Favicon

Journal of Functional Programming

Date: Tue, 26 Sep 89 23:05:51 EDT
To: fp@..., types <at> theory.LCS.MIT.EDU, scheme <at> mc.lcs.mit.edu

New journal announcement:

			    JOURNAL OF FUNCTIONAL PROGRAMMING

		A new quarterly journal from Cambridge University Press

				   CALL FOR PAPERS

Background:   Functional Programming languages have features that make them
	      attractive for program synthesis and transformation, parallel
	      processing and novel architecture computers.  Much research is
	      being devoted to their development.  The Journal of Functional
	      Programming is a new journal, the first to be devoted to this
	      important area of computer science.

Coverage:     The Journal of Functional Programming will provide a focus for
	      papers and foster research on all aspects of the subject.  In
	      particular, the journal will cover:  New languages and extensions;
	      Reasoning, proof and program transformation; Program synthesis;
	      Implementation techniques; Type theory; Parallelism; Applications.
	      Papers on declarative languages that deal with combining
	      functional and logic languages will also be appropriate.

Frequency:    The Journal of Functional Programming will have two issues in its
	      first year (1990), each of 128 pages.  Thereafter it will appear
	      quarterly.
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 29 Sep 1989 14:13
Picon

Abstract for "Logic from Computer Science"

Date: Thu, 28 Sep 89 15:54:45 PDT
To: ynm@...
Cc: types@...

          PCF considered as a programming language

                     John C. Mitchell
               Computer Science Department
                   Stanford University

                     Talk Abstract

This talk is about reduction properties of a lazy typed lambda 
calculus PCF with functions, pairing, and fixed-point operators at
all types. This language has been used as an example programming
language in past theoretical studies and, with the addition
of numerals and a few basic operations, it is sufficient to
define all partial recursive functions. The natural equational
axioms include eta-equivalence and the so-called "surjective 
pairing" axiom for pairs. However, if we define reduction R by 
directing each equational axiom, the resulting system is not 
confluent. This raises the question: Is there a confluent set of 
reduction rules which seems computationally sufficient? Moreover, 
how do we characterize the sufficiency of this set of rules? 
We are interested in answers which apply to PCF over common 
algebraic data types such as natural numbers, booleans, lists,
trees, etc., rather than the pure calculus.

We show that the reduction system R- obtained by dropping eta 
and surjective pairing has the following properties:
(Continue reading)

Permalink | Reply | 0 comments |

Gmane