file.pdf (231.06 kB)
Download file

Proof-Theoretic Foundation of Compilation in Logic Programming Languages

Download (231.06 kB)
journal contribution
posted on 01.04.2002, 00:00 by Iliano Cervesato
Commercial implementations of logic programming languages are engineered Appeared in the Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming — JICSLP’98 (J. Jaffar editor), pp ??–??, MIT Press, Manchester, UK, 16–19 June 1998. around a compiler based on Warren’s Abstract Machine (WAM) or a variant of it. In spite of various correctness proofs, the logical machinery relating the proof-theoretic specification of a logic programming language and its compiled form is still poorly understood. In this paper, we propose a logicindependent definition of compilation for logic programming languages. We apply this methodology to derive the first cut of a compiler and the corresponding abstract machine for the language of hereditary Harrop formulas and then for its linear refinement.

History

Date

01/04/2002

Usage metrics

Exports