Proof-Theoretic Foundation of Compilation in Logic Programming Languages

2002-04-01T00:00:00Z (GMT) 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.