headers
Frank Pfenning | 2 Oct 1989 16:31
Picon

Program: NACLP'89 Workshop on Types in Logic Programming

To: clp@..., clp.x <at> xerox.com, types <at> theory.LCS.MIT.EDU
Date: Mon, 02 Oct 89 10:37:55 EDT

Program: Special Workshop Session on
	 
		     "Types in Logic Programming"

on Friday, October 20 as part of NACLP'89 at Case Western Reserve
University in Cleveland, Ohio.

If you would like to attend this workshop or are interested in the
abstracts of the talks, send mail to Frank Pfenning <fp@...> on
the Internet.  Below is the tentative workshop schedule.

======================================================================
 9:00-9:30    Kimbal Marriott & Harald Sondergaard
	      Type Inference as Program Analysis

 9:30-10:00   Eyal Yardeni & Ehud Shapiro
	      A Type System for Logic Programs

10:00-10:30   Thom W. Fruehwirth
	      Type Checking with Subtypes in Prolog

  Break

10:45-11:15   Dale Miller & Gopalan Nadathur
	      The Polymorphic Typing of Lambda Prolog

11:15-11:45   Frank Pfenning & Ken Cline
(Continue reading)

Permalink | Reply | 0 comments |
headers
mitchell wand | 4 Oct 1989 22:59

Call for Papers: 1990 ACM Conf. on Lisp & Functional Programming

Date: Wed, 4 Oct 89 15:52:52 EDT
To: theorynt@..., scheme <at> mc.lcs.mit.edu, fp <at> yale.edu,
        types@...

			    1990 ACM Conference on
		       Lisp and Functional Programming

		       Nice, France, June 27--29, 1990

The 1990 ACM Conference on LISP and Functional Programming is the sixth in a
series of biennial conferences devoted to the theory, design, and
implementation of programming languages and systems related to LISP,
functional programming, and symbolic computation.  The conference is jointly
sponsored by ACM SIGPLAN, SIGACT, and SIGART in cooperation with SIGSAM.

Papers presented at the conference must include new ideas or experimental
results that have not been previously published.  Previous conferences have
included papers in the following areas: programming language concepts and
facilities; implementation methods; machine architectures; semantic
foundations; programming logics; and program development environments.  Beyond
these areas, authors are strongly encouraged to submit papers that introduce
important new topics that are relevant to functional programming and symbolic
computation.

Authors should submit 11 copies of a technical summary of a prospective
conference paper.  The length of the summary should not exceed 3,000 words (10
pages double-spaced or typeset 11-point on 16-point spacing).  Since the
committee expects to receive a large number of submissions, the summary should
be organized so that it is easily understood.  It is important for the summary
to identify what has been accomplished, explain why it is significant, and
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin.Pierce | 5 Oct 1989 03:14
Picon

Welcome to SML

To: sml@...
Date: Wed, 04 Oct 89 18:53:52 EDT

This message is to announce the creation of a new mailing list for
users, site maintainers, and developers of the Standard ML of New
Jersey compiler...

The distribution currently includes all site contacts for the SML of
NJ compiler, the members of two smaller lists of developers (ml-lib
and ml-bugs), and a number of users at CMU.  If you are aware of
others at your site that would be interested in participating, please
forward them this message.  (Conversely, if no one at your site is
actually using SML, you may want to request that your address be
dropped from the distribution.)

To send a message to the SML list, address it to

	sml@... 

(sites not connected to the Internet may need additional routing).
Mail to this address is immediately redistributed to the entire list.

Administrative mail such as requests to add or remove names from the
distribution should be addressed to 

	sml-request@...

I'm working with Dave Berry to set up a redistribution at Edinburgh
for sites in the UK.  Some UK addresses are still in the main
distribution so most administrative mail should be sent for now to
(Continue reading)

Permalink | Reply | 0 comments |
headers
dmjones | 5 Oct 1989 18:14
Picon

MIT TOC Seminar--Jerzy Tiuryn--Tue. Oct. 10, 1989

Date: Thu, 5 Oct 89 10:25:37 EDT
To: theory-seminars@...

                Massachusetts Institute of Technology
                    Theory of Computation Seminar

                   DATE: Tuesday, October 10, 1989
                         REFRESHMENTS: 4:00pm
                             TALK: 4:15pm
                           PLACE: NE43-512A

  "Polymorphic Type Reconstruction in ML-like Programming Languages"

                        Professor Jerzy Tiuryn
              University of Warsaw and Boston University
                            Warsaw, Poland

We survey our recent solutions to several problems in the area of type
reconstruction problems for ML, its extensions, and various fragments
of the second-order lambda-calculus:

-- the ML-typability problem is DEXPTIME-complete (settling an open
   problem of Kanellakis and Mitchell).

-- typability in ML+``polymorphic recursion'' is undecidable.

-- typability, in any fixed rank greater than 2, of the second-order
   lambda-calculus with constants is undecidable.

-- typability in rank 2 second-order lambda-calculus is
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 18 Oct 1989 17:20
Picon

Earthquake

