We present a proof-of-concept prototype of a (constructive variant of an) HOL interactive theorem prover written in a Higher Order Logic Programming (HOLP) language, namely an extension of λProlog. The prototype is meant to support the claim, that we reinforce, that HOLP is the class of languages that provides the right abstraction level and programming primitives to obtain concise implementations of theorem provers. We identify and advocate for a programming technique, that we call semi-shallow embedding, while at the same time identifying the reasons why pure λProlog is not sufficient to support that technique, and it needs to be extended.
Dunchev, T., Sacerdoti Coen, C., Tassi, E. (2016). Implementing HOL in an higher order logic programming language. New York, NY, USA : Association for Computing Machinery [10.1145/2966268.2966272].
Implementing HOL in an higher order logic programming language
DUNCHEV, TSVETAN CHAVDAROV;SACERDOTI COEN, CLAUDIO;
2016
Abstract
We present a proof-of-concept prototype of a (constructive variant of an) HOL interactive theorem prover written in a Higher Order Logic Programming (HOLP) language, namely an extension of λProlog. The prototype is meant to support the claim, that we reinforce, that HOLP is the class of languages that provides the right abstraction level and programming primitives to obtain concise implementations of theorem provers. We identify and advocate for a programming technique, that we call semi-shallow embedding, while at the same time identifying the reasons why pure λProlog is not sufficient to support that technique, and it needs to be extended.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
