A functional logic for higher level reasoning about computation

DOI10.1007/BF01211079MaRDI QIDQ1318281zbMATH OpenOpenAlexFDO

Authors John Staples, Peter J. Robinson, Daniel Hazel

Publication date 1 December 1994

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01211079

zbMATH Keywords

category theoryfunctional logicmodal logicprogram specificationreasoning about computationsemanticsset theorysyntax

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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).

Recommendations

• The completeness of functional logic
• scientific article; zbMATH DE number 1670754
• scientific article; zbMATH DE number 4200180
• scientific article; zbMATH DE number 4043306
• Logical Reasoning for Higher-Order Functions with Local State

Cites work

• A new method for determining linear precedence functions for precedence grammars
• Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
• scientific article; zbMATH DE number 3900125 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 42734 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 4114587 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)

Cited in

(19)

• Adapting functional programs to higher order logic
• The completeness of functional logic
• Automatizing parametric reasoning on distributed concurrent systems
• A first order logic of effects
• scientific article; zbMATH DE number 1670754 (Why is no real title available?)
• scientific article; zbMATH DE number 2185697 (Why is no real title available?)
• scientific article; zbMATH DE number 5007864 (Why is no real title available?)
• Descriptive and Relative Completeness of Logics for Higher-Order Functions
• scientific article; zbMATH DE number 4049001 (Why is no real title available?)
• scientific article; zbMATH DE number 77950 (Why is no real title available?)
• Semantic formalization of interactive reasoning functionality
• Axiomatization of a functional logic language
• Separating functional computation from relations
• Painless programming combining reduction and search, design principles for embedding decision procedures in high-level languages
• Computer Science Logic
• Programming Languages and Systems
• A Virtual Machine for Functional Logic Computations
• A logic for Miranda
• Comparing integrated and external logics of functional programs

Describes a project that uses

Uses Software

• Lucid
• Qu-Prolog

This page was built for publication: A functional logic for higher level reasoning about computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1318281)