HOLCF = HOL + LCF
From MaRDI portal
Publication:4267723
DOI10.1017/S095679689900341XzbMath0933.03028OpenAlexW2113426200MaRDI QIDQ4267723
David von Oheimb, Tobias Nipkow, Oscar Slotosch, Olaf Mueller
Publication date: 29 November 1999
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s095679689900341x
denotational semanticsconcurrencyfunctional programmingdomain theoryIsabelleChurch's Higher-Order LogicHOLCFScott's Logic for Computable Functions
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)
Related Items
Some Domain Theory and Denotational Semantics in Coq, A Purely Definitional Universal Domain, A Consistent Foundation for Isabelle/HOL, Representing model theory in a type-theoretical logical framework, The Isabelle Framework, Imperative Functional Programming with Isabelle/HOL, A consistent foundation for Isabelle/HOL, Short note: Strict unwraps make worker/wrapper fusion totally correct, Higher-Order Separation Logic in Isabelle/HOLCF, Partiality and recursion in interactive theorem provers – an overview, Adapting functional programs to higher order logic, An extensible encoding of object-oriented data models in HOL. With an application to IMP++
Uses Software
