DUNCHEV , Cvetan

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

We present a new interpreter for λProlog that runs consistently faster than the byte code compiled by Teyjus, that is believed to be the best available implementation of λProlog. The key insight is the identification of a fragment of the language, which we call reduction-free fragment (L β λ), that occurs quite naturally in λProlog programs and...