Deriving a Floyd–Hoare logic for non-local jumps from a formulæ-as-types notion of control

Apt, 1981, Ten years of Hoare’s logic: a survey – part I, ACM Trans. Program. Lang. Syst., 3, 431, 10.1145/357146.357150 Audebaud, 1999, Deriving proof rules from continuation semantics, Formal Aspects Comput., 11, 426, 10.1007/s001650050041 F. Barbanera, S. Berardi, Extracting constructive content from classical logic via control-like reductions, in: LNCS, vol. 662, Springer-Verlag, 1994, pp. 47–59. Barnes, 2003 Benton, 1998, Computational types from a logical perspective, J. Funct. Programming, 8, 177, 10.1017/S0956796898002998 M. Berger, Program logics for sequential higher-order control, in: Proceedings of the Third IPM International Conference, FSEN 2009, Lecture Notes in Computer Science, vol. 5961, Springer, 2010, pp. 194–211. Berger, 2002, Refined program extraction from classical proofs, Ann. Pure Appl. Logic, 114, 3, 10.1016/S0168-0072(01)00073-2 U. Berger, H. Schwichtenberg, Program development by proof transformation, in: H. Schwichtenberg (Ed.), Proof and Computation, Series F: Computer and Systems Sciences, vol. 139, NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20–August 1, 1993, Springer-Verlag, 1995, pp. 1–45. U. Berger, H. Schwichtenberg, Program extraction from classical proofs, in: Daniel Leivant (Ed.), Logic and Computational Complexity, Lecture Notes in Computer Science, vol. 139, Springer, Berlin/ Heidelberg, 1995, pp. 77–97. Borgida, 2002, On the frame problem in procedure specifications, IEEE Trans. Softw. Engrg., 21, 785, 10.1109/32.469460 Clarke, 1979, Programming language constructs for which it is impossible to obtain good Hoare axioms, J. ACM, 26, 10.1145/322108.322121 Clint, 1973, Program proving: coroutines, Acta Inform., 2, 50, 10.1007/BF00571463 Clint, 1972, Program proving: jumps and functions, Acta Inform., 1, 214, 10.1007/BF00288686 Colson, 1998, System T, call-by-value and the minimum problem, Theor. Comput. Sci., 206, 301, 10.1016/S0304-3975(98)00011-5 Constable, 1986 T. Coquand, Computational content of classical logic, in: Semantics and Logics of Computation, Cambridge University Press, 1996, pp. 470–517. P. Cousot, Methods and logics for proving programs, in: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), Elsevier Science Publishers B.V., North Holland, 1990, pp. 841–994. Crolard, 2004, A formulæ-as-types interpretation of subtractive logic, J. Logic Comput., 14, 529, 10.1093/logcom/14.4.529 T. Crolard, Certification de programmes impératifs d’ordre supérieur avec mécanismes de contrôle, Habilitation Thesis, LACL, Université Paris-Est, 2010. T. Crolard, A formally specified program logic for higher-order procedural variables and non-local jumps, Technical Report TR-LACL-2011-5, Université Paris-Est, 2011. Also available as arXiv:1112.1848. T. Crolard, E. Polonowski, A program logic for higher-order procedural variables and non-local jumps, Technical Report TR-LACL-2011-4, Université Paris-Est, 2011, Chapter 3 of the first author’s Habilitation thesis. Also available as arXiv:1112.1554. Crolard, 2009, Extending the Loop Language with Higher-Order Procedural Variables, ACM TOCL Implicit Comput. Complex., 10, 1 Curry, 1958 Damm, 1983, A sound relatively complete Hoare-logic for a language with higher type procedures, Acta Inform., 20, 59, 10.1007/BF00264295 O. Danvy, Back to Direct Style, in: ESOP’92, Springer, 1992, pp. 130–150. Danvy, 1992, Back to direct style II: first-class continuations, SIGPLAN Lisp Pointers, V, 299, 10.1145/141478.141564 P. de Groote, A simple calculus of exception handling, in: Second International Conference on Typed Lambda Calculi and Applications, LNCS, Edinburgh, United Kingdom, 1995, pp. 201–215. Donahue, 1977, Locations considered unnecessary, Acta Inform., 8, 221, 10.1007/BF00264468 M. Felleisen, The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages, Ph.D. thesis, Indiana University, Indianapolis, IN, USA, 1987. X. Feng, Z. Shao, A. Vaynberg, S. Xiang, Z. Ni, Modular verification of assembly code with stack-based control abstractions, in: Proceedings of the 2006 ACM SIGPLAN, Conference on Programming Language Design and Implementation (PLDI’06), New York, NY, USA, June 2006, ACM Press, pp. 401–414. Floyd, 1967, Assigning meanings to programs, Math. Aspects Comput. Sci., 19, 1 Friedman, 1978, Classically and intuitionistically provably recursive functions, Higher Set Theory, 21, 10.1007/BFb0103100 J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, vol. 7, Cambridge Tracts in Theorical Comp. Sci., 1989. Gödel, 1958, Über eine bisher noch nicht benützteerweiterung des finiten standpunktes, Dialectica, 12, 280, 10.1111/j.1746-8361.1958.tb01464.x Gordon, 1988 T.G. Griffin, A formulæ-as-types notion of control, in: Conference Record of the 17th Annual ACM Symposium on Principles of Programming Langages, 1990, pp. 47–58. Harper, 1993, Typing first-class continuations in ML, J. Funct. Programming, 3, 465, 10.1017/S095679680000085X J. Hatcliff, O. Danvy, A generic account of continuation-passing styles, in: POPL ’94: Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA, ACM, 1994, pp. 458–471. Henson, 1990, Information loss in the programming logic TK H. Herbelin, On the degeneracy of sigma-types in presence of computational classical logic, in: Pawel Urzyczyn (Ed.), Seventh International Conference, TLCA ’05, Nara, Japan, April 2005, Proceedings, Lecture Notes in Computer Science, vol. 3461, Springer, 2005, pp. 209–220. Hoare, 1969, An axiomatic basis for computer programming, Commun. ACM, 12, 576, 10.1145/363235.363259 C.A.R. Hoare, Procedures and parameters: an axiomatic approach, in: Symposium on Semantics of Algorithmic Languages, vol. 188, Springer, 1971, pp. 102–116. Honda, 2006, Descriptive and relative completeness of logics for higher-order functions, Autom. Lang. Programming, 360, 10.1007/11787006_31 Honda, 2005, An observationally complete program logic for imperative higher-order functions, Symp. Logic Comput. Sci. LICS, 5, 270 W.A. Howard, The formulæ-as-types notion of constructions, in: H.B. To, Curry: Essays on Combinatory Logic, Lambda-Calculs and Formalism, Academic Press, 1969, pp. 479–490. K. Jensen, Connection between Dijkstra’s predicate transformers and denotational continuation semantics, Technical Report DAIMI PB-86, Computer Science Dept., Aarhus Univ., 1978. Jones, 1990 Kelsey, 1998, Revised5 report on the algorithmic language scheme, Higher-Order Symbolic Comput., 11, 7, 10.1023/A:1010051815785 Kleymann, 1999, Hoare logic and auxiliary variables, Formal Aspects Comput., 11, 541, 10.1007/s001650050057 Krivine, 1994, Classical logic, storage operators and second order λ-calculus, Ann. Pure Appl. Logic, 68, 53, 10.1016/0168-0072(94)90047-7 Krivine, 1990, Programming with proofs, J. Inf. Process. Cybernet. EIK, 26, 149 Landin, 1964, The mechanical evaluation of expressions, Comput. J., 6, 308, 10.1093/comjnl/6.4.308 Landin, 1965, A correspondence between ALGOL 60 and Church’s lambda-notations: part II, Commun. ACM, 8, 158, 10.1145/363791.363804 P.J. Landin, A generalization of jumps and labels, Technical Report, UNIVAC Systems Programming Research, 1965. Landin, 1965, A correspondence between ALGOL 60 and Church’s lambda-notation: part I, Commun. ACM, 8, 89, 10.1145/363744.363749 Leivant, 1990, Contracting proofs to programs, 279 Leivant, 2002, Intrinsic reasoning about functional programs I: first order theories, Ann. Pure Appl. Logic, 114, 117, 10.1016/S0168-0072(01)00078-1 C. Lewington, Towards constructive program derivation in VDM, in: Kesav Nori, C. Veni Madhavan (Eds.), Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 472, Springer, Berlin/Heidelberg, 1990, pp. 115–132. Y. Makarov, Practical program extraction from classical proofs, Electron. Notes Theor. Comput. Sci. 155 (2006) 521–542 (in: Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)). Y. Makarov, Simplifying programs extracted from classical proofs, in: Stephen van Bakel, Stefano Berardi (Eds.), Workshop on Classical Logic and Computation, 2006. A.R. Meyer, D.M. Ritchie, The complexity of loop programs, in: Proceedings of the ACM Nat. Meeting, 1976. E. Moggi, An Abstract View of Programming Languages, University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science, 1990. Moggi, 1991, Notions of computation and monads, Inform. and Comput., 93, 55, 10.1016/0890-5401(91)90052-4 C.R. Murthy, Extracting constructive content from classical proofs, Ph.D. thesis, Cornell University, Department of Computer Science, 1990. C.R. Murthy, An evaluation semantics for classical proofs, in: Proceedings of the 6th Annual IEEE Symp. on Logic in Computer Science, 1991, pp. 96–107. C.R. Murthy, Classical proofs as programs: how, when, and why, Technical Report 91-1215, Cornell University, Department of Computer Science, 1991. A. Nanevski, G. Morrisett, L. Birkedal, Polymorphism and separation in hoare type theory, in: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, ACM, New York, NY, USA, 2006, pp. 62–73. A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, L. Birkedal, Ynot: reasoning with the awkward squad, in: ACM SIGPLAN International Conference on Functional Programming, Citeseer, 2008. O’Donnell, 1982, A critique of the foundations of Hoare style programming logics, Commun. ACM, 25, 927, 10.1145/358728.358748 O’Hearn, 2000, From Algol to polymorphic linear lambda-calculus, J. ACM, 47, 167, 10.1145/331605.331611 M. Parigot, Strong normalization for second order classical natural deduction, in: Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, 1993. Pfenning, 2001, A judgmental reconstruction of modal logic, Math. Struct. Comput. Sci., 11, 511, 10.1017/S0960129501003322 F. Pfenning, C. Schürmann, System description: Twelf – a meta-logical framework for deductive systems, in: CADE-16: Proceedings of the 16th International Conference on Automated Deduction, London, UK, Springer-Verlag, 1999, pp. 202–206. Plotkin, 1975, Call-by-name, call-by-value and the lambda-calculus, TCS, 1, 125, 10.1016/0304-3975(75)90017-1 I. Poernomo, Proofs-as-imperative-programs: application to synthesis of contracts, in: Perspectives of System Informatics: 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia, July 9–12, 2003, Revised Papers, 2003. I. Poernomo, J.N. Crossley, The Curry–Howard isomorphism adapted for imperative program synthesis and reasoning, in: Proceedings of the 7th and 8th Asian Logic Conferences, World Scientific, 2003. N.J. Rehof, M.H. Sørensen, The λΔ-calculus, in: Theoretical Aspects of Computer Software, LNCS, vol. 542, Springer-Verlag, 1994, pp. 516–542. Reus, 2005, About Hoare logics for higher-order store, Autom. Lang. Programming, 1337, 10.1007/11523468_108 Reynolds, 1974, On the relation between direct and continuation semantics, Autom. Lang. Programming, 141, 10.1007/3-540-06841-4_57 Schmidt, 1986 D. Sitaram, M. Felleisen, Reasoning with continuations II: full abstraction for models of control, in: Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP ’90, New York, NY, USA, ACM, 1990, pp. 161–175. M.H. Sørensen, P. Urzyczyn, Lectures on the Curry–Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, vol. 149, Elsevier, 2006. Spivey, 1989 W. Swierstra, A hoare logic for the state monad, in: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 5674, Springer, 2009, pp. 440–451. G. Tan, A.W. Appel, A compositional logic for control flow, in: Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 3855, Springer, 2006, pp. 80–94. Tennent, 1991, Continuations in possible-world semantics, Theor. Comput. Sci., 85, 283, 10.1016/0304-3975(91)90184-4 Thielecke, 1998, An introduction to Landin’s “A Generalization of Jumps and Labels”, Higher-Order Symbolic Comput., 11, 117, 10.1023/A:1010060315625 Thielecke, 2008, Control effects as a modality, J. Funct. Programming, 19, 17, 10.1017/S0956796808006734 A.S. Troelstra, Realizability, in: Handbook of Proof Theory, vol. 137, chapter VI, Elsevier, 1998, pp. 407–473. H. Xi, Imperative programming with dependent types, in: Proceedings of 15th IEEE Symposium on Logic in Computer Science, Santa Barbara, 2000, pp. 375–387.