×

zbMATH — the first resource for mathematics

A functional logic for higher level reasoning about computation. (English) Zbl 0801.03023
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).

MSC:
03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Lucid; Qu-Prolog
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bowen, K. A.:Model Theory for Modal Logic. D. Reidel, 1979.
[2] Boyer, R. S. and Moore, J. S.:A Computational Logic. Academic Press, 1979. · Zbl 0448.68020
[3] Dijkstra, E. W.:A Discipline of Programming. Prentice-Hall, 1976. · Zbl 0368.68005
[4] Floyd, R. W.: Assigning Meanings to Programs. In:Proc. Symp. in Applied Mathematics 19, Mathematical Aspects of Computer Science J. T. Schwartz (ed.), pp. 19-32, American Math. Soc., 1967. · Zbl 0189.50204
[5] Frege, G.:Begriffsschrift, 1879. Translated in:From Frege to Godel, J. van Heijenoort (ed.), pp. 1-82, Harvard University Press, 1967.
[6] Gordon, M. J. C.: A Proof Generating System for Higher-Order Logic. University of Cambridge Computer Laboratory Tech. Report No. 103, January 1987.
[7] Gordon, M. J. C.: Mechanising Programming Logics in Higher Order Logic. In: Proceedings of the Hardware Verification Workshop, Banff, June 1988.
[8] Henman, P. and Staples, J.: Introduction to Functional Set Theory. University of Queensland Dept. of Computer Science Tech. Report No. 144, February 1990; revised March 1992.
[9] Henman, P., Hazel, D. and Staples, J.: Modelling Programming Concepts in Functional Set Theory: an Outline. Software Verification Research Centre, University of Queensland Dept. of Computer Science Tech. Report No. 91-8, October 1991.
[10] Hoare, C. A. R.: An Axiomatic Basis for Computer Programming.Communications ACM,12, 567-580 (1969). · Zbl 0179.23106 · doi:10.1145/363235.363255
[11] Mendelson, E.:Introduction to Mathematical Logic, 3rd Edn. Wadsworth and Brooks/Cole, Monterey, California, 1987. · Zbl 0681.03001
[12] Paterson, R. A. and Hazel, D.: Qu-Prolog 3.0 Reference Manual. University of Queensland Dept. of Computer Science Techn. Report No. 195, December 1990.
[13] Pratt, V. R.: Dynamic Logic. In:Foundations of Computer Science III, Part 2, J. W. de Bakker and J. van Leeuwen (eds) pp. 53-82, Mathematical Centre Tracts 109, Mathematisch Centrum, 1979.
[14] Robinson, P. J. and Staples, J.: Formalising a Hierarchical Structure of Practical Mathematical Reasoning. To appear,Logic and Computation. · Zbl 0779.68078
[15] Saaltink, M.: The Mathematics of m-Verdi, Eves Project Technical Report TR-87-5420-03, I.P. Sharp Associates Ltd, 1987.
[16] Shoenfield, J. R.: Axioms of Set Theory. In:Handbook of Mathematical Logic, J. Barwise (ed.), North-Holland, 1977.
[17] Staples, J. and Robinson, P. J.: Functional Logic for Program Verification: Introductory Lectures. University of Queensland Dept. of Computer Science Tech. Report No. 168, revised February 1991.
[18] Staples, J., Abbas, A. and Liu, C.: A Functional Logic Model for the Verification of Real-Time Software. University of Queensland Dept. of Computer Science Tech. Report No. 197, December 1990.
[19] Staples, J., Davison, P., Henman, P., Robinson, P. J. & Paterson, R. A.: Towards a Unified Verification Architecture.Australian Computer Science Communications,11, 120-129 (1989).
[20] Staples, J., Robinson, P. J. and Ellis, G. R.: Persistent Variables in Qu-Prolog.Australian Computer Science Communications,13, 362-369 (1990).
[21] Staples, J., Robinson, P. J., Paterson, R. A., Hagen, R. A., Craddock, A. J. and Wallis, P. C.: Qu-Prolog ? an Extended Prolog for Meta Level Programming. In:Proceedings, Workshop on Meta-Programming in Logic Programming, J. W. Lloyd (ed.), University of Bristol, June 1988, pp. 319-322.
[22] Tang, T. G., Robinson, P. J. and Staples, J.: The Demonstration Proof Editor Demo2, University of Queensland Dept. of Computer Science Tech. Report No. 175, December 1990.
[23] van Benthem, J.:A Manual of Intensional Logic. CSLI, Stanford, 1988. · Zbl 0678.03010
[24] Wadge, W. W. and Ashcroft, E. A.:Lucid, the Dataflow Programming Language. Academic Press, 1985. · Zbl 0564.68002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.