ABSTRACT
There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged are *bisimulations* and *Kripke logical relations (KLRs)*. While both approaches are powerful, their complementary advantages have led us and other researchers to wonder whether there is an essential tradeoff between them. Furthermore, both approaches seem to suffer from fundamental limitations if one is interested in scaling them to inter-language reasoning. In this paper, we propose *relation transition systems (RTSs)*, which marry together some of the most appealing aspects of KLRs and bisimulations. In particular, RTSs show how bisimulations' support for reasoning about recursive features via *coinduction* can be synthesized with KLRs' support for reasoning about local state via *state transition systems*. Moreover, we have designed RTSs to avoid the limitations of KLRs and bisimulations that preclude their generalization to inter-language reasoning. Notably, unlike KLRs, RTSs are transitively composable.
Supplemental Material
- S. Abramsky. The lazy lambda calculus. In D. A. Turner, editor, Research Topics in Functional Programming, pages 65--117. 1990. Google ScholarDigital Library
- A. Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. Google ScholarDigital Library
- A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006. Google ScholarDigital Library
- A. Ahmed and M. Blume. An equivalence-preserving CPS translation via multi-language semantics. In ICFP, 2011. Google ScholarDigital Library
- A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009. Google ScholarDigital Library
- A. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23(5):657--683, 2001. Google ScholarDigital Library
- N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In ICFP, 2009. Google ScholarDigital Library
- L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and K. Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. In LICS, 2011. Google ScholarDigital Library
- L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. LMCS, 2(5:1), 2006.Google Scholar
- A. Buisse, L. Birkedal, and K. Støvring. A step-indexed Kripke model of separation logic for storable locks. In MFPS, 2011.Google ScholarDigital Library
- D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. LMCS, 7(2:16):1--37, June 2011.Google Scholar
- D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In ICFP, 2010. Google ScholarDigital Library
- D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal logic for higher-order stateful ADTs. In POPL, 2010. Google ScholarDigital Library
- J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. Google ScholarDigital Library
- A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv. Local reasoning about storable locks and threads. In APLAS, 2007. Google ScholarDigital Library
- A. Hobor, A. Appel, and F. Zappa Nardelli. Oracle semantics for concurrent separation logic. In ESOP, 2008. Google ScholarDigital Library
- C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In POPL, 2011. Google ScholarDigital Library
- V. Koutavas, P. B. Levy, and E. Sumii. From applicative to environmental bisimulation. In MFPS, 2011.Google ScholarDigital Library
- V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, 2006. Google ScholarDigital Library
- J. Laird. A fully abstract trace semantics for general references. In ICALP, 2007. Google ScholarDigital Library
- S. Lassen. Eager normal form bisimulation. In LICS, 2005. Google ScholarDigital Library
- S. B. Lassen and P. B. Levy. Typed normal form bisimulation. In CSL, 2007. Google ScholarDigital Library
- S. B. Lassen and P. B. Levy. Typed normal form bisimulation for parametric polymorphism. In LICS, 2008. Google ScholarDigital Library
- N. P. Mendler. Inductive types and type constraints in the second-order lambda-calculus. Annals of Pure and Applied Logic, 51(1--2):159--172, 1991.Google ScholarCross Ref
- A. S. Murawski and N. Tzevelekos. Game semantics for good general references. In LICS, 2011. Google ScholarDigital Library
- G. Neis, D. Dreyer, and A. Rossberg. Non-parametric parametricity. JFP, 21(4&5):497--562, 2011. Google ScholarDigital Library
- B. C. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM, 47(3):531--586, 2000. Google ScholarDigital Library
- A. Pitts. Typed operational reasoning. In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 7. MIT Press, 2005.Google Scholar
- A. Pitts and I. Stark. Operational reasoning for functions with local state. In HOOTS, 1998. Google ScholarDigital Library
- A. M. Pitts. Relational properties of domains. Information and Computation, 127:66--90, 1996.Google ScholarCross Ref
- J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, 1983.Google Scholar
- D. Sangiorgi. The lazy lambda calculus in a concurrency scenario. Information and Computation, 111(1):120--153, 1994. Google ScholarDigital Library
- D. Sangiorgi, N. Kobayashi, and E. Sumii. Environmental bisimulations for higher-order languages. In LICS, 2007. Google ScholarDigital Library
- K. Støvring and S. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In POPL, 2007. Google ScholarDigital Library
- E. Sumii. A complete characterization of observational equivalence in polymorphic łambda-calculus with general references. In CSL, 2009. Google ScholarDigital Library
- E. Sumii and B. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5):1--43, 2007. Google ScholarDigital Library
- J. Thamsborg and L. Birkedal. A Kripke logical relation for effect-based program transformations. In ICFP, 2011. Google ScholarDigital Library
- T. Uustalu and V. Vene. Mendler-style inductive types, categorically. Nordic Journal of Computing, 6(3):343--361, 1999. Google ScholarDigital Library
- V. Vafeiadis. Concurrent separation logic and operational semantics. In MFPS, 2011.Google ScholarDigital Library
- P. Wadler. Theorems for free! In FPCA, 1989. Google ScholarDigital Library
Index Terms
- The marriage of bisimulations and Kripke logical relations
Recommendations
The marriage of bisimulations and Kripke logical relations
POPL '12There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and ...
Logical Step-Indexed Logical Relations
LICS '09: Proceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer ScienceWe show how to reason about "step-indexed" logical relations in an abstract way, avoiding the tedious, error-prone, and proof-obscuring step-index arithmetic that seems superficially to be an essential element of the method. Specifically, we define a ...
Pilsner: a compositionally verified compiler for a higher-order imperative language
ICFP '15Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different ...
Comments