λ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 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.

λProlog
ParadigmLogic programming
Designed byDale Miller and Gopalan Nadathur
First appeared1987[1]
Typing disciplinestrongly typed
LicenseGNU General Public License v3
Websitewww.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/
Major implementations
Teyjus, ELPI
Influenced by
Prolog
Influenced
Makam

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

References

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

Tutorials and texts

Implementations


  1. 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.