A functional logic for higher level reasoning about computation (Q1318281)

This paper describes a syntax and semantics for ``functional logic'', which is a formal first-order logic with expressions that depend on an implicit parameter (such as a program state, time, a possible world) aimed at providing a high-level basis for reasoning about computation. The logic is able to bring together classical, Hoare (weakest preconditions) and modal logic, set theory and category theory in one logical framework. For instance, in the case of modal logic, it is possible to write down the semantic definition of the modal operators as an expression (axiom) in the object language. Furthermore, functional logic enables one to integrate (functional) assertions and procedural code. (A functional assertion denotes a Boolean-valued function rather than a single Boolean value).