λProlog

λProlog
Paradigm	Logic programming
Designed by	Dale Miller and Gopalan Nadathur
First appeared	1987[1]
Typing discipline	strongly typed
License	GNU General Public License v3
Website	www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/
Major implementations
	Teyjus, ELPI
Influenced by
	Prolog
Influenced
	Makam

λ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 the λ-tree syntax approach to 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.

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.

gollark: Or just complain about them being "brainwashed" at school or something.

gollark: Them not being that is somewhat more complicated and non-obvious?

gollark: I mean, economies of scale.

gollark: Never mind, pretty sure that was entirely comprehensible.

gollark: Hmm, my code seems to be doing incomprehensible things.

References

"FAQ: What implementations of lambda Prolog are available?". www.lix.polytechnique.fr. Retrieved 2019-12-16.

Tutorials and texts

Dale Miller and Gopalan Nadathur have written the book Programming with higher-order logic, published by Cambridge University Press in June 2012.
Amy Felty has written in 1997 a tutorial on lambda Prolog and its Applications to Theorem Proving ([Archived by WebCite https://www.webcitation.org/5WpO4HGEh?url=http://www.site.uottawa.ca/~afelty/dist/lprolog97.ps]).
John Hannan has written a tutorial on 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 PostScript, PDF, and html.

External links

λProlog homepage

Implementations

The Teyjus λProlog compiler is currently the oldest implementation still being maintained.[1] This compiler project is led by Gopalan Nadathur and various of his colleagues and students.
ELPI: an Embeddable λProlog Interpreter has been developed by Enrico Tassi and Claudio Sacerdoti Coen. It is implemented in OCaml and is available online. The system is described in a paper that appeared LPAR 2015.
The Abella prover can be used to prove theorems about λProlog programs and specifications.

Nadathur, Gopalan; Dustin Mitchell (1999). System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda Prolog. Conference on Automated Deduction. LNAI. 1632. pp. 287–291. doi:10.1007/3-540-48660-7_25. ISBN 978-3-540-66222-8.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[1] "FAQ: What implementations of lambda Prolog are available?". www.lix.polytechnique.fr. Retrieved 2019-12-16.

[2] Nadathur, Gopalan; Dustin Mitchell (1999). System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda Prolog. Conference on Automated Deduction. LNAI. 1632. pp. 287–291. doi:10.1007/3-540-48660-7_25. ISBN 978-3-540-66222-8.