Proofs, tests and continuation passing style

ABSTRACT

The concept of syntactical duality is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the proof/test duality proposed by Girard in his 1999 paper on the meaning of logical rules. In detail, starting from the notion of “test” proposed by Girard, we develop a notion of test for intuitionistic logic and we give a complete deductive system whose computational interpretation is the target language of the call-by-value and call-by-name continuation passing style translations.

REFERENCES

• 1: Ariola, Z. M. and Herbelin, H. 2003. Minimal classical logic and control operators. In Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2719. Springer, Berlin, 871--885.
• 2: Franco Barbanera , Stefano Berardi, Extracting Constructive Content from Classical Logic via Control-like Reductions, Proceedings of the International Conference on Typed Lambda Calculi and Applications, p.45-59, March 16-18, 1993
• 3: Franco Barbanera , Stefano Berardi, A Symmetric Lambda Calculus for "Classical" Program Extraction, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.495-515, April 19-22, 1994
• 4: Pierre-Louis Curien , Hugo Herbelin, The duality of computation, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.233-243, September 2000
• 5: Danos, V., Joinet, J.-B., and Schellinx, H. 1995. LKT and LKQ: Sequent calculi for second order logic based upon dual linear decomposition of classical implication. In Advances in Linear Logic, J.-Y. Girard et al. Eds. Cambridge University Press, 43--59.
• 6: Danos, V., Joinet, J.-B., and Schellinx, H. 1997. A new deconstructive logic: Linear logic. J Symbolic Logic 62, 3, 755--807.
• 7: Danvy, O. 2004. On evaluation contexts, continuations, and the rest of the computation. In Proceedings of the 4th ACM SIGPLAN Continuations Workshop (CW'04), H. Thielecke, Ed. Tech. rep. CSR-040-1.
• 8: Philippe De Groote, An environment machine for the λμ-calculus, Mathematical Structures in Computer Science, v.8 n.6, p.637-669, December 1998 [doi>10.1017/S0960129598002667]
• 9: Felleisen, M., Friedman, D. P., Kohlbecker, E. E., and Duba, B. F. 1986. Reasoning with continuations. In Proceedings of the 1st Annual IEEE Sympoisum on Logic in Computer Science (LICS'86), A. Meyer, Ed. IEEE Computer Society Press, 131--141.
• 10: Michael J. Fischer, Lambda calculus schemata, Proceedings of ACM conference on Proving assertions about programs, p.104-109, January 06-07, 1972, Las Cruces, New Mexico, United States
• 11: Carsten Führmann , Hayo Thielecke, On the call-by-value CPS transform and its semantics, Information and Computation, v.188 n.2, p.241-283, 29 January 2004 [doi>10.1016/j.ic.2003.08.001]
• 12: Girard, J.-Y. 1999. On the meaning of logical rules I: Syntax vs. semantics. In Proceedings of the 1997 NATO Advanced Study Institute on Computational Logic, U. Berger and H. Schwichtenberg, Eds. NATO ASI Series, Computer and Systems Sciences, vol. 165. Springer, 215--272.
• 13: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 14: Herbelin, H. 1995. Séquents qu'on calcule. Thèse de Doctorat, Université Paris 7.
• 15: Martin Hofmann , Thomas Streicher, Continuation models are universal for lambda-mu-calculus, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.387, June 29-July 02, 1997
• 16: Ichiro Ogata, A Proof Theoretical Account of Continuation Passing Style, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.490-505, September 22-25, 2002
• 17: C.-H. L. Ong , C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.215-227, January 15-17, 1997, Paris, France [doi>10.1145/263699.263722]
• 18: Michel Parigot, Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction, Proceedings of the International Conference on Logic Programming and Automated Reasoning, p.190-201, July 15-20, 1992
• 19: Parigot, M. 1997. Proofs of strong normalisation for second order classical natural deduction. J. Symbolic Logic 62, 4, 1461--1479.
• 20: Plotkin, G. D. 1975. Call-by-Name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1, 2, 125--159.
• 21: Amr Sabry , Matthias Felleisen, Reasoning about programs in continuation-passing style, Lisp and Symbolic Computation, v.6 n.3-4, p.289-360, Nov. 1993 [doi>10.1007/BF01019462]
• 22: Peter Selinger, Control categories and duality: on the categorical semantics of the lambda-mu calculus, Mathematical Structures in Computer Science, v.11 n.2, p.207-260, April 2001 [doi>10.1017/S096012950000311X]
• 23: Th. Streicher , B. Reus, Classical logic, continuation semantics and abstract machines, Journal of Functional Programming, v.8 n.6, p.543-572, November 1998 [doi>10.1017/S0956796898003141]
• 24: Wadler, P. 2005. Call-by-Value is dual to call-by-name reloaded. In Term Rewriting and Applications. Lecture Notes in Computer Science, vol. 3467. Springer, Berlin, 185--203.
• 25: Zucker, J. 1974. The correspondence between cut-elimination and normalization, Part I & II. Ann. Math. Logic 7, 1--155.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Languages, Theory

Keywords:
Minimal logic, call-by-name, call-by-value, continuations passing style, intutionistic logic, lambda calculus, linear logic