HOLCF: Higher order logic of computable functions

Abstract

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 offers the additional concept of type classes. HOLCF extends HOLC with concepts of domain theory such as complete partial orders, continuous functions and a fixed 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.