Research

Journal / Conference Papers

• Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui . A Semantic Account of Metric Preservation.
  In Proceedings of the 41th Symposium on Principles of Programming Languages POPL 2017, To appear, 2017.
  
• Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu . Combining Effects and Coeffects via Grading.
  In Proceedings of the 21th ACM SIGPLAN International Conference on Functional Programming, pp. 476-489, ACM, 2016. (c) ACM. (Paper page)
  
• Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès . Towards a Formal Theory of Graded Monads.
  In Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures 2016, LNCS 9634, pp. 513--530. Springer, Heidelberg, 2016. (c) Springer.
  Abstract: We initiate a formal theory of graded monads whose purpose is to adapt and to extend the formal theory of monads developed by Street in the early 1970's. We establish in particular that every graded monad can be factored in two different ways as a strict action transported along a left adjoint functor. We also explain in what sense the first construction generalizes the Eilenberg-Moore construction while the second construction generalizes the Kleisli construction. Finally, we illustrate the Eilenberg-Moore construction on the graded state monad induced by any object V in a symmetric monoidal closed category~$\Ccategory$.
• Shin-ya Katsumata and Tetsuya Sato. Codensity Liftings of Monads.
  In Proceedings of the 6th Conference on Algebra and Coalgebra in Computer Science, Volume 35 of LIPIcs. (Paper page)
  Abstract: We introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We next study the liftings of algebraic operations to the codensity-lifted monads. We also give a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.
• Shin-ya Katsumata. Parametric Effect Monads and Semantics of Effect Systems.
  In Proceedings of the 41th Symposium on Principles of Programming Languages POPL 2014, pp. 633-645, ACM, 2014. (Paper page,Slides for PPL2014(Japanese))
  Abstract: We study fundamental properties of a generalisation of monad called parametric effect monad, and apply it to the interpretation of general effect systems whose effects have sequential composition operators. We show that parametric effect monads admit analogues of the structures and concepts that exist for monads, such as Kleisli triples, the state monad and the continuation monad, Plotkin and Power's algebraic operations, and the categorical TT-lifting. We also show a systematic method to generate both effects and a parametric effect monad from a monad morphism. Finally, we introduce two effect systems with explicit and implicit subeffecting, and discuss their denotational semantics and the soundness of effect systems.
• Shin-ya Katsumata and Tetsuya Sato. Preorders on Monads and Coalgebraic Simulations.
  In Proceedings of the 16th International Conference on Foundations of Software Science and Computation Structures 2013, LNCS 7794, pp.145--160. Springer, Heidelberg, 2013. (c) Springer. (Paper page,PDF,Corrections)
  Abstract: We study the construction of preorders on Set-monads by the semantic TT-lifting. We show the universal property of this construction, and characterise the class of preorders on a monad as a limit of a Card^op-chain. We apply these theoretical results to identifying preorders on some concrete monads, including the powerset monad, maybe monad, and their composite monad. We also relate the construction of preorders and coalgebraic formulation of simulations.
• Koji Nakazawa and Shin-ya Katsumata. Extensional Models of Untyped Lambda-Mu Calculus.
  In Proceedings of the Fourth International Workshop on Classical Logic and Computation 2012, Electronic Proceedings in Theoretical Computer Science, volume 97, pp. 35-47, 2012. (Paper page)
  
• Shin-ya Katsumata. Relating computational effects by TT-lifting.
  In Information and Computation (Special issue on ICALP 2011), Volume 222, pp. 228-246, 2013. (ScienceDirect,PDF)
  
• Shin-ya Katsumata. Relating Computational Effects by TT-Lifting.
  In Proceedings of the 38th International Colloquium on Automata, Languages and Programming, LNCS 6756, pp. 174-185, 2011. (c) Springer. (Springer,PDF)
  Abstract: We consider the problem of establishing a relationship between two monadic semantics of the $\lambda_c$-calculus extended with algebraic operations. We show that two monadic semantics of any program are related if the relation includes value relations and is closed under the algebraic operations in the $\lambda_c$-calculus.
