[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
