Implementing HOL in an Higher Order Logic Programming Language

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.
Type de document :
Communication dans un congrès
Logical Frameworks and Meta Languages: Theory and Practice, Jun 2016, Porto, Portugal. ACM, pp.10, 2016, LFMTP '16. 〈10.1145/2966268.2966272〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01394686
Contributeur : Enrico Tassi <>
Soumis le : mercredi 9 novembre 2016 - 15:56:37
Dernière modification le : jeudi 11 janvier 2018 - 16:48:44
Document(s) archivé(s) le : mercredi 15 mars 2017 - 04:13:08

Fichier

holsuperlight.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi. Implementing HOL in an Higher Order Logic Programming Language. Logical Frameworks and Meta Languages: Theory and Practice, Jun 2016, Porto, Portugal. ACM, pp.10, 2016, LFMTP '16. 〈10.1145/2966268.2966272〉. 〈hal-01394686〉

Partager

Métriques

Consultations de la notice

100

Téléchargements de fichiers

79