Sciweavers

TPHOL
1995
IEEE

HOLCF: Higher Order Logic of Computable Functions

13 years 7 months ago
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.
Franz Regensburger
Added 26 Aug 2010
Updated 26 Aug 2010
Type Conference
Year 1995
Where TPHOL
Authors Franz Regensburger
Comments (0)