[TYPES/announce] Release of Version 2 of Teyjus --- A Lambda Prolog Implementation

[Xiaochu Qi]

On behalf of the members of the Teyjus project, I am happy to announce the 
release of Version 2 of the Teyjus implementation of Lambda Prolog. To 
recall, Lambda Prolog is a higher-order logic programming language that 
permits lambda terms to be used as representational devices and 
incorporates hypothetical and generic judgments as a means for specifying 
computations over the binding structures of these terms. As such, Lambda 
Prolog provides a convenient vehicle for, amongst other things, encoding 
and animating structural operational semantics specifications.

The earlier Teyjus system, Version 1, embodied an abstract machine based 
implementation of Lambda Prolog and was characterized by a treatment of 
full higher-order unification. Version 2 orients the implementation of the 
language around a deterministic and decidable form of higher-order 
unification known as pattern unification. As such, it represents a 
complete redesign of the abstract machine and a reimplementation of the 
associated emulator and compiler. The new system uses a mix of OCaml and C 
code: the emulator, that requires a proximity to the underlying machine 
for efficiency, is written in C and most other parts exploit the 
high-level features and security of OCaml. Careful attention has also been 
paid to portability of the code: the system has been tested on a variety 
of architectures with varying word sizes (this is an issue because an 
abstract machine emulator is involved) and is also known to run under 
different operating systems.

More details about the Teyjus system and project can be found at

   http://teyjus.cs.umn.edu.

The system is being distributed under a GPL licence. The source code can 
be downloaded using links on the same page.

Regards,
Xiaochu Qi