Document Open Access Logo

An Algebraic Approach to Formal System Metatheory

Author Francesco Gavazzo

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.50.pdf
  • Filesize: 1.01 MB
  • 31 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • Relation Algebra
  • Term Relations
  • Language Metatheory
  • Formal System Metatheory

Metrics

Abstract

We introduce an algebraic approach to the metatheory of formal systems of term assertions akin to those of structural and natural operational semantics, type theories, rewriting systems, and equational theories. We rest on Term Relation Algebras, viz. pointfree algebras of structurally-defined predicates on terms, to give a common algebraic semantics to different kinds of formal systems, regardless of their inferential mechanisms and underlying term structures. This enables abstract reasoning about formal systems, and their metatheory, through the algebra of the term predicates they define. We give a faithfully term-free algebraization of semantically-relevant term predicates, such as parallel reduction, big-step evaluation, and applicative bisimilarity. We extend this algebraization also to fundamental metatheoretical properties of these notions - including congruence of applicative bisimilarity, determinacy of evaluation, and confluence of reduction - and prove these properties using algebraic methods.

Cite As Get BibTex

Francesco Gavazzo. An Algebraic Approach to Formal System Metatheory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 50:1-50:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.50

Author Details

Francesco Gavazzo
  • University of Padova, Italy

Funding

This work was partially supported by the 2026 STARS Grants@Unipd CoG RELATIONS and by PRIN 2022 PNRR Project No. P2022HXNSC.

References

  1. Martín Abadi and Luca Cardelli. A Theory of Objects. Monographs in Computer Science. Springer, 1996. URL: https://doi.org/10.1007/978-1-4419-8598-9.
  2. Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, and Conor McBride. Derivatives of containers. In Martin Hofmann, editor, Proc. of TLCA 2003, volume 2701 of Lecture Notes in Computer Science, pages 16-30. Springer, 2003. URL: https://doi.org/10.1007/3-540-44904-3_2.
  3. S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-117. Addison Wesley, 1990. Google Scholar
  4. Samson Abramsky. Computational interpretations of linear logic. Theor. Comput. Sci., 111(1&2):3-57, 1993. URL: https://doi.org/10.1016/0304-3975(93)90181-R.
  5. Luca Aceto, Wan Fokkink, and Frits Vaandrager. Structural operational semantics. In J. A. Bergstra, A. Ponse, and S. A. Smolka, editors, Handbook of Process Algebra, pages 197-292. Elsevier, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50021-7.
  6. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, HANDBOOK OF MATHEMATICAL LOGIC, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier, 1977. URL: https://doi.org/10.1016/S0049-237X(08)71120-0.
  7. Peter Aczel. A general church-rosser theorem. Draft, Manchester, 1978. Google Scholar
  8. Jiří Adámek. Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae, 015(4):589-602, 1974. Google Scholar
  9. Hajnal Andréka, Judit X. Madarász, and István Németi. Algebras of relations of various ranks, some current trends and applications. Journal on Relational Methods in Computer Science, 1:27-49, 2004. Special volume (JoRMiCS). Google Scholar
  10. Martin Avanzini and Akihisa Yamada. Weighted rewriting. In René Thiemann and Christoph Weidenbach, editors, Proc. of FroCoS '25, Lecture Notes in Computer Science, pages 191-208. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04167-8_11.
  11. Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. Polynomial relators (extended abstract). In Proc. of (AMAST '91, Workshops in Computing, pages 303-326. Springer, 1991. Google Scholar
  12. Roland Carl Backhouse and Paul F. Hoogendijk. Elements of a relational theory of datatypes. In Formal Program Development - IFIP TC2/WG 2.1 State-of-the-Art Report, pages 7-42, 1993. URL: https://doi.org/10.1007/3-540-57499-9_15.
  13. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139032636.
  14. Henk P. Barendregt. Some Extensional Term Models for Combinatory Logics and Lambda Calculi. PhD thesis, Utrecht University, Utrecht, The Netherlands, 1971. Google Scholar
  15. H.P. Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  16. Gabriel A. Baum, Armando M. Haeberer, and Paulo A. S. Veloso. On the representability of the ∇-abstract relational algebra. Journal of the IGPL, 1:3-4, 1992. Google Scholar
  17. Han Bäumer. On the use of relation algebra in the theory of reduction systems. In CSN, volume 92, page 5464, 1992. Google Scholar
  18. M. Bezem, J.W. Klop, E. Barendsen, R. de Vrijer, and Terese. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  19. Richard S. Bird and Oege de Moor. Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, 1997. Google Scholar
  20. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  21. Willem J. Blok and Don Pigozzi. Algebraizable Logics, volume 396 of Memoirs of the American Mathematical Society. American Mathematical Society, Providence, 1989. Google Scholar
  22. Corrado Böhm. Alcune proprietà delle forme βη-normali del λ k-calcolo. Pubblicazioni dell'Istituto per le Applicazioni del Calcolo, 696, 1968. Google Scholar
  23. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: Rewriting with Frobenius structure. Journal of the ACM, 2022. Google Scholar
  24. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory II: Rewriting with symmetric monoidal structure. Mathematical Structures in Computer Science, 2022. Google Scholar
  25. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory III: Confluence with and without Frobenius. Mathematical Structures in Computer Science, 2022. Google Scholar
  26. Peio Borthelle, Tom Hirschowitz, and Ambroise Lafont. A cellular howe theorem. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, Proc. of LICS 2020, pages 273-286. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394738.
  27. Stanley Burris and H. P. Sankappanavar. A Course in Universal Algebra. Springer, New York, 1981. Google Scholar
  28. A. Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical Computer Science, 115(1):43-62, 1993. URL: https://doi.org/10.1016/0304-3975(93)90054-W.
  29. Rod M. Burstall. Proving properties of programs by structural induction. Comput. J., 12(1):41-48, 1969. URL: https://doi.org/10.1093/COMJNL/12.1.41.
  30. Ross Casley, Roger F. Crew, José Meseguer, and Vaughan R. Pratt. Temporal structures. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings, volume 389 of Lecture Notes in Computer Science, pages 21-51. Springer, 1989. URL: https://doi.org/10.1007/BFB0018343.
  31. Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans. AMS, 39:472-482, 1936. Google Scholar
  32. J.H. Conway. Regular Algebra and Finite Machines. Chapman and Hall mathematics series. Dover Publications, Incorporated, 2012. Google Scholar
  33. H.B. Curry and R. Feys. Combinatory Logic. Number v. 1 in Combinatory Logic. North-Holland Publishing Company, 1958. Google Scholar
  34. Francesco Dagnino, Paola Giannini, and Elena Zucca. Monadic type-and-effect soundness. In Jonathan Aldrich and Alexandra Silva, editors, Proc. of ECOOP 2025, LIPIcs, pages 7:1-7:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2025.7.
  35. Francesco Dagnino and Fabio Pasquali. Logical foundations of quantitative equality. In Christel Baier and Dana Fisman, editors, Proc. of LICS 2022, pages 16:1-16:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533337.
  36. Francesco Dagnino and Fabio Pasquali. Quantitative equality in substructural logic via lipschitz doctrines. Log. Methods Comput. Sci., 21(1), 2025. URL: https://doi.org/10.46298/LMCS-21(1:7)2025.
  37. U. Dal Lago, F. Gavazzo, and P.B. Levy. Effectful applicative bisimilarity: Monads, relators, and howe’s method. In Proc. of LICS 2017, pages 1-12, 2017. Google Scholar
  38. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proc. ACM Program. Lang., 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498692.
  39. B.A. Davey and H.A. Priestley. Introduction to lattices and order. Cambridge University Press, 1990. Google Scholar
  40. Jules Desharnais, Bernhard Möller, and Georg Struth. Algebraic notions of termination. Log. Methods Comput. Sci., 7(1), 2011. URL: https://doi.org/10.2168/LMCS-7(1:1)2011.
  41. Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453-457, 1975. URL: https://doi.org/10.1145/360933.360975.
  42. Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. Google Scholar
  43. Henk Doornbos and Roland Carl Backhouse. Algebra of program termination. In Roland Carl Backhouse, Roy L. Crole, and Jeremy Gibbons, editors, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, International Summer School and Workshop, Oxford, UK, April 10-14, 2000, Revised Lectures, volume 2297 of Lecture Notes in Computer Science, pages 203-236. Springer, 2000. URL: https://doi.org/10.1007/3-540-47797-7_6.
  44. Henk Doornbos, Roland Carl Backhouse, and Jaap van der Woude. A calculational approach to mathematical induction. Theor. Comput. Sci., 179(1-2):103-135, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00154-5.
  45. Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, Cambridge, 1991. Google Scholar
  46. Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and Peter Mager, editors, Proc. of POPL '88, pages 180-190. ACM Press, 1988. URL: https://doi.org/10.1145/73560.73576.
  47. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. The MIT Press, 1st edition, 2009. Google Scholar
  48. Marcelo P. Fiore. Second-order and dependently-sorted abstract syntax. In Proc. of LICS 2008, pages 57-68. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.38.
  49. Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 193-202. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782615.
  50. Peter J. Freyd and Andre Scedrov. Categories, allegories, volume 39 of North-Holland mathematical library. North-Holland, 1990. Google Scholar
  51. Marcelo F. Frias. Fork Algebras in Algebra, Logic and Computer Science, volume 2 of Advances in Logic. World Scientific, 2002. URL: https://doi.org/10.1142/4899.
  52. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 214-224. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782617.
  53. Francesco Gavazzo. Allegories of symbolic manipulations. In Proc. of LICS, pages 1-15, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175807.
  54. Francesco Gavazzo and Cecilia Di Florio. Elements of quantitative rewriting. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571256.
  55. Francesco Gavazzo and Claudia Faggian. A relational theory of monadic rewriting systems, part I. In Proc. of LICS 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470633.
  56. Francesco Gavazzo, Riccardo Treglia, and Gabriele Vanoni. Monadic intersection types, relationally. In Stephanie Weirich, editor, Proc. of ESOP 2024, volume 14576 of Lecture Notes in Computer Science, pages 22-51. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_2.
  57. Gerhard Gentzen. Untersuchungen Über das logische schliessen. i. Mathematische Zeitschrift, 35:176-210, 1935. Google Scholar
  58. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge University Press, USA, 1989. Google Scholar
  59. Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24(1):68-95, 1977. URL: https://doi.org/10.1145/321992.321997.
  60. Sergey Goncharov, Stefan Milius, Lutz Schröder, Stelios Tsampas, and Henning Urbat. Towards a higher-order mathematical operational semantics. Proc. ACM Program. Lang., 7(POPL):632-658, 2023. URL: https://doi.org/10.1145/3571215.
  61. A.D. Gordon. A tutorial on co-induction and functional programming. In Workshops in Computing, pages 78-95. Springer London, September 1994. Google Scholar
  62. A.D. Gordon. Bisimilarity as a theory of functional programming. In Stephen D. Brookes, Michael G. Main, Austin Melton, and Michael W. Mislove, editors, Proc. of MFPS 1995, volume 1 of Electronic Notes in Theoretical Computer Science, pages 232-252. Elsevier, 1995. URL: https://doi.org/10.1016/S1571-0661(04)80013-6.
  63. Andrew D. Gordon. Operational equivalences for untyped and polymorphic object calculi. In Andrew D. Gordon and Andrew M. Pitts, editors, Higher Order Operational Techniques in Semantics. Cambridge University Press, Cambridge, UK, 1998. Google Scholar
  64. David Gries and Fred B. Schneider. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer, 1993. URL: https://doi.org/10.1007/978-1-4757-3837-7.
  65. D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. Foundations of Computing. MIT Press, 2000. Google Scholar
  66. Robert Harper. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press, 2016. URL: https://www.cs.cmu.edu/%7Erwh/pfpl/index.html.
  67. Leon Henkin, J. Donald Monk, and Alfred Tarski. Cylindric Algebras. Part I, volume 64 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1971. Google Scholar
  68. J.R. Hindley and J.P. Seldin. Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, 2008. Google Scholar
  69. André Hirschowitz and Marco Maggesi. Modules over monads and linearity. In Daniel Leivant and Ruy J. G. B. de Queiroz, editors, Proc. of WoLLIC 2007, volume 4576 of Lecture Notes in Computer Science, pages 218-237. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73445-1_16.
  70. André Hirschowitz and Marco Maggesi. Modules over monads and initial semantics. Inf. Comput., 208(5):545-564, 2010. URL: https://doi.org/10.1016/j.ic.2009.07.003.
  71. Tom Hirschowitz and Ambroise Lafont. A categorical framework for congruence of applicative bisimilarity in higher-order languages. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/lmcs-18(3:37)2022.
  72. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  73. D.J. Howe. Proving congruence of bisimulation in functional programming languages. Inf. Comput., 124(2):103-112, 1996. URL: https://doi.org/10.1006/INCO.1996.0008.
  74. Gérard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797-821, 1980. URL: https://doi.org/10.1145/322217.322230.
  75. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherwieght java: A minimal core calculus for java and GJ. In Brent Hailpern, Linda M. Northrop, and A. Michael Berman, editors, Proc. of OOPSLA 1999, pages 132-146. ACM, 1999. URL: https://doi.org/10.1145/320384.320395.
  76. P.T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium: Volume 2. Oxford Logic Guides. Clarendon Press, 2002. Google Scholar
  77. André Joyal. Foncteurs analytiques et espèces de structures. Comptes rendus de l'Académie des sciences. Série I. Mathématique, 298(15):393-396, 1984. Google Scholar
  78. André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88(1):55-112, July 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
  79. Gilles Kahn. Natural semantics. In Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS '87, pages 22-39, Berlin, Heidelberg, 1987. Springer-Verlag. URL: https://doi.org/10.1007/BFB0039592.
  80. G. A. Kavvos. Modalities, cohesion, and information flow. Proc. ACM Program. Lang., 3(POPL):20:1-20:29, 2019. URL: https://doi.org/10.1145/3290333.
  81. Yasuo Kawahara. Notes on the universality of relational functors. Memoirs of the Faculty of Science, Kyushu University. Series A, Mathematics, 27(2):275-289, 1973. Google Scholar
  82. Jan Willem Klop. Combinatory reduction systems. PhD thesis, Univ. Utrecht, 1980. Google Scholar
  83. Dexter Kozen. On kleene algebras and closed semirings. In Branislav Rovan, editor, Proc. of MFCS 1990, volume 452 of Lecture Notes in Computer Science, pages 26-47. Springer, 1990. URL: https://doi.org/10.1007/BFb0029594.
  84. Dexter Kozen. On action algebras. DAIMI Report Series, 21(381), January 1992. URL: https://doi.org/10.7146/dpb.v21i381.6613.
  85. Dexter Kozen. A completeness theorem for kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1065.
  86. Dexter Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 19(3):427-443, 1997. URL: https://doi.org/10.1145/256167.256195.
  87. Jean-Louis Krivine. Lambda-Calculus, Types and Models. Ellis Horwood Series in Computers and Their Applications. Ellis Horwood, New York, 1993. URL: https://dl.acm.org/doi/10.5555/167408.
  88. Thomas Lamiaux and Benedikt Ahrens. An introduction to different approaches to initial semantics. CoRR, abs/2401.09366, 2024. URL: https://doi.org/10.48550/arXiv.2401.09366.
  89. S.B. Lassen. Relational Reasoning about Functions and Nondeterminism. PhD thesis, Dept. of Computer Science, University of Aarhus, May 1998. Google Scholar
  90. F. W. Lawvere. Cohesive toposes and cantor’s "Lauter Einsen". Philosophia Mathematica, 2(1):5-15, 1994. URL: https://doi.org/10.1093/philmat/2.1.5.
  91. F. William Lawvere. Adjointness in Foundations. Dialectica, 23(3-4):281-296, 1969. URL: https://doi.org/10.1111/j.1746-8361.1969.tb01194.x.
  92. F.William Lawvere. Axiomatic cohesion. Theory and Applications of Categories [electronic only], 19:41-49, 2007. Google Scholar
  93. P.B. Levy. Infinitary howe’s method. Electr. Notes Theor. Comput. Sci., 164(1):85-104, 2006. URL: https://doi.org/10.1016/J.ENTCS.2006.06.006.
  94. 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.
  95. C. Lüth. Categorical Term Rewriting: Monads and Modularity. PhD thesis, University of Edinburgh, 1998. Google Scholar
  96. S. MacLane. Categories for the Working Mathematician. Springer-Verlag, 1971. Google Scholar
  97. Roger D. Maddux. Relation algebras. In Chris Brink, Wolfram Kahl, and Gunther Schmidt, editors, Relational Methods in Computer Science, Advances in computing science, pages 22-38. Springer, 1997. URL: https://doi.org/10.1007/978-3-7091-6510-2_2.
  98. Radu Mardare, Prakash Panangaden, and Gordon D. Plotkin. Quantitative algebraic reasoning. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proc. of LICS 2016, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  99. Per Martin-Löf. Constructive mathematics and computer programming. In L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, editors, Logic, Methodology and Philosophy of Science VI, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153-175. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70189-2.
  100. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  101. Ian A. Mason and Carolyn L. Talcott. Equivalence in functional languages with effects. J. Funct. Program., 1(3):287-327, 1991. URL: https://doi.org/10.1017/S0956796800000125.
  102. Conor Mcbride. The derivative of a regular type is its type of one-hole contexts (extended abstract), 2009. Google Scholar
  103. John McCarthy. Towards a mathematical science of computation. In Information Processing, Proceedings of the 2nd IFIP Congress 1962, Munich, Germany, August 27 - September 1, 1962, pages 21-28. North-Holland, 1962. Google Scholar
  104. Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348-375, 1978. URL: https://doi.org/10.1016/0022-0000(78)90014-4.
  105. Robin Milner and Mads Tofte. Co-induction in relational semantics. Theor. Comput. Sci., 87(1):209-220, 1991. URL: https://doi.org/10.1016/0304-3975(91)90033-X.
  106. Robin Milner, Mads Tofte, and Robert Harper. Definition of standard ML. MIT Press, 1990. Google Scholar
  107. J. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, 1969. Google Scholar
  108. M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43(2):223-243, 1942. Google Scholar
  109. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang., 3(ICFP):110:1-110:30, 2019. URL: https://doi.org/10.1145/3341714.
  110. Lorenzo Pace. A relation algebra for term rewriting: A differential approach to sequential reduction (revised version). CoRR, abs/2312.02996, 2023. URL: https://doi.org/10.48550/arXiv.2312.02996.
  111. F. Pfenning. Computation and Deduction. Cambridge University Press, 2016. URL: https://books.google.it/books?id=N6YkPQAACAAJ.
  112. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  113. A. M. Pitts. Applications of sup-lattice enriched category theory to sheaf theory. Proc. London Math. Soc., 57:433-480, 1988. Google Scholar
  114. A.M. Pitts. Howe’s method for higher-order languages. In D. Sangiorgi and J. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge Tracts in Theoretical Computer Science, pages 197-232. Cambridge University Press, 2011. Google Scholar
  115. A.M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  116. Andrew M. Pitts. Some notes on inductive and co-inductive techniques in the semantics of functional programs. Technical Report BRICS-NS-94-5, BRICS, Department of Computer Science, University of Aarhus, December 1994. vi+135 pp, draft version. URL: https://cs.au.dk/~gerth/MC/.
  117. Andrew M. Pitts. Equivariant syntax and semantics. In Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan J. Eidenbenz, and Ricardo Conejo, editors, Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings, volume 2380 of Lecture Notes in Computer Science, pages 32-36. Springer, 2002. URL: https://doi.org/10.1007/3-540-45465-9_3.
  118. Andrew M. Pitts. Alpha-structural recursion and induction. J. ACM, 53(3):459-506, 2006. URL: https://doi.org/10.1145/1147954.1147961.
  119. G.D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  120. G.D. Plotkin. Lcf considered as a programming language. Theoretical Computer Science, 5(3):223-255, 1977. URL: https://doi.org/10.1016/0304-3975(77)90044-5.
  121. Gordon Plotkin. Lambda-definability and logical relations. Technical Report SAI-RM-4, School of A.I., University of Edinburgh, 1973. Google Scholar
  122. Gordon D. Plotkin. A Structural Approach to Operational Semantics. DAIMI FN-19. Computer Science Department, Aarhus University, 1981. Google Scholar
  123. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan J. M. M. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, Cambridge tracts in theoretical computer science, pages 233-289. Cambridge University Press, 2012. Google Scholar
  124. A.J. Power. An abstract formulation for rewrite systems. In D.H. Pitt, D.E. Rydehard, P. Dybjer, A.M. Pitts, and A. Poigné, editors, Category Theory and Computer Science, volume 389, pages 300-312. Springer, 1989. URL: https://doi.org/10.1007/BFB0018358.
  125. Vaughan R. Pratt. Semantical considerations on floyd-hoare logic. In 17th Annual Symposium on Foundations of Computer Science (sfcs 1976), pages 109-121. IEEE, 1976. URL: https://doi.org/10.1109/SFCS.1976.27.
  126. Vaughan R. Pratt. Action logic and pure induction. In Jan van Eijck, editor, Logics in AI, European Workshop, JELIA '90, Amsterdam, The Netherlands, September 10-14, 1990, Proceedings, volume 478 of Lecture Notes in Computer Science, pages 97-120. Springer, 1990. URL: https://doi.org/10.1007/BFb0018436.
  127. Vaughan R. Pratt. Dynamic algebras: Examples, constructions, applications. Stud Logica, 50(3-4):571-605, 1991. URL: https://doi.org/10.1007/BF00370685.
  128. Vaughan R. Pratt. Origins of the calculus of binary relations. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), Santa Cruz, California, USA, June 22-25, 1992, pages 248-254. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/LICS.1992.185537.
  129. Dag Prawitz. Natural Deduction: A Proof-Theoretical Study. Dover Publications, Mineola, N.Y., 1965. Google Scholar
  130. J.C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513-523, 1983. Google Scholar
  131. K.I. Rosenthal. Quantales and their applications. Pitman research notes in mathematics series. Longman Scientific & Technical, 1990. Google Scholar
  132. Davide Sangiorgi. On the proof method for bisimulation (extended abstract). In Proc. of MFCS'95, Lecture Notes in Computer Science, pages 479-488. Springer, 1995. URL: https://doi.org/10.1007/3-540-60246-1_153.
  133. Gunther Schmidt. Relational Mathematics, volume 132 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2011. Google Scholar
  134. Peter Schroeder-Heister. Proof-Theoretic Semantics. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2024 edition, 2024. Google Scholar
  135. P. Selinger. A Survey of Graphical Languages for Monoidal Categories, pages 289-355. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  136. Paul Shields. Charles S. Peirce on the Logic of Number. Docent Press, 2012. Originally a doctoral dissertation, Fordham University, 1981. Google Scholar
  137. M.H.B. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Rapport (Københavns universitet. Datalogisk institut). Datalogisk Institut, Københavns Universitet, 1998. URL: https://books.google.it/books?id=mm73GQAACAAJ.
  138. Allen Stoughton. Substitution revisited. Theoretical Computer Science, 59(3):317-325, 1988. URL: https://doi.org/10.1016/0304-3975(88)90149-1.
  139. Georg Struth. Calculating church-rosser proofs in kleene algebra. In Harrie C. M. de Swart, editor, Proc. of RelMICS 2001, volume 2561 of Lecture Notes in Computer Science, pages 276-290. Springer, 2001. URL: https://doi.org/10.1007/3-540-36280-0_19.
  140. Georg Struth. Abstract abstract reduction. J. Log. Algebraic Methods Program., 66(2):239-270, 2006. URL: https://doi.org/10.1016/j.jlap.2005.04.001.
  141. Masako Takahashi. Parallel reductions in lambda-calculus. Inf. Comput., 118(1):120-127, 1995. URL: https://doi.org/10.1006/INCO.1995.1057.
  142. A. Tarski and S.R. Givant. A Formalization of Set Theory Without Variables. Number v. 41 in A formalization of set theory without variables. American Mathematical Soc., 1988. Google Scholar
  143. Alfred Tarski. On the calculus of relations. J. Symb. Log., 6(3):73-89, 1941. URL: https://doi.org/10.2307/2268577.
  144. Alfred Tarski. What are logical notions? History and Philosophy of Logic, 7(2):143-154, 1986. URL: https://doi.org/10.1080/01445348608837096.
  145. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 280-291. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614955.
  146. Henning Urbat, Stelios Tsampas, Sergey Goncharov, Stefan Milius, and Lutz Schröder. Weak similarity in higher-order mathematical operational semantics. CoRR, abs/2302.08200, 2023. URL: https://doi.org/10.48550/arXiv.2302.08200.
  147. S. Vickers. Topology Via Logic. Cambridge Tracts in Theoretica. Cambridge University Press, 1996. Google Scholar
  148. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, 1994. URL: https://doi.org/10.1006/inco.1994.1093.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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