An overview of λProlog

By Gopalan Nadathur and Dale Miller, from ICLP 88, available from the λProlog website:

λProlog is a logic programming language that extends Prolog by incorporating notions of higher-order functions, λ-terms, higher-order unification, polymorphic types, and mechanisms for building modules and secure abstract data types. These new features are provided in a principled fashion by extending the classical first-order theory of Horn clauses to the intuitionistic higher-order theory of hereditary Harrop formulas. The justification for considering this extension a satisfactory logic programming language is provided through the proof-theoretic notion of a uniform proof. The correspondence between each extension to Prolog and the new features in the stronger logical theory is discussed. Also discussed are various aspects of an experimental implementation of λProlog.

EDIT: Teyjus 2.0 is available.

2 Responses to “An overview of λProlog”


  1. 1 Zach Snow October 21, 2009 at 12:52 am

    I thought I would mention the relatively recent release of Teyjus 2.0, an implementation of lambdaProlog from Dr. Nadathur’s group (disclaimer: of which I am a part). See http://code.google.com/p/teyjus/ if you are interested.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: