Abstract effects and proof-relevant logical relations

Abstract

We give a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked: non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as 'pure' or 'read only'. This 'fictional purity' allows clients of a module to validate soundly more effect-based program equivalences than would be possible with previous semantics. Our semantics uses a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves twoawkward problems caused by naïve use of existential quantification in Kripke logical relations, namely failure of admissibility and spurious functional dependencies.

References

1. A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009.
2. G. Barthe, V. Capretta, and O. Pons. Setoids in type theory. J. Funct. Program., 13(2):261--293, 2003.
3. N. Benton, L. Beringer, M. Hofmann, and A. Kennedy. Relational semantics for effect-based program transformations: higher-order store. In PPDP, 2009.
4. N. Benton, M. Hofmann, and V. Nigam. Proof-relevant logical relations for name generation. In TLCA, 2013.
5. N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In ICFP, 2009.
6. N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect-based program transformations with dynamic allocation. In PPDP, 2007.
7. N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Reading, writing and relations. In APLAS, volume 4279 of LNCS, 2006.
8. N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In ICFP, 1998.
9. N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In TLCA, volume 3461 of LNCS, 2005.
10. L. Birkedal, A. Carboni, G. Rosolini, and D. S. Scott. Type theory via exact categories. In LICS, 1998.
11. L. Birkedal, K. Stovring, and J. Thamsborg. The category-theoretic solution of recursive metric-space equations. Theor. Comp. Sci., 411:4102--4122, 2010.
12. G. Boudol. Typing termination in a higher-order concurrent imperative language. Inf. Comput., 208(6), 2010.
13. C. Calcagno, P. W. O'Hearn, and H. Yang. Local action and abstract separation logic. In LICS, pages 366--378, 2007.
14. A. Carboni, P. J. Freyd, and A. Scedrov. A categorical approach to realizability and polymorphic types. In MFPS, LNCS 298, 1987.
15. Y. Cheon, G. T. Leavens, M. Sitaraman, and S. H. Edwards. Model variables: cleanly supporting abstraction in design by contract. Softw., Pract. Exper., 35(6):583--599, 2005.
16. W. P. de Roever and K. Engelhardt. Data Refinement: Model-oriented Proof Theories and their Comparison. Cambridge University Press, 1998.
17. T. Dinsdale-Young, P. Gardner, and M. J. Wheelhouse. Abstraction and refinement for local reasoning. In VSTTE, volume 6217 of LNCS, 2010.
18. D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. Logical Methods in Computer Science, 7(2), 2011.
19. D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In Proc. ICFP, ACM, pages 143--156, 2010.
20. J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, and A. Schmitt. Combinators for bi-directional tree transformations: a linguistic approach to the view update problem. In POPL, pages 233--246, 2005.
21. M. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Asp. Comput., 13(3--5):341--363, 2002.
22. D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In LISP and Functional Programming, 1986.
23. C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In POPL, 2011.
24. C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and kripke logical relations. In J. Field and M. Hicks, editors, POPL, pages 59--72. ACM, 2012.
25. J. B. Jensen and L. Birkedal. Fictional separation logic. In ESOP, volume 7211 of LNCS, 2012.
26. O. Kammar and G. D. Plotkin. Algebraic foundations for effect-dependent optimisations. In POPL, 2012.
27. V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, 2006.
28. N. Krishnaswami, L. Birkedal, and J. Aldrich. Verifying event-driven programs using ramified frame properties. In TLDI, 2010.
29. N. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In ICFP, 2012.
30. R. Ley-Wild and A. Nanevski. Subjective auxiliary state for coarse-grained concurrency. In POPL, 2013.
31. S. Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer, 2nd edition, Sept. 1998.
32. B. Meyer. Applying "design by contract". IEEE Computer, 25(10):40--51, 1992.
33. F. Oles. A Category-Theoretic Approach to the Semantics of Programming Languages. PhD thesis, Carnegie Mellon University, 1982.
34. A. Pitts and I. Stark. Operational reasoning for functions with local state. In Higher order operational techniques in semantics, pages 227--273. Cambridge University Press, 1998.
35. A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013.
36. A. M. Pitts and I. D. B. Stark. Observable properties of higher-order functions that dynamically create local names, or what's new? In MFCS, volume 711 of LNCS, 1993.
37. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002.
38. J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare triples and frame rules for higher-order store. Logical Methods in Computer Science, 7(3), 2011.
39. I. Stark. Names and Higher-Order Functions. PhD thesis, U. Cambridge, 1994.
40. E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. In POPL, 2005.
41. J. Thamsborg and L. Birkedal. A Kripke logical relation for effect-based program transformations. In ICFP, 2011.
42. V. Vafeiadis and M. J. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, volume 4703 of LNCS, 2007.
43. P. Wadler and P. Thiemann. The marriage of effects and monads. ACM Trans. Comput. Log., 4(1):1--32, 2003.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Compilers

      • Dynamic compilers

  • Software organization and properties

    • Contextual software domains

      • Operating systems

        • Memory management

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program analysis

    • Program semantics

      • Denotational semantics