Realizability Without Symmetry

Author Haruka Tomita

Thumbnail PDF


  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Haruka Tomita
  • Research Institute for Mathematical Sciences, Kyoto University, Japan


I would like to express the deepest appreciation to my supervisor Masahito Hasegawa for a lot of his support, encouragement and advice. Many of his suggestions are incorporated into this paper. I am also grateful to Naohiko Hoshino for helpful discussions and lending his expertise on realizability. I also want to thank Stephen Lack for constructive discussions and comments. Thanks also to anonymous reviewers for variable suggestions and comments.

Cite AsGet BibTex

Haruka Tomita. Realizability Without Symmetry. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


In categorical realizability, it is common to construct categories of assemblies and modest sets from applicative structures. In this paper, we introduce several classes of applicative structures and apply the categorical realizability construction to them. Then we obtain closed multicategories, closed categories and skew closed categories, which are more general categorical structures than Cartesian closed categories and symmetric monoidal closed categories. Moreover, we give the necessary and sufficient conditions for obtaining closed multicategories and closed categories of assemblies.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Realizability
  • combinatory algebra
  • closed multicategory
  • closed category
  • skew closed category


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


  1. Samson Abramsky. Temperley-lieb algebra: from knot theory to logic and computation via quantum mechanics. arXiv preprint arXiv:0910.2737, 2009. Google Scholar
  2. Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625-665, 2002. Google Scholar
  3. Samson Abramsky and Marina Lenisa. A fully complete PER model for ML polymorphic types. In International Workshop on Computer Science Logic, pages 140-155. Springer, 2000. Google Scholar
  4. Valeria de Paiva and Harley Eades. Dialectica categories for the lambek calculus. In International Symposium on Logical Foundations of Computer Science, pages 256-272. Springer, 2018. Google Scholar
  5. Samuel Eilenberg and G Max Kelly. Closed categories. In Proceedings of the Conference on Categorical Algebra, pages 421-562. Springer, 1966. Google Scholar
  6. Masahito Hasegawa. A quantum double construction in Rel. Mathematical Structures in Computer Science, 22(4):618-650, 2012. Google Scholar
  7. J Roger Hindley and Jonathan P Seldin. Lambda-calculus and Combinators, an Introduction, volume 13. Cambridge University Press Cambridge, 2008. Google Scholar
  8. Naohiko Hoshino. Linear realizability. In International Workshop on Computer Science Logic, pages 420-434. Springer, 2007. Google Scholar
  9. Jiaming Jiang, Harley Eades III, and Valeria de Paiva. On the lambek calculus with an exchange modality. arXiv preprint arXiv:1904.06847, 2019. Google Scholar
  10. Yuichi Komori. Syntactical investigations into BI logic and BB'I logic. Studia Logica, 53(3):397-416, 1994. Google Scholar
  11. Joachim Lambek. Deductive systems and categories II. standard constructions and closed categories. In Category theory, homology theory and their applications I, pages 76-122. Springer, 1969. Google Scholar
  12. John R Longley. Realizability toposes and language semantics. PhD thesis, University of Edinburgh, 1995. Google Scholar
  13. Oleksandr Manzyuk. Closed categories vs. closed multicategories. Theory and Applications of Categories, 26(5):132-175, 2012. Google Scholar
  14. Eugenio Moggi. Computational lambda-calculus and monads. Technical report ECS-LFCS-88-66, University of Edinburgh, 1988. Google Scholar
  15. Amr Sabry. Note on axiomatizing the semantics of control operators. Technical report CIS-TR-96-03, Department of Computer Science, University of Oregon, 1996. Google Scholar
  16. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and symbolic computation, 6(3-4):289-360, 1993. Google Scholar
  17. Ross Street. Skew-closed categories. Journal of Pure and Applied Algebra, 217(6):973-988, 2013. Google Scholar
  18. Kornel Szlachányi. Skew-monoidal categories and bialgebroids. Advances in Mathematics, 231(3-4):1694-1730, 2012. Google Scholar
  19. Noam Zeilberger. A theory of linear typings as flows on 3-valent graphs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 919-928. ACM, 2018. Google Scholar
  20. Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal plain lambda terms. Logical Methods in Computer Science, 11(3):1-39, 2015. Google Scholar