To: types@...
Reply-To: John C. Mitchell <jcm@...>
Date: Wed, 18 Oct 89 08:47:54 PDT

Several people have sent messages asking if Stanford is
still standing, so I thought I'd post a message to this list.
Although the epicenter of the quake was closer to Santa Cruz,
the main damage seems to be in SF (since there are bigger
buildings). In the Palo Alto area, the main overpass off of
HWY 101 into the city has apparently collapsed, and several
miles of the other freeway, 280, have buckled and are closed.
Many people have undoubtably lost glassware and other breakables,
but I do not know of any serious injuries or reported deaths
on the Peninsula. There is a gas leak somewhere at Stanford,
and so everyone is encouraged to stay at home (as I am).
It is possible that some of the local aqueducts have been
damaged, and so we are trying to conserve water, even more than
usual.

At the time of the quake, I was giving a slightly technical
talk about typing object-oriented programs to an audience of
not-quite-specialists. The talk started at 4, and at 5:04 I
was trying to wrap up the question session when the walls
started shaking. Several of us ran to the doorway, and others
dove under the large conference table in the middle of the room.
I gather the quake lasted about 15 seconds, but it seemed much
longer. Margaret Jacks Hall has a number of internal  reinforced
concrete pillars, about 2 feet in diameter. The two in the
corners of the conference room shook and swayed. Needless to say, 
there were no further questions about the talk.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Dr.Hans | 19 Oct 1989 17:07

Semi-Unification and Type Inference

Date: Thu, 19 Oct 89 16:49:04 +0100

    DECIDABILITY OF THE SEMI-UNIFICATION PROBLEM IN TWO VARIABLES
                     (H.Leiss, October 19, 1989)

Concerning the announcement of A.J.Kfoury/J.Tiuryn/P.Urcyczyn of the
undecidability of semi-unification (in the types <at> theory of Sept 25),
I want to point out that in June '89 I have shown decidability of the 
semi-unification problem in two variables. This has been reported at
the Computer Science Logic '89 conference, and the paper will (hope-
fully) appear in the proceedings to be published as Springer LNCS.
It also contains a reduction calculus for semi-unification problems
for which I couldn't find any example of nonterminating reductions.

To me it seems extremely unlikely that unsolvable semi-unification
problems will be generated by typability checks for `natural' ML+ programs.

Hans Leiss, 
Siemens AG, 
Otto-Hahn-Ring 6,
D-8000 Munich 83
Permalink | Reply | 0 comments |
headers
coppo%ITOINFO.BITNET | 23 Oct 1989 17:35

Undecidable Second-order Type-Scheme Problem

Date: Mon Oct 23 14:28:50 GMT+0100 1989

Assuming the undecidability of the semiunification problem for a language
without constants (as stated in  a previous message on the Type Net) we can
prove that:
   it is undecidable if a (closed) lambda-term M has a second order type
   that is a (substitution) instance of the type (scheme) t. I.e.,
        there is a simple substitution S such that |- M:St.
Type schemes and simple substitutions are defined in our paper [1].
Type schemes are description of  second order types in which we only fix
the first order structure (arrows and repeated patterns) of the type. Simple
substitutions map type schemes in second order types.
To prove the result we define a lambda-term M and a type scheme t such that
|-M:St for some S, if and only if a given semiunification problem
{(t1,u1),...,(tn,un)} has a solution. (The hypothesis that M is closed is
just for simplicity.)
Of course the result does not imply the undecidability of the inference
problem for the second order lambda-calculus.
                        Paola Giannini, Simona Ronchi.
[1] Paola Giannini, Simona Ronchi, "Characterization of typings in polymorphic
type discipline" LICS 88
Permalink | Reply | 0 comments |
headers
David M. Jones | 30 Oct 1989 17:03
Picon

MIT TOC Seminar--Harry Mairson--Wed Nov 1

Date: Mon, 30 Oct 89 09:44:46 EST
To: theory-seminars@...

                Massachusetts Institute of Technology
                    Theory of Computation Seminar

                  DATE: Wednesday, November 1, 1989
                         REFRESHMENTS: 3:15pm
                             TALK: 3:30pm
                      PLACE: NE43 8th Floor Playroom

                  Deciding ML Typability is Complete
                  for Deterministic Exponential Time

                           Harry G. Mairson
                    Department of Computer Science
                         Brandeis University
                        Waltham, Massachusetts

The functional programming folklore that ML-style expressions can be
typed efficiently is not true.  Some simple ML programs can be
exhibited whose smallest types are enormous -- of exponential size in
the size of the expression.  Indeed, Kanellakis and Mitchell recently
showed that deciding ML expression typability is PSPACE-hard.

We improve the latter result, showing that deciding ML typability is
DEXPTIME-complete.  The proof consists of a straightforward
"simulation" of any deterministic one-tape Turing machine M with input
x running in O(c^{|x|}) time by a polynomial-sized ML formula
Phi_{M,x} such that M accepts x iff Phi_{M,x} is typable.  The key
(Continue reading)

Permalink | Reply | 0 comments |

Gmane