article

HOLCF = HOL + LCF

Authors:

David Von Oheimb,

Oscar SlotoschAuthors Info & Claims

Journal of Functional Programming, Volume 9, Issue 2

Pages 191 - 223

https://doi.org/10.1017/S095679689900341X

Published: 01 March 1999 Publication History

Abstract

HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF supports standard domain theory (in particular fixpoint reasoning and recursive domain equations), but also coinductive arguments about lazy datatypes. This paper describes in detail how domain theory is embedded in HOL, and presents applications from functional programming, concurrency and denotational semantics.

References

[1]

Agerholm, S. (1994a) Formalising a model of the ¿-calculus in HOL-ST. Technical Report 354, University of Cambridge Computer Laboratory.

[2]

Agerholm, S. (1994b) A HOL basis for reasoning about functional programs. PhD thesis, Department of Computer Science, University of Aarhus. (BRICS report RS-94-44.).

[3]

Agerholm, S. (1995) LCF examples in HOL. The Computer J., 38, 121-130.

[4]

Audebaud, P. (1991) Partial objects in the calculus of constructions. 6th IEEE Symp. Logic in Computer Science, pp. 86-95. IEEE Press.

[5]

Bartels, F., Dold, A., von Henke, F., Pfeifer, H. and Rueß, H. (1996) Formalizing fixed-point theory in PVS. Technical Report, Universität Ulm.

[6]

Constable, R. and Smith, S. (1987) Partial objects in constructive type theory. 2nd IEEE Symp. Logic in Computer Science, pp. 183-193. IEEE Press.

[7]

Constable, R. L. et al. (1986) Implementing Mathematics with the NURPL Proof Development System. Prentice-Hall.

[8]

Crary, K. (1998) Admissibility of fixpoint induction over partial types. In: Kirchner, C. and Kirchner, H. (eds), Automated Deduction -- CADE-15: Lecture Notes in Computer Science 1421, pp. 270-285. Springer-Verlag.

[9]

Devillers, M., Griffioen, D. and Müller, O. (1997) Possibly infinite sequences in theorem provers: A comparative study. In: Gunter, E. L. and Felty, A. (eds), Theorem Proving in Higher Order Logics: Lecture Notes in Computer Science 1275, pp. 89-104. Springer-Verlag.

[10]

Gordon, M. C. J., Milner, R. and Wadsworth, C. P. (1979) Edinburgh LCF: a mechanised logic of computation: Lecture Notes in Computer Science 78. Springer-Verlag.

[11]

Gordon, M. J. C. and Melham, T. F. (eds). (1993) Introduction to HOL: A theorem-proving environment for higher order logic. Cambridge University Press.

[12]

Hudak, P., Peyton Jones, S. and Wadler, P. (1992) Report on the programming language Haskell: A non-strict, purely functional language. ACM SIGPLAN Notices, 27(5).

Digital Library

[13]

Lynch, N. and Tuttle, M. (1989) An introduction to Input/Output automata. CWI Quarterly, 2(3), 219-246.

[14]

