Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-27T17:45:59.132Z Has data issue: false hasContentIssue false

Feferman-Landin Logic

from PART III - APPLICATIVE AND SELF-APPLICATIVE THEORIES

Published online by Cambridge University Press:  31 March 2017

By
Ian A. Mason  and
Carolyn L. Talcott
Edited by
Wilfried Sieg ,
Richard Sommer  and
Carolyn Talcott
Wilfried Sieg
Affiliation:
Carnegie Mellon University, Pennsylvania
Richard Sommer
Affiliation:
Stanford University, California
Carolyn Talcott
Affiliation:
Stanford University, California
Get access

Summary

Abstract This paper presents a logic based on Feferman's Variable Type Theories for reasoning about programs written in a class of imperative functional languages called Landinesque languages.

To Solomon Feferman on the occasion of his 70th Birthday with much gratitude.

Historical background Feferman-Landin Logic is so named because of the influence that the work of both Feferman and Landin has had on our work. Of particular relevance are two key ideas:

Landin's idea: a programming language can be thought of as the lambda calculus augmented by operations on the basic data, as well as computational environment. We call such languages Landinesque languages.

Feferman's idea: to formalize constructive mathematics in 2-sorted classical theories called variable type theories. In these theories both functions and data are objects of discourse in a first order setting, as are collections of such things.

Both authors were PhD students of Solomon Feferman in the early 1980's where, under his influence,we began the research programleading to thework that this paper will report on. Both the theories used by Feferman, and his approach to formalizing constructive mathematics seemed very natural and we felt that this approach should also work for developing formal systems for reasoning about programs.

The first step in such an endeavor is to develop the mathematical semantics of the programs of interest. Our focus has been on reasoning about non-functional primitives. Together we have studied lambda calculus augmented by operations formanipulating control [39], manipulating memory [29], and for communicating asynchronously in an open distributed environment [2]. In each casewe developed an operational semantics based solely on syntactic entities,and studied the natural operational equivalence generated by that semantics (operational equivalence meaning being equi-defined in all closing contexts). Crucial in such work is the ability to simplify the criteria for operational equivalence to some form of context lemma a la Robin Milner [31] to avoid the complexity of reasoning about arbitrary program contexts. In both the case of memory, and control, we have established such simplifications now known in the literature as CIU theorems (Closed Instantiations of Uses). The case for communicating asynchronously in an open distributed environment remains open.

Type
Chapter
Information
Reflections on the Foundations of Mathematics
Essays in Honor of Solomon Feferman
 , pp. 293 - 328
