Mason, Ian A. A first order logic of effects. (English) Zbl 0901.68182 Theor. Comput. Sci. 185, No. 2, 277-318 (1997). Summary: We describe some of our progress towards an operational implementation of a modern programming logic. The logic is inspired by the variable type systems of Feferman, and is designed for reasoning about imperative functional programs. The logic goes well beyond traditional programming logics, such as Hoare’s logic and dynamic logic in its expressibility, yet is less problematic to encode into higher order logics. The main focus of the paper is to present an axiomatization of the base first order theory. Cited in 2 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B70 Logic in computer science Keywords:formal methods; \(\lambda\)-calculus; contexts; operational semantics; theorem proving; programming logic Software:Isabelle PDFBibTeX XMLCite \textit{I. A. Mason}, Theor. Comput. Sci. 185, No. 2, 277--318 (1997; Zbl 0901.68182) Full Text: DOI References: [1] Abelson, H.; Sussman, G. J., Structure and Interpretation of Computer Programs (1985), MIT Press, McGraw-Hill: MIT Press, McGraw-Hill New York [2] Abramsky, S., The lazy lambda calculus, (Turner, D. A., Research Topics in Functional Programming (1990), Addison-Wesley: Addison-Wesley Reading, MA) · Zbl 0779.03003 [3] Abramsky, S., Domain theory in logical form, Ann. Pure Appl. Logic, 51, 1, 1-77 (1991) · Zbl 0737.03006 [4] Agha, G.; Mason, I. A.; Smith, S. F.; Talcott, C. L., Towards a theory of actor computation, (The 3rd Internat. Conf. Concurrency Theory (CONCUR ’92). The 3rd Internat. Conf. Concurrency Theory (CONCUR ’92), Lecture Notes in Computer Science, vol. 630 (1992), Springer: Springer Berlin), 565-579 [5] Agha, G.; Mason, I. A.; Smith, S. F.; Talcott, C. L., A foundation for actor computation, J. Functional Programming, XX, 1-72 (1997) · Zbl 0870.68091 [6] Apt, K. R., Ten years of Hoare’s logic: a survey — part I, ACM Trans. Programming Languages Systems, 4, 431-483 (1981) · Zbl 0471.68006 [7] Avron, A.; Honsell, F.; Mason, I. A.; Pollack, R., Using typed lambda calculus to implement formal systems on a machine, J. Autom. Reasoning, 9, 309-354 (1992) · Zbl 0784.68072 [8] Barendregt, H., The Lambda Calculus: its Syntax and Semantics (1981), North-Holland: North-Holland Amsterdam · Zbl 0467.03010 [9] Bloom, B., Can LCF be topped?, Inform. Comput., 87, 264-301 (1990) · Zbl 0825.68447 [10] Chang, C. C.; Keisler, H. J., Model Theory (1973), North-Holland: North-Holland Amsterdam · Zbl 0276.02032 [11] Egidi, L.; Honsell, F.; Ronchi della Rocca, S., Operational, denotational and logical descriptions: a case study, Fund. Inform., 16, 2, 149-170 (1992) · Zbl 0762.68042 [12] Feferman, S., A language and axioms for explicit mathematics, (Algebra and Logic, Lecture Notes in Mathematics, vol. 450 (1975), Springer: Springer Berlin), 87-139 [13] Feferman, S., Constructive theories of functions and classes, (Logic Colloquium ’78, North-Holland (1979)), 159-224, Amsterdam [14] Feferman, S., A theory of variable types, Rev. Colomb. Matématicas, 19, 95-105 (1985) · Zbl 0615.03045 [15] Feferman, S., Polymorphic typed lambda-calculi in a type-free axiomatic framework, (Logic and Computation, Contemporary Mathematics, vol. 106 (1990), AMS: AMS Providence, RI), 101-136 · Zbl 0701.03007 [16] Felleisen, M., The calculi of lambda-v-cs conversion: A syntactic theory of control and state in imperative higher-order programming languages, (PhD thesis (1987), Indiana University) [18] Felleisen, M.; Friedman, D. P., Control operators, the SECD-machine, and the λ-calculus, (Wirsing, M., Formal Description of Programming Concepts III (1986), North-Holland: North-Holland Amsterdam), 193-217 [19] Felleisen, M.; Hieb, R., The revised report on the syntactic theories of sequential control and state, Theoret. Comput. Sci., 103, 235-271 (1992) · Zbl 0764.68094 [21] Frost, J., Effective programming, (PhD thesis (1996), Technical University of Denmark), also published as Technical Report IT-TR 1996-001. [22] Frost, J.; Mason, I. A., An operational logic of effects, (Proc. Australasian Theory Symp., CATS ’96 (1996)), 147-156 [23] Harel, D., Dynamic logic, (Gabbay, D.; Guenthner, G., Handbook of Philosophical Logic, vol. II (1984), D. Reidel: D. Reidel Dordrecht), 497-604 · Zbl 0875.03076 [24] Honsell, F.; Mason, I. A.; Smith, S. F.; Talcott, C. L., A theory of classes for a functional language with effects, (Proc. CSL92. Proc. CSL92, Lecture Notes in Computer Science, vol. 702 (1993), Springer: Springer Berlin), 309-326 · Zbl 0835.68013 [25] Honsell, F.; Mason, I. A.; Smith, S. F.; Talcott, C. L., A variable typed logic of effects, Inform. Comput., 119, 1, 55-90 (1995) · Zbl 0832.68009 [26] Howe, D., Equality in the lazy lambda calculus, (4th Annual Symp. on Logic in Computer Science, IEEE (1989)) [27] Jim, T.; Meyer, A. R., Full abstraction and the context lemma, (Theoretical Aspects of Computer Science. Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, vol. 526 (1991), Springer: Springer Berlin), 131-151 · Zbl 1493.68090 [28] Kleene, S. C., Introduction to Metamathematics (1952), North-Holland: North-Holland Amsterdam · Zbl 0047.00703 [29] Landin, P. J., The mechanical evaluation of expressions, Comput. J., 6, 308-320 (1964) · Zbl 0122.36106 [30] Mason, I. A., The Semantics of Destructive Lisp, (PhD thesis (1986), Stanford University), Also available as CSLI Lecture Notes No. 5, Center for the Study of Language and Information, Stanford University. · Zbl 0678.68003 [31] Mason, I. A., Parametric computation, (Harland, J., Australasian Theory Symp. CATS ’97. Australasian Theory Symp. CATS ’97, Australian Computer Science Communications, Vol. 19 (1997)), 103-112, No. 2 [32] Mason, I. A.; Talcott, C. L., Axiomatizing operational equivalence in the presence of side effects, (4th Annual Symp. on Logic in Computer Science, IEEE (1989)) · Zbl 0722.03027 [33] Mason, I. A.; Talcott, C. L., A sound and complete axiomatization of operational equivalence between programs with memory, (Technical Report STAN-CS-89-1250 (1989), Department of Computer Science, Stanford University) [34] Mason, I. A.; Talcott, C. L., Reasoning about programs with effects, (Programming Language Implementation and Logic Programming, PLILP’90. Programming Language Implementation and Logic Programming, PLILP’90, Lecture Notes in Computer Science, vol. 456 (1990), Springer: Springer Berlin), 189-203 [35] Mason, I. A.; Talcott, C. L., Equivalence in functional languages with effects, J. Functional Programming, 1, 287-327 (1991) · Zbl 0941.68540 [36] Mason, I. A.; Talcott, C. L., Inferring the equivalence of functional programs that mutate data, Theoret. Comput. Sci., 105, 2, 167-215 (1992) · Zbl 0768.68092 [37] Mason, I. A.; Talcott, C. L., References, local variables and operational reasoning, (7th Annual Symp. on Logic in Computer Science, IEEE (1992)), 186-197 [38] Mason, I. A.; Talcott, C. L., Program transformation via contextual assertions, (Logic, Language and Computation, Festschrift in Honor of Satoru Takasu. Logic, Language and Computation, Festschrift in Honor of Satoru Takasu, Lecture Notes in Computer Science, vol. 792 (1994), Springer: Springer Berlin), 225-254 [39] Mason, I. A., Hoare’s logic in the LF, (Technical Report ECS-LFCS-87-32 (1987), Laboratory for foundations of computer science, University of Edinburgh) [40] Mason, I. A.; Talcott, C. L., Reasoning about object systems in VTLoE, Internat. J. Foundations Comput. Sci., 6, 3, 265-298 (1995) · Zbl 0830.68021 [41] Milner, R., Fully abstract models of typed λ-calculi, Theoret. Comput. Sci., 4, 1-22 (1977) · Zbl 0386.03006 [42] Moggi, E., Computational lambda-calculus and monads, (4th Annual Symp. on Logic in Computer Science, IEEE (1989)) · Zbl 0716.03007 [43] Moggi, E., Notions of computation and monads, Information and Comput., 93, 1 (1991) · Zbl 0723.68073 [44] Morris, J. H., Lambda calculus models of programming languages, (PhD thesis (1968), Massachusetts Institute of Technology) [45] Nelson, C. G.; Oppen, D. C., Fast decision procedures based on congruence closure, (Technical Report STAN-CS-77-647 (1977), Department of Computer Science, Stanford University) · Zbl 0441.68111 [46] Ong, C-H. L., The lazy lambda calculus: an investigation into the foundations of functional programming, (PhD thesis (1988), Imperial College, University of London) [47] Paulson, L. C., Isabelle, a generic theorem prover, (Lecture Notes in Computer Science, vol. 828 (1994), Springer: Springer Berlin) · Zbl 0825.68059 [48] Pitts, A. M., Evaluation logic, (IVth Higher-Order Workshop, Banff, vol. 283 of Workshops in Computing (1990), Springer: Springer Berlin) · Zbl 0521.03051 [49] Pitts, A. M.; Stark, I., On the observable properties of higher order functions that dynamically create local names, (ACM Sigplan Workshop on State in Programming Languages. ACM Sigplan Workshop on State in Programming Languages, YaleU/DCS/RR-968 (1993)) [50] Plotkin, G., Call-by-name, call-by-value and the lambda calculus, Theoret. Comput. Sci., 1, 125-159 (1975) · Zbl 0325.68006 [51] Prawitz, D., Natural Deduction: A Proof-theoretical Study (1965), Almquist and Wiksell · Zbl 0173.00205 [52] Rabin, M. O., Decidability of second order theories and automata on infinite trees, Trans. Amer. Math. Soc., 141, 1-35 (1969) · Zbl 0221.02031 [53] Reynolds, J. C., Idealized ALGOL and its specification logic, (Néel, D., Tools and Notions for Program Construction (1982), Cambridge University Press: Cambridge University Press Cambridge), 121-161 [54] Smith, S. F., From operational to denotational semantics, (MFPS 1991. MFPS 1991, Lecture Notes in Computer Science, vol. 598 (1992), Springer: Springer Berlin), 54-76 [55] Talcott, C. L., The essence of rum: a theory of the intensional and extensional aspects of Lisp-type computation, (PhD thesis (1985), Stanford University) [56] Talcott, C. L., Binding structures, (Lifschitz, V., Artificial Intelligence and Mathematical Theory of Computation (1991), Academic Press: Academic Press New York) · Zbl 0755.68083 [57] Talcott, C. L., A theory for program and data type specification, Theoret. Comput. Sci., 104, 129-159 (1992) · Zbl 0759.68061 [58] Talcott, C. L., A theory of binding structures and its applications to rewriting, Theoret. Comput. Sci., 112, 99-143 (1993) · Zbl 0783.68089 [59] Talcott, C. L., Reasoning about functions with effects, (Gordon, A.; Pitts, A., Higher Order Operational Techniques in Semantics (1997)), to appear. · Zbl 0971.68024 [60] Tenney, R. L., Decidable pairing functions, (PhD thesis (1972), Cornell University), Also appears as Computer Science TR 72-136. [61] Weyhrauch, R. W., Prolegomena to a theory of formal reasoning, Artificial Intelligence, 13, 133-170 (1980) · Zbl 0435.68070 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.