Müller, O. (1998a) I/O automata and beyond - temporal logic and abstraction in Isabelle. In: Grundy, J. and Newey, M. (eds), Theorem Proving in Higher Order Logics (TPHOLs'98): Lecture Notes in Computer Science 1479, pp. 1-18. Springer-Verlag.

[15]

Müller, O. (1998b) A verification environment for I/O-automata based on formalized meta-theory . PhD thesis, Institut für Informatik, Technical Universität München.

[16]

Müller, O. and Nipkow, T. (1997) Traces of I/O automata in Isabelle/HOLCF. In: Bidoit, M. and Dauchet, M. (eds), Tapsoft'97: Theory and practice of software development: Lecture Notes in Computer Science 1214, pp. 580-594. Springer-Verlag.

[17]

Nipkow, T. (1993) Order-sorted polymorphism in Isabelle. In: Huet, G. and Plotkin, G. (eds), Logical Environments, pp. 164-188. Cambridge University Press.

[18]

Nipkow, T. (1996) Winskel is (almost) right: Towards a mechanized semantics textbook. In: Chandru, V. and Vinay, V. (eds), Foundations of Software Technology and Theoretical Computer Science: Lecture Notes in Computer Science 1180, pp. 180-192. Springer-Verlag.

[19]

Nipkow, T. (1998a) Isabelle/HOL. The Tutorial. Unpublished Manuscript. (Available at www.in.tum.de/~nipkow/pubs/HOL.html.)

[20]

Nipkow, T. (1998b) Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10, 171-186.

[21]

Nipkow, T. and Slind, K. (1995) I/O automata in Isabelle/HOL. In: Dybjer, P., Nordström, B. and Smith, J. (eds), Types for Proofs and Programs: Lecture Notes in Computer Science 996, pp. 101-119. Springer-Verlag.

[22]

Oheimb, D. von. (1995) Datentypspezifikationen in Higher-Order LCF. MPhil thesis, Technische Universität München.

[23]

Paulson, L. C. (1985) Verifying the unification algorithm in LCF. Science of Computer Programming, 5, 143-169.

[24]

Paulson, L. C. (1987) Logic and Computation. Cambridge University Press.

[25]

Paulson, L. C. (1994) Isabelle: A generic theorem prover: Lecture Notes in Computer Science 828. Springer-Verlag.

[26]

Paulson, L. C. (1997) Generic automatic proof tools. In: Veroff, R. (ed), Automated reasoning and its applications. MIT Press. (Also Report 396, Computer Laboratory, University of Cambridge.).

[27]

Regensburger, F. (1994) HOLCF: Eine konservative Erweiterung von HOL um LCF. PhD thesis, Technische Universität München.

[28]

Regensburger, F. (1995) HOLCF: Higher Order Logic of Computable Functions. In: Schubert, E. T., Windley, P. J. and Alves-Foss, J. (eds), Higher Order Logic Theorem Proving and its Applications: Lecture Notes in Computer Science 971, pp. 293-307. Springer-Verlag.

[29]

Slind, K. (1996) Function definition in higher order logic. In: von Wright, J., Grundy, J. and Harrison, J. (eds), Theorem Proving in Higher Order Logics: Lecture Notes in Computer Science 1125, pp. 381-397. Springer-Verlag.

[30]

Slotosch, O. (1997a) Higher order quotients and their implementation in isabelle hol. In: Gunter, E. L. and Felty, A. (eds), Theorem proving in higher order logics: Lecture Notes in Computer Science 1275, pp 291-306. Springer-Verlag.

[31]

Slotosch, O. (1997b) Refinements in HOLCF: Implementation of interactive systems. PhD thesis, Institut für Informatik, TU München.

[32]

Wenzel, M. (1997) Type classes and overloading in higher-order logic. In: Gunter, E. L. and Felty, A. (eds), Theorem Proving in Higher Order Logics: Lecture Notes in Computer Science, pp. 307-322. Springer-Verlag.

[33]

Winskel, G. (1993) The Formal Semantics of Programming Languages. MIT Press.

Cited By

Ballenghien BWolff B(2024)A Theory of Proc-Omata—and Proof Methods for Process ArchitecturesTheoretical Aspects of Computing – ICTAC 202410.1007/978-3-031-77019-7_16(272-289)Online publication date: 25-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-77019-7_16
Kanabar HVivien SAbrahamsson OMyreen MNorrish MPohjola JZanetti R(2023)PureCake: A Verified Compiler for a Lazy Functional LanguageProceedings of the ACM on Programming Languages10.1145/35912597:PLDI(952-976)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591259
Kună?Ar OPopescu A(2019)A Consistent Foundation for Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-018-9454-862:4(531-555)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s10817-018-9454-8
Show More Cited By

HOLCF = HOL + LCF

Recommendations

From LCF to Isabelle/HOL
Special Issue on History of Formal Methods
Abstract
Interactive theorem provers have developed dramatically over the past four decades, from primitive beginnings to today’s powerful systems. Here, we focus on Isabelle/HOL and its distinctive strengths. They include automatic proof search, borrowing ...
PNL to HOL: From the logic of nominal sets to the logic of higher-order functions

Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the @?-quantifier or @l-binder are just term-formers satisfying ...
Higher-Order Separation Logic in Isabelle/HOLCF

We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a way that one may use any theory defined in Isabelle/HOLCF to construct ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Functional Programming

Journal of Functional Programming Volume 9, Issue 2

March 1999

131 pages

ISSN:0956-7968

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 March 1999

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ballenghien BWolff B(2024)A Theory of Proc-Omata—and Proof Methods for Process ArchitecturesTheoretical Aspects of Computing – ICTAC 202410.1007/978-3-031-77019-7_16(272-289)Online publication date: 25-Nov-2024
https://dl.acm.org/doi/10.1007/978-3-031-77019-7_16
Kanabar HVivien SAbrahamsson OMyreen MNorrish MPohjola JZanetti R(2023)PureCake: A Verified Compiler for a Lazy Functional LanguageProceedings of the ACM on Programming Languages10.1145/35912597:PLDI(952-976)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591259
Kună?Ar OPopescu A(2019)A Consistent Foundation for Isabelle/HOLJournal of Automated Reasoning10.1007/s10817-018-9454-862:4(531-555)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s10817-018-9454-8
Spector-Zabusky ABreitner JRizkallah CWeirich SAndronick JFelty A(2018)Total Haskell is reasonable CoqProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167092(14-27)Online publication date: 8-Jan-2018
https://dl.acm.org/doi/10.1145/3167092
Huffman B(2012)Formal verification of monad transformersACM SIGPLAN Notices10.1145/2398856.236453247:9(15-16)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364532
Huffman BThiemann PFindler R(2012)Formal verification of monad transformersProceedings of the 17th ACM SIGPLAN international conference on Functional programming10.1145/2364527.2364532(15-16)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2364527.2364532
Danielsson NAltenkirch T(2010)Subtyping, declarativelyProceedings of the 10th international conference on Mathematics of program construction10.5555/1886619.1886629(100-118)Online publication date: 21-Jun-2010
https://dl.acm.org/doi/10.5555/1886619.1886629
Hobor ADockins RAppel A(2010)A theory of indirection via approximationACM SIGPLAN Notices10.1145/1707801.170632245:1(171-184)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1707801.1706322
Hobor ADockins RAppel AHermenegildo MPalsberg J(2010)A theory of indirection via approximationProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1706299.1706322(171-184)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1706299.1706322
Bertot YKomendantsky VAntoy SAlbert E(2008)Fixed point semantics and partial recursion in CoqProceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming10.1145/1389449.1389461(89-96)Online publication date: 15-Jul-2008
https://dl.acm.org/doi/10.1145/1389449.1389461
Show More Cited By

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents