Document Open Access Logo

Modules over Monads and Operational Semantics

Authors André Hirschowitz, Tom Hirschowitz, Ambroise Lafont

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2020.12.pdf
  • Filesize: 0.68 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Categorical semantics
  • Theory of computation → Operational semantics
Keywords
  • Operational semantics
  • Category theory

Metrics

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

Abstract

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as  ̅λμ-calculus, π-calculus, Positive GSOS specifications, differential λ-calculus, and the big-step, simply-typed, call-by-value λ-calculus. Finally, we design a suitable notion of signature for transition monads.

Cite As Get BibTex

André Hirschowitz, Tom Hirschowitz, and Ambroise Lafont. Modules over Monads and Operational Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.12

Author Details

André Hirschowitz
  • Université Côte d’Azur, CNRS, Nice, France
Tom Hirschowitz
  • Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, France
Ambroise Lafont
  • University of New South Wales, Sydney, Australia

Acknowledgements

We thank the anonymous referees for their constructive comments.

References

  1. Benedikt Ahrens. Modules over relative monads for syntax and semantics. MSCS, 26:3-37, 2016. Google Scholar
  2. Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular specification of monads through higher-order presentations. In Herman Geuvers, editor, Proc. 4th Int. Conf. on Formal Structures for Comp. and Deduction, LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  3. Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Reduction monads and their signatures. PACMPL, 4(POPL):31:1-31:29, 2020. URL: http://dx.doi.org/10.1145/3371099.
  4. Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. Logical Methods in Computer Science, 11(1), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(1:3)2015.
  5. Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, and Anton Setzer. A categorical semantics for inductive-inductive definitions. In Andrea Corradini, Bartek Klin, and Corina Cîrstea, editors, Proc. 4th Alg. and Coalgebra in Comp. Sci., volume 6859 of LNCS, pages 70-84. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22944-2_6.
  6. Falk Bartels. GSOS for probabilistic transition systems: (extended abstract). Electronic Notes in Theoretical Computer Science, 65(1):29-53, 2002. CMCS '2002, Coalgebraic Methods in Computer Science. URL: http://dx.doi.org/10.1016/S1571-0661(04)80358-X.
  7. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, 1995. URL: http://dx.doi.org/10.1145/200836.200876.
  8. Peio Borthelle, Tom Hirschowitz, and Ambroise Lafont. A cellular Howe theorem. In Proc. 35th ACM/IEEE Logic in Comp. Sci. ACM, 2020. URL: http://dx.doi.org/10.1145/3373718.3394738.
  9. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. TCS, 309:1-41, 2003. Google Scholar
  10. M. P. Fiore and C.-K. Hur. Second-order equational logic. In Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), 2010. Google Scholar
  11. Marcelo Fiore and Chung-Kil Hur. On the construction of free algebras for equational systems. TCS, 410:1704-1729, 2009. Google Scholar
  12. Marcelo P. Fiore. Second-order and dependently-sorted abstract syntax. In Proc. 23rd Logic in Comp. Sci., pages 57-68. IEEE, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.38.
  13. Marcelo P. Fiore and Sam Staton. A congruence rule format for name-passing process calculi from mathematical structural operational semantics. In Proc. 21st Logic in Comp. Sci., pages 49-58. IEEE, 2006. URL: http://dx.doi.org/10.1109/LICS.2006.7.
  14. Marcelo P. Fiore and Daniele Turi. Semantics of name and value passing. In Proc. 16th Logic in Comp. Sci., pages 93-104. IEEE, 2001. URL: http://dx.doi.org/10.1109/LICS.2001.932486.
  15. Richard Garner. Combinatorial structure of type dependency. Journal of Pure and Applied Algebra, 219(6):1885 - 1914, 2015. URL: http://dx.doi.org/10.1016/j.jpaa.2014.07.015.
  16. Makoto Hamana. Term rewriting with variable binding: An initial algebra approach. In Proc. 5th Princ. and Practice of Decl. Prog. ACM, 2003. URL: http://dx.doi.org/10.1145/888251.888266.
  17. Hugo Herbelin. Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes. PhD thesis, Paris Diderot University, France, 1995. URL: https://tel.archives-ouvertes.fr/tel-00382528.
  18. André Hirschowitz and Marco Maggesi. Modules over monads and linearity. In WoLLIC, volume 4576 of LNCS, pages 218-237. Springer, 2007. URL: http://dx.doi.org/10.1007/3-540-44802-0_3.
  19. Tom Hirschowitz. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. LMCS, 9(3), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(3:10)2013.
  20. Ambroise Lafont. Signatures and models for syntax and operational semantics in the presence of variable binding. PhD thesis, École Nationale Superieure Mines - Telecom Atlantique Bretagne Pays de la Loire - IMT Atlantique, 2019. URL: https://arxiv.org/abs/1910.09162v2.
  21. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO - Theor. Inf. and Applic., 33(6):507-534, 1999. URL: http://dx.doi.org/10.1051/ita:1999130.
  22. Jan Reiterman. A left adjoint construction related to free triples. JPAA, 10:57-71, 1977. Google Scholar
  23. Davide Sangiorgi and David Walker. The π-calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  24. Sam Staton. General structural operational semantics through categorical logic. In Proc. 23rd Logic in Comp. Sci., pages 166-177. IEEE, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.43.
  25. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proc. 12th Logic in Comp. Sci., pages 280-291, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614955.
  26. Lionel Vaux. λ-calcul différentiel et logique classique : interactions calculatoires. PhD thesis, Université Aix-Marseille 2, 2007. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact