Hostname: page-component-745bb68f8f-hvd4g Total loading time: 0 Render date: 2025-01-26T04:02:11.281Z Has data issue: false hasContentIssue false
  • English
  • Français

HOLCF = HOL + LCF

Published online by Cambridge University Press:  01 March 1999

OLAF MÜLLER ,
TOBIAS NIPKOW ,
DAVID VON OHEIMB  and
OSCAR SLOTOSCH
OLAF MÜLLER
Affiliation:
Institut für Informatik, Technische Universität München, D-80290 München, Germany
TOBIAS NIPKOW
Affiliation:
Institut für Informatik, Technische Universität München, D-80290 München, Germany
DAVID VON OHEIMB
Affiliation:
Institut für Informatik, Technische Universität München, D-80290 München, Germany
OSCAR SLOTOSCH
Affiliation:
Institut für Informatik, Technische Universität München, D-80290 München, Germany
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Information
Journal of Functional Programming , Volume 9 , Issue 2 , March 1999 , pp. 191 - 223
Copyright
© 1999 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.