research-article

Implementing HOL in an Higher Order Logic Programming Language

Authors:

Cvetan Dunchev,

Claudio Sacerdoti Coen,

Enrico TassiAuthors Info & Claims

LFMTP '16: Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Article No.: 4, Pages 1 - 10

https://doi.org/10.1145/2966268.2966272

Published: 23 June 2016 Publication History

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.

References

[1]

A. W. Appel and A. P. Felty. Lightweight Lemmas in lambda-Prolog. In Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29-December 4, 1999, pages 411--425. MIT Press, 1999. ISBN 0-262-54104-1.

Digital Library

[2]

R. Arthan. On Definitions of Constants and Types in HOL. Journal of Automated Reasoning, 56(3):205--219, 2016. ISSN 1573-0670.

Digital Library

[3]

A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. Hints in Unification. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pages 84--98, 2009.

Digital Library

[4]

P. Baillot and M. Hofmann. Type Inference in Intuitionistic Linear Logic. In Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria, pages 219--230, 2010.

Digital Library

[5]

R. Blanco, Z. Chihani, and D. Miller. Translating between implicit and explicit versions of proof. Unpublished, 2015. URL http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/implicit-explicit-draft.pdf.

[6]

Z. Chihani, D. Miller, and F. Renaud. Foundational Proof Certificates in First-Order Logic. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, pages 162--177, 2013.

Digital Library

[7]

N. G. de Bruijn. Lambda calculus with namefree formulas in involving symbols that represent reference transforming mappings. In Indagationes Mathematicae, volume 81(3), pages 348--356, 1978.

[8]

D. Delahaye. A Tactic Language for the System Coq. In Logic for Programming and Automated Reasoning: 7th International Conference, LPAR 2000 Reunion Island, France, November 6-10, 2000 Proceedings, pages 85--95. Springer Berlin Heidelberg, 2000. ISBN 978-3-540-44404-6.

Digital Library

[9]

C. Dunchev, F. Guidi, C. Sacerdoti Coen, and E. Tassi. ELPI: Fast, Embeddable, lambda-Prolog Interpreter. In Logic for Programming, Artificial Intelligence and Reasoning: 20th International Conference, LPAR-20 2015, Suva, Fiji, 2015, Proceedings, pages 460--468. Springer Berlin Heidelberg, 2015. ISBN 978-3-662-48899-7.

[10]

A. P. Felty. Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language. J. Autom. Reasoning, 11(1):41--81, 1993.

[11]

A. P. Felty and D. Miller. Specifying theorem provers in a higher-order logic programming language. In 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pages 61--80, 1988.

Digital Library

[12]

T. Frhwirth. Theory and practice of constraint handling rules. The Journal of Logic Programming, 37(13):95--138, 1998. ISSN 0743-1066.

[13]

E. Giachino, E. B. Johnsen, C. Laneve, and K. I. Pun. Time complexity of concurrent programs. CoRR, abs/1511.05104, 2015.

Digital Library

[14]

M. J. C. Gordon and A. M. Pitts. The HOL logic and system. In J. Bowen, editor, Towards Verified Systems, volume 2 of Real-Time Safety Critical Systems, chapter 3, pages 49--70. Elsevier Science B.V., 1994.

[15]

M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer, 1979. ISBN 3-540-09724-4.

[16]

J. Harrison. HOL light: An overview. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pages 60--66, 2009a.

Digital Library

[17]

J. Harrison. HOL Light: An Overview. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pages 60--66, Berlin, Heidelberg, 2009b. Springer Berlin Heidelberg. ISBN 978-3-642-03359-9.

Digital Library

[18]

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system release 3.08, Documentation and users manual. In Projet Cristal, INRIA, 2004.

[19]

A. Mahboubi and E. Tassi. Canonical Structures for the Working Coq User. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pages 19--34, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. ISBN 978-3-642-39634-2.

Digital Library

[20]

D. Miller. Unification Under a Mixed Prefix. J. Symb. Comput., 14(4): 321--358, 1992.

Digital Library

[21]

D. Miller. Foundational Proof Certificates. In All about Proofs, Proofs for All (APPA), pages 150--163, 2014.

[22]

G. Nadathur and D. J. Mitchell. System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog. In Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pages 287--291, 1999.

Digital Library

[23]

G. Nadathur and G. Tong. Realizing Modularity in lambdaProlog. Journal of Functional and Logic Programming - March 15, 1999, 1999(Special Issue 2), 1999.

[24]

C. Sacerdoti Coen, E. Tassi, and S. Zacchiroli. Tinycals: Step by Step Tacticals. Electr. Notes Theor. Comput. Sci., 174(2):125--142, 2007.

Digital Library

[25]

A. Spiwack. An abstract type for constructing tactics in Coq. In Proof Search in Type Theory, Edinburgh, United Kingdom, July 2010a. URL https://hal.inria.fr/inria-00502500.

[26]

A. Spiwack. An abstract type for constructing tactics in coq. Unpublished, 2010b. URL http://assert-false.net/arnaud/papers/An%20abstract%20type%20for%20constructing%20tactics%20in%20Coq.pdf.

[27]

I. Whiteside, D. Aspinall, L. Dixon, and G. Grov. Towards Formal Proof Script Refactoring. In Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings, pages 260--275, 2011.

Digital Library

[28]

F. Wiedijk. The Seventeen Provers of the World: Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006. ISBN 3540307044.

Digital Library

Cited By

GUIDI FSACERDOTI COEN CTASSI E(2019)Implementing type theory in higher order constraint logic programmingMathematical Structures in Computer Science10.1017/S0960129518000427(1-26)Online publication date: 1-Mar-2019
https://doi.org/10.1017/S0960129518000427
Miller D(2018)Mechanized Metatheory RevisitedJournal of Automated Reasoning10.1007/s10817-018-9483-3Online publication date: 4-Oct-2018
https://doi.org/10.1007/s10817-018-9483-3

Index Terms

Implementing HOL in an Higher Order Logic Programming Language
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
      2. Language types

Recommendations

Specifying and implementing theorem provers in a higher-order logic programming language
Self-Formalisation of Higher-Order Logic

We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison's ...
An embedding of the ACL2 logic in HOL
ACL2 '06: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications

We describe an embedding of the ACL2 logic into higher-order logic. An implementation of this embedding allows ACL2 to be used as an oracle for higher-order logic provers.

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences

LFMTP '16: Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

June 2016

41 pages

ISBN:9781450347778

DOI:10.1145/2966268

Conference Chair:
Sandra Alves,
Program Chairs:
Gilles Dowek,
Daniel R. Licata

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 June 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LFMTP '16

LFMTP '16: Theory and Practice

June 23, 2016

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 11 of 20 submissions, 55%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
98
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

GUIDI FSACERDOTI COEN CTASSI E(2019)Implementing type theory in higher order constraint logic programmingMathematical Structures in Computer Science10.1017/S0960129518000427(1-26)Online publication date: 1-Mar-2019
https://doi.org/10.1017/S0960129518000427
Miller D(2018)Mechanized Metatheory RevisitedJournal of Automated Reasoning10.1007/s10817-018-9483-3Online publication date: 4-Oct-2018
https://doi.org/10.1007/s10817-018-9483-3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten