Document Open Access Logo

A Fibrational Tale of Operational Logical Relations

Authors Francesco Dagnino , Francesco Gavazzo

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.3.pdf
  • Filesize: 0.93 MB
  • 21 pages

Document Identifiers

Author Details

Francesco Dagnino
  • University of Genova, Italy
Francesco Gavazzo
  • University of Bologna, Italy

Funding

This work was partially funded by the MUR project T-LADIES (PRIN 2020TL3X8X). The second author is supported by the ERC Consolidator Grant DLV-818616 DIAPASoN.

Acknowledgements

The authors would like to thank the anonymous reviewers for the many useful comments, some of which improved of our work.

Cite AsGet BibTex

Francesco Dagnino and Francesco Gavazzo. A Fibrational Tale of Operational Logical Relations. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.3

Abstract

Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a λ-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations - a recently introduced notion of higher-order distance between programs - both pure and effectful, bringing them back to a common picture with traditional ones.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
Keywords
  • logical relations
  • operational semantics
  • fibrations
  • generic effects
  • program distance

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proc. ACM Program. Lang., 4(ICFP):90:1-90:28, 2020. URL: https://doi.org/10.1145/3408972.
  2. S. Abramsky and A. Jung. Domain theory. In Handbook of Logic in Computer Science, pages 1-168. Clarendon Press, 1994. Google Scholar
  3. Amal J. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Proc. of ESOP 2006, pages 69-83, 2006. URL: https://doi.org/10.1007/11693024_6.
  4. Andrew W. Appel and David A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-683, 2001. Google Scholar
  5. A.W. Appel and D.A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-683, 2001. URL: https://doi.org/10.1145/504709.504712.
  6. Robert J. Aumann. Borel structures for function spaces. Illinois Journal of Mathematics, 5(4):614-630, 1961. Google Scholar
  7. H.P. Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  8. M. Barr. Relational algebras. Lect. Notes Math., 137:39-55, 1970. Google Scholar
  9. Jean Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, pages 1-77. Springer, 1967. URL: https://doi.org/10.1007/BFb0074299.
  10. Nick Benton, Martin Hofmann, and Vivek Nigam. Abstract effects and proof-relevant logical relations. In Proc. of POPL 2014, pages 619-632, 2014. Google Scholar
  11. Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Handle with care: relational interpretation of algebraic effects and handlers. PACMPL, 2(POPL):8:1-8:30, 2018. Google Scholar
  12. Lars Birkedal, Guilhem Jaber, Filip Sieczkowski, and Jacob Thamsborg. A kripke logical relation for effect-based program transformations. Inf. Comput., 249:160-189, 2016. Google Scholar
  13. A. Bizjak and L. Birkedal. Step-indexed logical relations for probability. In Proc. of FOSSACS 2015, pages 279-294, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_18.
  14. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. In Proc. of CONCUR 2018, pages 17:1-17:17, 2018. Google Scholar
  15. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Coinduction up-to in a fibrational setting. In Proc. of CSL-LICS '14, pages 20:1-20:9, 2014. Google Scholar
  16. Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 33-46, 2016. Google Scholar
  17. Karl Crary and Robert Harper. Syntactic logical relations for polymorphic and recursive types. Electr. Notes Theor. Comput. Sci., 172:259-299, 2007. Google Scholar
  18. Francesco Dagnino and Fabio Pasquali. Logical foundations of quantitative equality. In Proceedings of the 37th ACM/IEEE Symposium on Logic in Computer Science, LICS 2022. ACM, 2022. to appear. URL: https://doi.org/10.1145/3531130.3533337.
  19. Francesco Dagnino and Giuseppe Rosolini. Doctrines, modalities and comonads. Mathematical Structures in Computer Science, pages 1-30, 2021. URL: https://doi.org/10.1017/S0960129521000207.
  20. Ugo Dal Lago and Francesco Gavazzo. Effectful normal form bisimulation. In Proc. of ESOP 2019, pages 263-292, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_10.
  21. Ugo Dal Lago and Francesco Gavazzo. On bisimilarity in lambda calculi with continuous probabilistic choice. In Proc. of MFPS 2019, pages 121-141, 2019. URL: https://doi.org/10.1016/j.entcs.2019.09.007.
  22. Ugo Dal Lago and Francesco Gavazzo. Differential logical relations part II: increments and derivatives. In Gennaro Cordasco, Luisa Gargano, and Adele A. Rescigno, editors, Proc. of ICTCS 2020, volume 2756 of CEUR Workshop Proceedings, pages 101-114, 2020. Google Scholar
  23. Ugo Dal Lago and Francesco Gavazzo. Differential logical relations, part II increments and derivatives. Theor. Comput. Sci., 895:34-47, 2021. Google Scholar
  24. Ugo Dal Lago and Francesco Gavazzo. Resource transition systems and full abstraction for linear higher-order effectful programs. In Proc. of FSCD 2021, volume 195 of LIPIcs, pages 23:1-23:19, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.23.
  25. Ugo Dal Lago and Francesco Gavazzo. Effectful program distancing. Proc. ACM Program. Lang., 6(POPL):1-30, 2022. Google Scholar
  26. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proc. ACM Program. Lang., 6(POPL):1-28, 2022. Google Scholar
  27. Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. Effectful applicative bisimilarity: Monads, relators, and howe’s method. In Proc. of LICS 2017, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005117.
  28. Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. Effectful applicative similarity for call-by-name lambda calculi. In Proc. of ICTCS 2017, pages 87-98, 2017. Google Scholar
  29. Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. Effectful applicative similarity for call-by-name lambda calculi. Theor. Comput. Sci., 813:234-247, 2020. URL: https://doi.org/10.1016/j.tcs.2019.12.025.
  30. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, Proc. of ICALP 2019, volume 132 of LIPIcs, pages 111:1-111:14, 2019. Google Scholar
  31. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Proc. of ICALP 2019, pages 111:1-111:14, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.111.
  32. Derek Dreyer, Amal Ahmed, and Lars Birkedal. Logical step-indexed logical relations. Logical Methods in Computer Science, 7(2), 2011. Google Scholar
  33. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program., 22(4-5):477-528, 2012. Google Scholar
  34. Brian P. Dunphy and Uday S. Reddy. Parametric limits. In Proc. of LICS 2004, pages 242-251. IEEE Computer Society, 2004. Google Scholar
  35. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Proc. of POPL 2017, 2:1-28, 2017. Google Scholar
  36. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. PACMPL, 2(POPL):59:1-59:28, 2018. Google Scholar
  37. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proc. of LICS 2018, pages 452-461, 2018. URL: https://doi.org/10.1145/3209108.3209149.
  38. Francesco Gavazzo. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. PhD thesis, University of Bologna, Italy, 2019. URL: http://amsdottorato.unibo.it/9075/.
  39. Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, and Tim Revell. Bifibrational functorial semantics of parametric polymorphism. In Dan R. Ghica, editor, Proc. of MFPS 2015, volume 319 of Electronic Notes in Theoretical Computer Science, pages 165-181. Elsevier, 2015. Google Scholar
  40. Neil Ghani, Patricia Johann, and Clément Fumex. Fibrational induction rules for initial algebras. In Anuj Dawar and Helmut Veith, editors, Proc. of CSL 2010, volume 6247 of Lecture Notes in Computer Science, pages 336-350. Springer, 2010. Google Scholar
  41. Neil Ghani, Patricia Johann, and Clément Fumex. Generic fibrational induction. Log. Methods Comput. Sci., 8(2), 2012. Google Scholar
  42. Neil Ghani, Patricia Johann, and Clément Fumex. Indexed induction and coinduction, fibrationally. Log. Methods Comput. Sci., 9(3), 2013. Google Scholar
  43. J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. Google Scholar
  44. Michèle Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, pages 68-85. Springer Berlin Heidelberg, 1982. Google Scholar
  45. A.D. Gordon. A tutorial on co-induction and functional programming. In Workshops in Computing, pages 78-95. Springer London, September 1994. URL: https://doi.org/10.1007/978-1-4471-3573-9_6.
  46. Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. Math. Struc. Comput. Sci., 18(6):1169-1217, 2008. URL: https://doi.org/10.1017/S0960129508007172.
  47. Marco Grandis. Weak subobjects and the epi-monic completion of a category. Journal of Pure and Applied Algebra, 154(1-3):193-212, 2000. Google Scholar
  48. Robert Harper. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press, 2016. Google Scholar
  49. Claudio Hermida. Fibrations, logical predicates and indeterminates. PhD thesis, University of Edinburgh, UK, 1993. Google Scholar
  50. Claudio Hermida and Bart Jacobs. Structural induction and coinduction in a fibrational setting. Inf. Comput., 145(2):107-152, 1998. Google Scholar
  51. Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson. Logical relations and parametricity - A reynolds programme for category theory and programming languages. Electronic Notes on Theoretical Computer Science, 303:149-180, 2014. URL: https://doi.org/10.1016/j.entcs.2014.02.008.
  52. Martin Hofmann. Logical relations and nondeterminism. In Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, pages 62-74, 2015. Google Scholar
  53. Pieter Hofstra. The dialectica monad and its cousins. In Models, Logics, and Higher-dimensional Categories: A Tribute to the Work of Mihaly Makkai, number 53 in CRM proceedings & lecture notes, pages 107-139, 2011. Google Scholar
  54. Jesse Hughes and Bart Jacobs. Factorization systems and fibrations: Toward a fibred birkhoff variety theorem. In Richard Blute and Peter Selinger, editors, CTCS 2002, volume 69 of Electronic Notes in Theoretical Computer Science, pages 156-182. Elsevier, 2002. Google Scholar
  55. Bart P. F. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics. North-Holland, 2001. URL: http://www.elsevierdirect.com/product.jsp?isbn=9780444508539.
  56. Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational metatheory for algebraic effects. In Proc. of LICS 2010, pages 209-218. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.29.
  57. Ohad Kammar and Dylan McDermott. Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics. In Sam Staton, editor, Proc. of MFPS 2018, volume 341 of Electronic Notes in Theoretical Computer Science, pages 239-260. Elsevier, 2018. Google Scholar
  58. Shin-ya Katsumata. A generalisation of pre-logical predicates and its applications. PhD thesis, University of Edinburgh, UK, 2005. Google Scholar
  59. Shin-ya Katsumata. A semantic formulation of tt-lifting and logical predicates for computational metalanguage. In C.-H. Luke Ong, editor, Proc. of CSL 2005, volume 3634 of Lecture Notes in Computer Science, pages 87-102. Springer, 2005. Google Scholar
  60. Shin-ya Katsumata. Relating computational effects by ⊤⊤-lifting. Inf. Comput., 222:228-246, 2013. Google Scholar
  61. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Proc. of POPL 2014, pages 633-646, 2014. Google Scholar
  62. Shin-ya Katsumata, Tetsuya Sato, and Tarmo Uustalu. Codensity lifting of monads and its dual. Logical Methods in Computer Science, 14(4), 2018. Google Scholar
  63. G. A. Kavvos. Modalities, cohesion, and information flow. Proc. ACM Program. Lang., 3(POPL):20:1-20:29, 2019. Google Scholar
  64. Gregory M. Kelly. Basic concepts of enriched category theory. Reprints in Theory and Applications of Categories, (10):1-136, 2005. Google Scholar
  65. Daan Leijen. Implementing algebraic effects in c. In Bor-Yuh Evan Chang, editor, Programming Languages and Systems, pages 339-363, Cham, 2017. Springer International Publishing. Google Scholar
  66. P.B. Levy, J. Power, and H. Thielecke. Modelling environments in call-by-value programming languages. Inf. Comput., 185(2):182-210, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00088-9.
  67. Daniel R. Licata, Michael Shulman, and Mitchell Riley. A fibrational framework for substructural and modal logics. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, volume 84 of LIPIcs, pages 25:1-25:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.25.
  68. QingMing Ma and John C. Reynolds. Types, abstractions, and parametric polymorphism, part 2. In Proc. of MFPS 1991, volume 598 of Lecture Notes in Computer Science, pages 1-40. Springer, 1991. Google Scholar
  69. Maria Emilia Maietti, Fabio Pasquali, and Giuseppe Rosolini. Quasi-toposes as elementary quotient completions, 2021. URL: http://arxiv.org/abs/arXiv:2111.15299.
  70. Maria Emilia Maietti and Giuseppe Rosolini. Elementary quotient completion. Theory and Application of Categories, 27(17):445-463, 2013. Google Scholar
  71. Ernest G. Manes and Michael A. Arbib. Algebraic Approaches to Program Ssemantics. Texts and Monographs in Computer Science. Springer, 1986. Google Scholar
  72. Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM Symposium on Principles of Programming Languages, POPL 2015, pages 3-16. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676970.
  73. Paul-André Melliès and Noam Zeilberger. A bifibrational reconstruction of lawvere’s presheaf hyperdoctrine. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 555-564. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934525.
  74. John C. Mitchell. Foundations for programming languages. Foundation of computing series. MIT Press, 1996. Google Scholar
  75. John C. Mitchell and Andre Scedrov. Notes on sconing and relators. In Proc. of CSL '92, volume 702 of Lecture Notes in Computer Science, pages 352-378. Springer, 1992. Google Scholar
  76. Peter W. O'Hearn and Robert D. Tennent. Parametricity and local variables. J. ACM, 42(3):658-709, 1995. Google Scholar
  77. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  78. Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In Proc. of LICS 2021, pages 1-14, 2021. Google Scholar
  79. Gordon Plotkin. Lambda-definability and logical relations. Technical Report SAI-RM-4, School of A.I., University of Edinburgh, 1973. Google Scholar
  80. Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Proc. of FOSSACS 2001, pages 1-24, 2001. URL: https://doi.org/10.1007/3-540-45315-6_1.
  81. Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69-94, 2003. URL: https://doi.org/10.1023/A:1023064908962.
  82. J. Reed and B.C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Proc. of ICFP 2010, pages 157-168, 2010. URL: https://doi.org/10.1145/1863543.1863568.
  83. J.C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513-523, 1983. Google Scholar
  84. Edmund P. Robinson and Giuseppe Rosolini. Reflexive graphs and parametric polymorphism. In Proc. of LICS '94, pages 364-371. IEEE Computer Society, 1994. Google Scholar
  85. Michael A. Shulman. Framed bicategories and monoidal fibrations. Theory and Applications of Categories, (18):650-738, 2008. Google Scholar
  86. Kristina Sojakova and Patricia Johann. A general framework for relational parametricity. In Anuj Dawar and Erich Grädel, editors, Proce. of LICS 2018,, pages 869-878. ACM, 2018. Google Scholar
  87. Richard Statman. Logical relations and the typed lambda-calculus. Inf. Control., 65(2/3):85-97, 1985. Google Scholar
  88. Sam Staton. Commutative semantics for probabilistic programming. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, pages 855-879, 2017. Google Scholar
  89. Sam Staton, Hongseok Yang, Frank D. Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 525-534, 2016. Google Scholar
  90. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. URL: https://doi.org/10.1016/0022-4049(72)90019-9.
  91. Ross Street. Two constructions on lax functors. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 13(3):217-264, 1972. Google Scholar
  92. Thomas Streicher. Fibered categories a la jean benabou, 2018. URL: http://arxiv.org/abs/arXiv:1801.02927.
  93. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. Google Scholar
  94. Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. Logical relations for fine-grained concurrency. In Roberto Giacobazzi and Radhia Cousot, editors, Proc. of POPL '13, pages 343-356. ACM, 2013. Google Scholar
  95. Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. Proc. ACM Program. Lang., 3(POPL):36:1-36:29, 2019. Google Scholar
  96. C. Villani. Optimal Transport: Old and New. Grundlehren der mathematischen Wissenschaften. Springer Berlin Heidelberg, 2008. Google Scholar
  97. Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb. Contextual equivalence for a probabilistic language with continuous random variables and recursion. PACMPL, 2(ICFP):87:1-87:30, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact