HOLCF: Higher order logic of computable functions
From MaRDI portal
Recommendations
- A functional logic for higher level reasoning about computation
- Higher-order separation logic in Isabelle/HOLCF
- HOL-: An intentional first-order expression of higher-order logic
- HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
- Descriptive and Relative Completeness of Logics for Higher-Order Functions
- Higher-order computational logic
- scientific article; zbMATH DE number 234014
- scientific article; zbMATH DE number 2110621
- An lCF-style interface between HOL and first-order logic
Cited in
(16)- HasCasl: integrated higher-order specification and program development
- On the formalization of gamma function in HOL
- The HASCASL prologue: Categorical syntax and semantics of the partial \(\lambda\)-calculus
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Some Domain Theory and Denotational Semantics in Coq
- The HOL-Omega Logic
- scientific article; zbMATH DE number 4160688 (Why is no real title available?)
- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
- Fixpoints and search in PVS
- Using Structural Recursion for Corecursion
- HOLCF = HOL + LCF
- Higher-order computational logic
- Stateless higher-order logic with quantified types
- Theorem Proving in Higher Order Logics
- Using lattice theory in higher order logic
- Winskel is (almost) right. Towards a mechanized semantics textbook
This page was built for publication: HOLCF: Higher order logic of computable functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3024884)
