From process logic to program logic

ABSTRACT

We present a process logic for the p -calculus with the linear/affine type discipline [6, 7, 31, 32, 33, 59, 60]. Built on the preceding studies on logics for programs and processes, simple systems of assertions are developed, capturing the classes of behaviours ranging from purely functional interactions to those with destructive update, local state and genericity. A central feature of the logic is representation of the behaviour of an environment as the dual of that of a process in an assertion, which is crucial for obtaining compositional proof systems. From the process logic we can derive compositional program logics for various higher-order programming languages, whose soundness is proved via their embeddings into the process logic. In this paper, the key technical framework of the process logic and its applications is presented focussing on pure functional behaviour and a prototypical call-by-value functional language, leaving the full technical development to [27, 26].

REFERENCES

• 1: M. Abadi , L. Cardelli , P.-L. Curien, Formal parametric polymorphism, Theoretical Computer Science, v.121 n.1-2, p.9-58, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90082-5 ]
• 2: Martín Abadi , K. Rustan M. Leino, A Logic of Object-Oriented Programs, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.682-696, April 14-18, 1997
• 3: Samson Abramsky , Radha Jagadeesan , Pasquale Malacaria, Full abstraction for PCF, Information and Computation, v.163 n.2, p.409-470, Dec 2000 [doi>10.1006/inco.2000.2930 ]
• 4: Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981 [doi>10.1145/357146.357150]
• 5: J. C. M. Baeten , W. P. Weijland, Process algebra, Cambridge University Press, New York, NY, 1991
• 6: Berger, M., Honda, K. and Yoshida, N., Sequentiality and the π-Calculus, TLCA01, LNCS 2044, 29--45, 2001.
• 7: Berger, M., Honda, K. and Yoshida, N., Genericity and the π-Calculus, FoSSaCs'03, LNCS 2620, 103--119, 2003.
• 8: Boudol, G., Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992.
• 9: Luís Caires , Luca Cardelli, A spatial logic for concurrency (part I), Information and Computation, v.186 n.2, p.194-235, 01 November 2003 [doi>10.1016/S0890-5401(03)00137-8]
• 10: Clint, M. and Hoare C.A.R. Program proving: jumps and functions. Acta Inf. 1:214--224, 1971.
• 11: Patrick Coust, Methods and logics for proving programs, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 12: Curry, B. and Feys, R. Combinatory Logic. North-Holland, 1958.
• 13: Mads Dam, Proof systems for π-calculus logics, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
• 14: Gordon, M., Milner, A. and Wadsworth, C., Edinburgh LCF, LNCS 78, 1979.
• 15: Carl A. Gunter, Semantics of programming languages: structures and techniques, MIT Press, Cambridge, MA, 1992
• 16: Floyd, W. Assigning meaning to programs. Prc. Symp. in Applied Mathematics. 19:19--32, 1967.
• 17: Francez N. and Pnueli, A. A proof method for cyclic programs. Acta Inf. 9, pp.133--157, 1978.
• 18: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 19: Harel, D. Proving the correctness of regular deterministic programs. TCS, 12:61--81, 1980.
• 20: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• 21: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 22: Hoare, C.A.R. Procedures and Parameters: an axiomatic approach. Lecture Notes in Mathematics 188, 102--116, Semantics of Algorithmic Languages, Springer, 1971.
• 23: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 24: Hoare, C.A.R. and Wirth, N., An axiomatic definition of the programming language PASCAL. Acta Inf. 2:335--355, 1973.
• 25: Kohei Honda, Composing processes, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.344-357, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237802]
• 26: Honda, K. Sequential Process Logics: Soundness Proofs. Typescript, 50pp. November 2003/January 2004. Available at: www.dcs.qmul.ac.uk/~kohei/logics.
• 27: Honda, K. Process Logic and Duality: Part (1) Sequential Processes. Typescript, 210pp. March 2004. Available at: www.dcs.qmul.ac.uk/~kohei/logics.
• 28: Kohei Honda , Nobuko Yoshida, A compositional logic for polymorphic higher-order functions, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.191-202, August 24-26, 2004, Verona, Italy [doi>10.1145/1013963.1013985]
• 29: Kohei Honda , Mario Tokoro, An Object Calculus for Asynchronous Communication, Proceedings of the European Conference on Object-Oriented Programming, p.133-147, July 15-19, 1991
• 30: Kohei Honda , Nobuko Yoshida, Game-theoretic analysis of call-by-value computation, Theoretical Computer Science, v.221 n.1-2, p.393-456, June 28, 1999 [doi>10.1016/S0304-3975(99)00039-0 ]
• 31: Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 16-18, 2002, Portland, Oregon
• 32: Kohei Honda , Nobuko Yoshida, Noninterference through flow analysis, Journal of Functional Programming, v.15 n.2, p.293-349, March 2005 [doi>10.1017/S0956796804005477]
• 33: Honda, K., Yoshida, N. and Berger, M., Control in the π -Calculus, Proc. CW'04, ACM, 2004.
• 34: J. M. E. Hyland , C.-H. L. Ong, On full abstraction for PCF: I, II, and III, Information and Computation, v.163 n.2, p.285-408, Dec 2000 [doi>10.1006/inco.2000.2917 ]
• 35: Bart Jacobs , Joachim van den Berg , Marieke Huisman , Martijn van Berkum , U. Hensel , H. Tews, Reasoning about Java classes: preliminary report, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.329-340, October 18-22, 1998, Vancouver, British Columbia, Canada
• 36: Jones, C.B. Specification and Design of (Parallel) Programs. Proc. IFIP 9th World Computer Congress. North Holland, 321--332, 1983.
• 37: Naoki Kobayashi , Benjamin C. Pierce , David N. Turner, Linearity and the pi-calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.5, p.914-947, Sept. 1999 [doi>10.1145/330249.330251]
• 38: Kowaltowsky, T. Axiomatic approach to side effects and general jumps. Acta Informatica 7, 357--360.
• 39: Olivier Laurent, Polarized Games, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.265, July 22-25, 2002
• 40: Gary T. Leavens , Albert L. Baker, Enhancing the Pre- and Postcondition Technique for More Expressive Specifications, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume II, p.1087-1106, September 20-24, 1999
• 41: Longley, J. and Plotkin, G. Logical Full Abstraction and PCF. Tbilisi Symposium on Logic, Language and Information. 333--352, Stanford, CSLI, 1998.
• 42: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987
• 43: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 44: Milner, R., Functions as Processes, MSCS. 2(2):119--141, 1992,
• 45: Milner, R., Speech by Robin Milner on receiving an Honorary Degree from the University of Bologna, ICALP'97, http://www.cs.unibo.it/icalp/Lauree milner.html.
• 46: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 47: Robin Milner , Joachim Parrow , David Walker, Modal logics for mobile processes, Theoretical Computer Science, v.114 n.1, p.149-171, June 14 1993
• 48: Milner, R., Polyadic π -Calculus: a tutorial. Proceedings of the International Summer School on Logic Algebra of Specification, Marktoberdorf, 1992.
• 49: Naur, P. Proof of algorithms by general snapshots. BIT 6, 310--316, 1966.
• 50: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 51: Oheimb, D.V., Hoare Logic for Java in Isabelle/HOL. Concurrency: Practice and Experience. John Wiley, 2002.
• 52: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 53: Pierce, B.C. and Sangiorgi. D, Typing and subtyping for mobile processes. MSCS, 6(5):409--454, 1996.
• 54: Gordon D. Plotkin , Martín Abadi, A Logic for Parametric Polymorphism, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.361-375, March 16-18, 1993
• 55: Arnd Poetzsch-Heffter , Peter Müller, A Programming Logic for Sequential Java, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.162-176, March 22-28, 1999
• 56: Reynolds, J. Intuitionistic Reasoning about Shared Mutable Data Structure, Millennial Perspectives in Computer Science, Oxford, 1999.
• 57: Davide Sangiorgi, &pgr;-calculus, internal mobility, and agent-passing calculi, Theoretical Computer Science, v.167 n.1-2, p.235-274, Oct. 30, 1996
• 58: David Walker, Objects in the &pgr;-calculus, Information and Computation, v.116 n.2, p.253-271, Feb. 1, 1995 [doi>10.1006/inco.1995.1018 ]
• 59: Nobuko Yoshida , Martin Berger , Kohei Honda, Strong normalisation in the π-calculus, Information and Computation, v.191 n.2, p.145-202, 15 June 2004 [doi>10.1016/j.ic.2003.08.004]
• 60: Nobuko Yoshida , Kohei Honda , Martin Berger, Linearity and Bisimulation, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.417-434, April 08-12, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques; Logics of programs; Assertions
      F.3.2 Semantics of Programming Languages
          Subjects: Process models

General Terms:
Languages, Theory, Verification

Keywords:
π-calculus, duality, higher-order functions, hoare logic, mobile processes, types