HOLCF: Higher Order Logic of Computable Functions

This paper presents a survey of HOLCF, a higher order logic of computable functions. The logic HOLCF is based on HOLC, a variant of the well known higher order logic HOL, which o ers the additional concept of type classes. HOLCF extends HOLC with concepts of domain theory such as complete partial orders, continuous functions and a xed point operator. With the help of type classes the extension can be formulated in a way such that the logic LCF constitutes a proper sublanguage of HOLCF. Therefore techniques from higher order logic and LCF can be combined in a fruitful manner avoiding drawbacks of both logics. The development of HOLCF was entirely conducted within the Isabelle system.

• Type: Conference
• Year: 1995
• Where: TPHOL
• Authors: Franz Regensburger
• Keywords: Automated Reasoning, Logic Holcf, Order Logic Hol, TPHOL 1995, Type Classes