Publisher: Cambridge University Press
Print publication year: 2002

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1] H., Abelson and G. J., Sussman, Structure and interpretation of computer programs, TheMIT Press, McGraw-Hill Book Company, 1985.
[2] G., Agha, I. A., Mason, S. F., Smith, and C. L., Talcott, A foundation for actor computation, Journal of Functional Programming, vol. 7 (1997), pp. 1-72.Google Scholar
[3] K.R., Apt, Ten years of Hoare's logic: A survey-part I, ACM Transactions on Programming Languages and Systems, vol. 4 (1981), pp. 431-483.Google Scholar
[4] C.C., Chang and H.J., Keisler, Model theory, North-Holland, Amsterdam, 1973.
[5] S., Feferman, A language and axioms for explicit mathematics, Algebra and logic, Springer Lecture Ntes inMathematics, vol. 450, Springer Verlag, 1975, pp. 87-139.
[6] S., Feferman, Non-extensional type-free theories of partial operations and classifications, i., Proof theory symposium, kiel 1974 (J., Diller and G. H., Müller, editors), Lecture notes in mathematics, no. 500, Springer, Berlin, 1975, pp. 73-118.
[7] S., Feferman, Constructive theories of functions and classes, Logic colloquium –78, North-Holland, 1979, pp. 159-224.
[8] S., Feferman, A theory of variable types, Revista Colombiana deMatématicas, vol. 19 (1985), pp. 95- 105.Google Scholar
[9] S., Feferman, Polymorphic typed lambda-calculi in a type-free axiomatic framework, Logic and computation, Contemporary Mathematics, vol. 106, A.M.S., Providence R. I., 1990, pp. 101-136.
[10] S., Feferman, Logics for termination and correctness of functional programs,, Logic from computer science, MSRI Publications, vol. 21, Springer Verlag, 1992, pp. 101-136.
[11] S., Feferman, Logics for termination and correctness of functional programs, II. logics of strength PRA., Proof theory, Cambridge University Press, 1992.
[12] M., Felleisen,, 1993, Personal communication.
[13] M., Felleisen and D.P., Friedman, Control operators, the SECD-machine, and the _-calculus, Formal description of programming concepts III (M., Wirsing, editor), North-Holland, 1986, pp. 193- 217.
[14] M., Felleisen and A., Sabry, Continuations in programming practice: Introduction and survey, 1999, available at http://www.cs.uoregon.edu/∼sabry/papers/continuations.ps.
[15] J., Ford and I. A., Mason, Establishing a General Context Lemma in PVS, 2nd Australasian Workshop on Computational Logic, AWCL–01, 2001, available at http://mcs.une.edu.au/∼pvs/.
[16] D. P., Friedman, Applications of continuations, Technical Report 237, Indiana Univeristy Computer Science Department, 1988, Tutorial given at POPL88.
[17] J., Frost, Effective programming, Ph.D. thesis, Technical University of Denmark, 1996, also published as Techincal Report IT-TR 1996-001.
[18] J., Frost and I. A., Mason, An Operational Logic of Effects, Proceedings of the Australasian Theory Symposium, CATS –96, 1996, pp. 147-156.
[19] M. J. C., Gordon, Operational reasoning and denotational semantics, Technical Report SAIL Memo AIM-264, Artificial Intelligence Laboratory, Stanford University, 1975.
[20] J., Gosling, B., Joy, and G. L., Steele Jr., The Java language specification, Addison-Wesley, 1996.
[21] D., Harel, Dynamic logic, Handbook of philosophical logic, vol. ii (D., Gabbay and G., Guenthner, editors), D., Reidel, 1984, pp. 497-604.Google Scholar
[22] F., Honsell, I. A., Mason, S. F., Smith, and C. L., Talcott, A Variable Typed Logic of Effects, Information and Computation, vol. 119 (1995), no. 1, pp. 55-90.Google Scholar
[23] D., Howe, Equality in the lazy lambda calculus, Fourth annual symposium on logic in computer science, IEEE, 1989.
[24] D. J., Howe, Proving congruence of bisimulation in functional programming languages, Information and Computation, vol. 124 (1996), no. 2, pp. 103-112.Google Scholar
[25] P. J., Landin, The mechanical evaluation of expressions, Computer Journal, vol. 6 (1964), pp. 308-320.Google Scholar
[26] I. A., Mason, A First Order Logic of Effects, Theoretical Computer Science, vol. 185 (1997), pp. 277 - 318.Google Scholar
[27] I. A., Mason, Computing with contexts, Higher-Order and Symbolic Computation, vol. 12 (1999), pp. 171-201.Google Scholar
[28] I. A., Mason, S. F., Smith, and C. L., Talcott, From Operational Semantics to Domain Theory, Information and Computation, vol. 128 (1996), no. 1, pp. 26-47.Google Scholar
[29] I. A., Mason and C. L., Talcott, Equivalence in functional languages with effects, Journal of Functional Programming, vol. 1 (1991), pp. 287-327.Google Scholar
[30] I. A., Mason and C. L., Talcott, Reasoning about object systems in VTLoE, International Journal of Foundations of Computer Science, vol. 6 (1995), no. 3, pp. 265-298.Google Scholar
[31] R., Milner, Fully abstract models of typed _-calculi, Theoretical Computer Science, vol. 4 (1977), pp. 1-22.Google Scholar
[32] R., Milner, M., Tofte, and R., Harper, The definition of standard ML, MIT Press, 1990.
[33] E., Moggi, Computational lambda-calculus and monads, Fourth annual symposium on logic in computer science, IEEE, 1989.
[34] A. M., Pitts, Evaluation logic, Ivth higher-order workshop, banff, Workshops in Computing, vol. 283, Springer-Verlag, 1990.
[35] G., Plotkin, Call-by-name, call-by-value and the lambda calculus, Theoretical Computer Science, vol. 1 (1975), pp. 125-159.Google Scholar
[36] D., Prawitz, Natural deduction: A proof-theoretical study, Almquist and Wiksell, 1965.
[37] J.C., Reynolds, Idealized ALGOL and its specification logic, Tools and notions for program construction (D., Néel, editor), Cambridge University Press, 1982, pp. 121-161.
[38] G. L., Steele and G. J., Sussman, Scheme: An interpreter for extended lambda calculus, Higher- Order and Symbolic Computation, vol. 11 (1999), no. 4, pp. 405-439.Google Scholar
[39] C. L., Talcott, The essence of Rum: A theory of the intensional and extensional aspects of Lisp-type computation, Ph.D. thesis, Stanford University, 1985.
[40] C. L., Talcott, A theory for program and data type specification, Theoretical Computer Science, vol. 104 (1992), pp. 129-159.Google Scholar
[41] C. L., Talcott, A theory for program and data specification, Theoretical Computer Science, vol. 104 (1993), pp. 129-159.Google Scholar
[42] C. L., Talcott, Reasoning about functions with effects, Higher order operational techniques in semantics, Cambridge University Press, 1996.

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×