λProlog
   HOME

TheInfoList



OR:

λProlog, also written lambda Prolog, is a logic programming language featuring
polymorphic typing In programming language theory and type theory, polymorphism is the provision of a single interface to entities of different types or the use of a single symbol to represent multiple different types.: "Polymorphic types are types whose operati ...
,
modular programming Modular programming is a software design technique that emphasizes separating the functionality of a Computer program, program into independent, interchangeable modules, such that each contains everything necessary to execute only one aspect of th ...
, and
higher-order programming Higher-order programming is a style of computer programming that uses software components, like functions, modules or objects, as values. It is usually instantiated with, or borrowed from, models of computation such as lambda calculus which make ...
. These extensions to
Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
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 the λ-tree syntax approach to ''
higher-order abstract syntax In computer science, higher-order abstract syntax (abbreviated HOAS) is a technique for the representation of abstract syntax trees for languages with variable binders. Relation to first-order abstract syntax An abstract syntax is ''abstract'' b ...
'', 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.


History

Since 1986, λProlog has received numerous implementations. As of 2013, the language and its implementations are still actively being developed. The Abella theorem prover has been designed to provide an interactive environment for proving theorems about the declarative core of λProlog.


See also

* Curry's paradox#Lambda calculus — about inconsistency problems caused by combining (propositional) logic and ''untyped'' lambda calculus


References


Tutorials and texts


Dale Miller
an
Gopalan Nadathur
have written the boo
''Programming with higher-order logic''
published by Cambridge University Press in June 2012.
Amy Felty
has written in 1997 a tutorial o
lambda Prolog and its Applications to Theorem Proving
( rchived by WebCite https://www.webcitation.org/5WpO4HGEh?url=http://www.site.uottawa.ca/~afelty/dist/lprolog97.ps.
John Hannan
has written a tutorial o
Program Analysis in lambda Prolog
for the 1998 PLILP Conference.
Olivier Ridoux
has written ''Lambda-Prolog de A à Z... ou presque'' (163 pages, French). It is available as tp://ftp.irisa.fr/techreports/habilitations/ridoux.ps.gz PostScript tp://ftp.irisa.fr/techreports/habilitations/ridoux.pdf PDF an
html


External links


λProlog homepage


at the Software Preservation Group.


Implementations


The Teyjus λProlog compiler
is currently the oldest implementation still being maintained. This compiler project is led b
Gopalan Nadathur
and various of his colleagues and students.
ELPI: an Embeddable λProlog Interpreter
has been developed b
Enrico Tassi
an
Claudio Sacerdoti Coen
It is implemented in OCaml and is availabl
online
The system is described in
paper
that appeared LPAR 2015. * Th
Abella
prover can be used to prove theorems about λProlog programs and specifications. Prolog programming language family Logic programming languages Logic in computer science {{Compu-lang-stub