ΛProlog

λProlog, also written lambda Prolog, is a logic programming language featuring polymorphic typing, modular programming, and higher-order programming. These extensions to Prolog are derived from the higher-order hereditary Harrop formulas used to justify the foundations of λProlog. Higher-order quantification, simply typed λ-terms, and higher-order unification gives λProlog the basic supports needed to capture "higher-order abstract syntax", an approach to representing syntax that maps object-level bindings to programming language bindings. Programmers in λProlog need not deal with bound variable names: instead various declarative devices are available to deal with binder scopes and their instantiations. Since 1986, λProlog has received numerous implementations.

External links

* [http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/ λProlog homepage]

Implementations

* [http://teyjus.cs.umn.edu/ The Teyjus λProlog compiler] is the most recent and effective implementation to date. This compiler project is led by [http://www-users.cs.umn.edu/~gopalan/ Gopalan Nadathur] and various of his colleagues and students.

Tutorials

* [http://www.irisa.fr/prive/ridoux/ Olivier Ridoux] has written "Lambda-Prolog de A à Z... ou presque" (163 pages, French). It is available as [ftp://ftp.irisa.fr/techreports/habilitations/ridoux.ps.gz PostScript] , [ftp://ftp.irisa.fr/techreports/habilitations/ridoux.pdf PDF] , and [http://www.irisa.fr/lande/ridoux/LPAZ/lpaz_html.html html] .
* [http://www.cse.psu.edu/~hannan/ John Hannan] has written a tutorial on [http://www.cse.psu.edu/~hannan/papers/plilp-tutorial.ps.gz Program Analysis in lambda Prolog] for the 1998 PLILP Conference.
* [http://www.site.uottawa.ca/~afelty/ Amy Felty] has written in 1997 a tutorial on [http://www.site.uottawa.ca/~afelty/dist/lprolog97.ps lambda Prolog and its Applications to Theorem Proving] (Archived by WebCite® [http://www.webcitation.org/5WpO4HGEh] ).