• Shin-ya Katsumata. Categorical Descriptional Composition.
  In Proceedings of the 8th Asian Symposium on Programming Languages and Systems, LNCS 6461, pp. 222-238, Springer 2010. (c) Springer. (Springer,PDF)
  Abstract: Descriptional composition is a method to fuse two term transformation algorithms described by attribute couplings (AC, attribute grammars over terms) into one. In this article, we provide a general categorical framework for the descriptional composition based on traced symmetric monoidal categories and the Int construction by Joyal et al. We demonstrate that this framework can handle the descriptional composition of SSUR-ACs, nondeterministic SSUR-ACs, quasi-SSUR ACs and quasi-SSUR stack ACs.
• Masahito Hasegawa and Shin-ya Katsumata. A note on the biadjunction between 2-categories of traced monoidal categories and tortile monoidal categories.
  In Mathematical Proceedings of Cambridge Philosophical Society, volume 148, pp. 107-109, 2009. (c) Cambridge Philosophical Society. (PDF)
  
• Shin-ya Katsumata. A Characterisation of Lambda Definability with Sums via TT-Closure Operators.
  In Proceedings of the 17th Annual Conference on Computer Science Logic, LNCS 5213, pp. 278-292. Springer 2008. (c) Springer. (Springer,PDF)
  Abstract: We give a new characterisation of morphisms that are definable by the interpretation of the simply typed lambda calculus with sums in any bi-Cartesian closed category. The TT-closure operator will be used to construct the category in which the collection of definable morphisms at sum types can be characterised as the coproducts of such collections at lower types.
• Shin-ya Katsumata. Attribute Grammars and Categorical Semantics.
  In Proceedings of the 35th International Colloquium on Automata, Languages and Programming, LNCS 5126, pp. 271-282. Springer 2008. (c) Springer. (Springer,PDF)
  Abstract: This is the conference version of the manuscript A New Foundation of Attribute Grammars in Traced Symmetric Monoidal Categories.
• Shin-ya Katsumata and Susumu Nishimura. Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement.
  In Journal of Functional Programming (Special issue on ICFP 2006), volume 18, issue 5-6, pp. 781-819, 2008. (Cambridge Journals)
  Abstract: This is the journal version of the following paper.
• Shin-ya Katsumata and Susumu Nishimura. Algebraic Fusion of Functions with an Accumulating Parameter and Its Improvement.
  In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, pp. 227-238, ACM, 2006. (c) ACM. (author's version in PDF,ACM)
  Abstract: We present a unifying solution to the problem of fusion of functions, where both the producer function and the consumer function have one accumulating parameter. The key idea in this development is to formulate the producer function as a function which computes over a monoid of {\em data context}s. Upon this formulation, we develop a fusion method called {\em algebraic fusion} based on the elementary theory of universal algebra and monoids. The producer function is fused with a monoid homomorphism that is derived from the definition of the consumer function, and is turned into a higher-order function~$f$ that computes over the monoid of endofunctions. We then introduce a general concept called {\em improvement}, in order to reduce the cost of computing over the monoid of endofunctions (i.e., function closures). An improvement of the function $f$ via a monoid homomorphism $h$ is a function $g$ that satisfies $f=h\circ g$. This provides a principled way of finding a first-order function representing a solution to the fusion problem. It also presents a clean and unifying account for varying fusion methods that have been proposed so far. Furthermore, we show that our method extends to support partial and infinite data structures, by means of an appropriate monoid structure. (The trip to the conference was partially supported by Kyoto Daigaku Kyouiku Kenkyuu Shinkou Zaidan.)
• Shin-ya Katsumata. A Semantic Formulation of TT-lifting and Logical Predicates for Computational Metalanguage.
  In Proceedings of the 14th Annual Conference on Computer Science Logic, LNCS 3634, pp. 87-102. Springer 2005. (c) Springer. (PDF)
  Abstract: A semantic formulation of Lindley and Stark's TT-lifting is given. We first illustrate our semantic formulation of the TT-lifting in Sets with several examples, and apply it to the logical predicates for Moggi's computational metalanguage. We then abstract the semantic TT-lifting as the lifting of strong monads across bifibrations with lifted symmetric monoidal closed structures. (This work further develops the example I considered in chapter 4 of my PhD thesis. The trip to the conference was partially supported by Saneyoshi Shogakukai.)
• Shin-ya Katsumata. A Generalisation of Prelogical Predicates to Simply Typed Formal Systems.
  In Proceedings of the 31st International Colloquium on Automata, Languages and Programming, LNCS 3142, pp. 831-845. Springer 2004. (c) Springer. (PDF)
  Abstract: We generalise the notion of prelogical predicates to arbitrary simply typed formal systems and their categorical models. We establish the basic lemma of prelogical predicates and composability of binary prelogical relations in this generalised setting. This generalisation takes place in a framework for typed higher-order abstract syntax and semantics.
• Jo Hannay, Shin-ya Katsumata and Donald Sannella. Semantic and Syntactic Approaches to Simulation Relations.
  In Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science, LNCS 2747, pp. 68-91. Springer 2003. (c) Springer.
  Abstract: Simulation relations are tools for establishing the correctness of data refinement steps. In the simply-typed lambda calculus, logical relations are the standard choice for simulation relations, but they suffer from certain shortcomings; these are resolved by use of the weaker notion of pre-logical relations instead. Developed from a syntactic setting, abstraction barrier-observing simulation relations serve the same purpose, and also handle polymorphic operations. Meanwhile, second-order pre-logical relations directly generalise pre-logical relations to polymorphic lambda calculus (System F). We compile the main refinement-pertinent results of these various notions of simulation relation, and try to raise some issues for aiding their comparison and reconciliation.
• Shin-ya Katsumata. Behavioural equivalence and Indistinguishability in Higher-Order Typed Languages.
  In Proceedings of the 16th International Workshop on Recent Trends in Algebraic Development Techniques, LNCS 2755, pp. 284-298. Springer 2002. (c) Springer. (PDF)
  Abstract: We extend the study of the relationship between behavioural equivalence and indistinguishability relation to the simply typed lambda calculus, where higher-order types are available. The relationship between these two notions is established in terms of factorisability. The main technical tool of this study is pre-logical relations, which give a precise characterisation of behavioural equivalence. We then consider a higher-order logic to reason about models of the simply typed lambda calculus, and relate the resulting standard satisfaction relation to behavioural satisfaction.
• Alan Mycroft, Atsushi Ohori and Shin-ya Katsumata. Comparing Type-Based and Proof-Directed Decompilation.
  In Proceedings of the 8th Working Conference on Reverse Engineering, pp. 362-367. IEEE Press 2001. (c) IEEE.
  Abstract: In the past couple of years interest in decompilation has widened from its initial concentration on reconstruction of control flow into well-founded-in-theory methods to reconstruct type information. Mycroft described Type-Based Decompilation and Katsumata and Ohori described Proof-Directed Decompilation. This note summarises the two approaches and identifies their commonality, strengths and weaknesses; it concludes by suggesting how they may be integrated.
• Shin-ya Katsumata and Atsushi Ohori. Proof-Directed De-compilation of Low-Level Code.
  In Proceedings of the 10th European Symposium on Programming, LNCS 2028, pp. 352-366. Springer 2001. (c) Springer.
  Abstract: We present a proof theoretical method for de-compiling low-level code to the typed lambda calculus. We first define a proof system for a low-level code language based on the idea of Curry-Howard isomorphism. This allows us to regard an executable code as a proof in intuitionistic propositional logic. As being a proof of intuitionistic logic, it can be translated to an equivalent proof of natural deduction proof system. This property yields an algorithm to translate a given code into a lambda term. Moreover, the resulting lambda term is not a trivial encoding of a sequence of primitive instructions, but reflects the behavior of the given program. This process therefore serves as proof-directed de-compilation of a low-level code language to a high-level language. We carry out this development for a subset of Java Virtual Machine instructions including most of its features such as jumps, object creation and method invocation. The proof-directed de-compilation algorithm has been implemented, which demonstrates the feasibility of our approach.

Manuscripts

• Naohiko Hoshino and Shin-ya Katsumata. Int Construction and Semibiproducts. (RIMS-1676)
  Abstract: We study a relationship between the Int construction of Joyal et al. and a weakening of biproducts called semibiproducts. We then provide an application of geometry of interaction interpretation for the multiplicative additive linear logic (MALL for short) of Girard.We consider not biproducts but semibiproducts because in general the Int construction does not preserve biproducts. We show that Int construction is left biadjoint to the forgetful functor from the 2- category of compact closed categories with semibiproducts to the 2-category of traced symmetric monoidal categories with semibiproducts. We then illustrate a traced distributive symmetric monoidal category with biproducts B(Pfn) and relate the interpretation of MALL in Int(B(Pfn)) to token machines defined over weighted MALL proofs.
• Shin-ya Katsumata. A New Foundation of Attribute Grammars in Traced Symmetric Monoidal Categories. (PDF)
  Abstract: In this paper we propose a new categorical formulation of attribute grammars in traced symmetric monoidal categories. The new formulation, called monoidal attribute grammars, concisely captures the essence of the classical attribute grammars. We study monoidal attribute grammars in two categories: Rel^+ and wCPPO. It turns out that in Rel^+ monoidal attribute grammars correspond to the graph-theoretic representation of attribute dependencies, while in wCPPO monoidal attribute grammars are equivalent to Chirica and Martin's K-systems. We also show that in traced symmetric monoidal closed categories every monoidal attribute grammar is equivalent to the one which does not use inherited attributes.

Talks

• Graded monads and the semantics of effect systems.
  QSLC (Quantative Semantics of Logic and Computation) workshop, affiliated workshop of Computer Science Logic 2016, Aix Marseille University, France, 2 Sept, 2016.
• On Graded coalgebras of graded linear exponential comonad.
  CRECOGI (Concurrent, Resourceful and Effectful COmputation, by Geometry of Interaction) workshop, affiliated workshop of Computer Science Logic 2016, Aix-Marseille University, France, 28 Aug, 2016.
• From DCC to local DCC.
  理論計算機科学と圏論ワークショップ CSCAT 2015, 理化学研究所計算科学研究機構, 神戸, 17 Mar, 2016.
• From DCC to local DCC.
  Shonan Meeting on Logic and Verification Methods in Security and Privacy, Shonan Kokusai Village, Kanagawa, 28 Oct, 2015.
• On Graded Monads.
  CRECOGI (Concurrent, Resourceful and Effectful COmputation, by Geometry of Interaction) kickoff workshop, RIMS, Kyoto university, Kyoto, 11 Jul, 2015.
• ファイブレーションと余稠密モナドによるモナドの持ち上げ.
  理論計算機科学と圏論ワークショップ CSCAT 2015, 鹿児島大学, 15 Mar, 2015.
• モナド、代数理論と計算効果.
  Workshop on Programming and Programming Languages, Matsuyama, 4 Mar, 2015.
• Parametric Effect Monads and Semantics of Effect Systems.
  Programming Languages Interest Group, The University of Edinburgh, Edinburgh, 3 Nov, 2014.
• Parametric Effect Monads and Semantics of Effect Systems.
  University of Dundee, Dundee, 30 Oct, 2014.
• Relating Computational Effects by TT-Lifting (invited talk).
  Twelfth International Symposium on Functional and Logic Programming, Ishikawa Prefectural Museum of Art, Kanazawa, Japan, 6 June, 2014.
• Logical Relations for Monads and Categorical TT-Lifting (invited talk).
  Mathematically Structured Functional Programming, Grenoble, France, 12 Apr, 2014.
• Parametric Effect Monads and Semantics of Effect Systems.
  Workshop on Programming and Programming Languages, Aso, 6 Mar, 2014.
• Parametric Effect Monads and Semantics of Effect Systems.
  Institute of Cybernetics at Tallinn University of Technology, Tallinn, Estonia, 28 Nov, 2013.
• Relating Computational Effects by TT-Lifting (invited talk).
  House of the Brotherhood of the Blackheads, Tallinn, Estonia, 21 Nov, 2013.
• Lecture on Categorical Approach to Logic.
  Kisoron Summer School, Keio University, Tokyo, 5 - 8 Aug, 2013.
• A Generic Soundness Result for Effect Systems (Poster).
  Asian Symposium on Programming Languages and Systems, Kyoto, 12 Dec, 2012.
• 効果システムの健全性について (Poster).
  Workshop on Programming and Programming Languages, Shirahama, 9 Mar, 2012.
• A Generic Soundness Result for Effect Systems.
  Logic and Interaction 2012, Marseille, France, 13 Feb, 2012.
• A Categorical Approach to Attribute Grammars.
  ALOCO Seminar on Formal Methods for Component-based Programming, Yaouunde university, Cameroon, 13 Jan, 2012.
• Relating Computational Effects by TT-Lifting.
  Workshop on linear logic (GoI, TSMCs and Implicit Complexity), Kyoto university, 7 Nov, 2011.
• A Categorical Approach to Attribute Grammars.
  Tokyo Programming Seminar, National Institute of Informatics, Tokyo, 23 Jun, 2011.
• Relating Computational Effects by TT-Lifting.
  Adventures of Categories, Research Institute for Mathematical Sciences, Kyoto university, 1 Jun, 2011.
• Relating Computational Effects by TT-Lifting.
  Asian Workshop on Foundations of Software, Shanghai, May, 2011.
• モナド的意味論の比較問題について(ポスター).
  Workshop on Programming and Programming Languages, Sapporo, March, 2011.
• A Gentle Introduction to Denotational Semantics.
  Workshop on Adventures in Categories, Research Institute for Mathematical Sciences, Kyoto university, November, 2010.
• Fullness of Monadic Translation by TT-Lifting.
  LOLA 2010 Syntax and Semantics of Low-Level Languages, Edinburgh university, July, 2010.
• A Categorical Geometory of Interaction for Additives.
  Laboratoire Preuves, Programmes et SystemÈes universitÉ Paris Diderot - Paris 7, March, 2010.
• Logical Predicates for Monads by TT-Lifting.
  Workshop on Category Theory, Computer Science and Topology, Shinshu university, October, 2009.
• Attribute Grammars and Categorical Semantics.
  Workshop on Geometry of Interaction, Traced Monoidal Categories and Implicit Complexity, August, 2009.
• A note on the biadjunction between 2-categories of traced monoidal categories and tortile monoidal categories.
  Workshop on Computer Science and Category Theory, Chiba university, March, 2009.
• Attribute Grammars and Categorical Semantics.
  Workshop on Mathematics for Pressing Problems in Computer Science, Research Institute for Mathematical Sciences, Kyoto university, June, 2008.
• Attribute Grammars and Traced Symmetric Monoidal Categories.
  Workshop on Computer Science and Category Theory, Tohoku university, March, 2008.
• TT-lifting and Logical Predicates for Computational Types.
  Workshop on Computer Science and Category Theory, Kyoto university, March, 2007.
• An Algebraic Approach to Shortcut Fusion of Functions with an Accumulating Parameter.
  Workshop on Programming and Programming Languages, Ogoto, March, 2007.
• An Algebraic Approach to Shortcut Fusion of Functions with an Accumulating Parameter.
  TOPS Seminar, the university of Tokyo, January, 2006.
• Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages.
  Advanced Industrial Science and Technolgy, Amagasaki, August, 2003.

PhD Thesis

MSc Thesis