[comp.archives] [comp.lang.prolog] A Type checking/reconstruction procedure for Typed-Prolog

lakshman@n.cs.uiuc.edu (T.K. Lakshman) (02/26/91)

Archive-name: languages/prolog/typed-prolog/1991-02-25
Archive: a.cs.uiuc.edu:/pub/reddy/typed-prolog/Types.tar.Z [128.174.252.1]
Original-posting-by: lakshman@n.cs.uiuc.edu (T.K. Lakshman)
Original-subject: A Type checking/reconstruction procedure for Typed-Prolog
Reposted-by: emv@ox.com (Edward Vielmetti)

	 TYPED PROLOG: TYPE CHECKING AND RECONSTRUCTION 
----------------------------------------------------------------------
This is to announce the availability of a type checking/reconstruction
procedure for TYPED PROLOG: a prescriptively typed logic programming 
language. Some features of TYPED PROLOG: 

	*.  Explicit type declarations (following the syntax 
	of type declarations in the Mycroft-O'Keefe type checker)

	*. Typed Semantics based on many sorted logic.
 
	*. Support for a large subset of Prolog: including the (in)famous 
	cut, not, assert and retract.

	*. A type CHECKING and RECONSTRUCTION procedure based on Milner's
	type checking algorithm for ML. The procedure performs: 

	a. TYPE CHECKING : when given a Typed Prolog program with type 
	declarations for all function and predicate symbols, the procedure 
	type-checks the program based on the type rules of Typed Prolog.

	b. TYPE RECONSTRUCTION : when given a Typed Prolog program where type
	declarations for predicate symbols are omitted, the procedure 
	reconstructs the omitted predicate types. 

The user can essentially write ordinary Prolog programs in the standard
syntax and use the above-mentioned implementation to type-check the programs 
and reconstruct omitted types for predicates. 

----------------------------------------------------------------------
	       OBTAINING THE CODE and THE RELATED PAPER
----------------------------------------------------------------------

The type-checking/reconstruction code is written in Prolog and has been
tested on Quintus Prolog (v 3.0), C Prolog (v 1.4) and SB Prolog (v 2.5). 
This type-checking / reconstruction code is available via ANONYMOUS FTP 
as follows: 

Machine:    a.cs.uiuc.edu. (On the login prompt please say anonymous).
Directory:  pub/reddy/typed-prolog 
File:       Types.tar.Z (please don't forget to set BINARY)

The Types.tar.Z file can be tared/uncompressed as follows: 

(uncompress Types.tar.Z; tar xf Types.tar; echo "y" | \
rm Types.tar >/dev/null) &

This  creates the Typed-Prolog directory. This directory contains 
in addition to the type-checking / reconstruction code and examples, a
README file and a dvi and a postscript copy of a related 
Typed Prolog paper.

----------------------------------------------------------------------
-- 
----------------------------------------------------------------------------
INTERNET   : lakshman@cs.uiuc.edu
OFFICE    : 217-244-5973        MAIL    : Dept. of C.S., DCL, 
				1304 W Springfield Ave, Urbana, Il 61801.