Computer Science Team, Research Institute for Mathematical SciencesKyoto University

• Kazushige Terui. Can a computer be a mathematician? From foundations of mathematics to the theory of proofs and programs (in Japanese).
  Seidosha, 2015.

• Shin-ya Katsumata. Parametric Effect Monads and Semantics of Effect Systems.
  In Proc. POPL '14,pp. 633-645, ACM, 2014.


• Tetsuya Sato. Identifying All Preorders on the Subdistribution Monad.
  Electronic Notes in Theoretical Computer Science 308,pp 309-327, 2014.


• Naohiko Hoshino, Koko Muroya and Ichiro Hasuo. Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects.
  In Proceedings of CSL-LICS 2014.

• Shin-ya Katsumata and Tetsuya Sato. Preorders on Monads and Coalgebraic Simulations.
  In Proc. FoSSaCS '13, LNCS 7794,pp.145--160. Springer, Heidelberg, 2013. (c) Springer


• Masahito Hasegawa (Ed.). Typed Lambda Calculi and Applications: TLCA 2013, Proceedings.
  Springer LNCS 7941, 2013.


• Tamas Hajgato and Masahito Hasegawa. Traced *-autonomous categories are compact closed.
  Theory and Applications of Categories 28(7):206-212, 2013.


• Kenshi Miyabe. L1-computability, layerwise computability and Solovay reducibility.
  to appear in Computability.


• Kenshi Miyabe and Akimichi Takemura. The law of the iterated logarithm in game-theoretic probability with quadratic and stronger hedges.
  to appear in Stochastic Processes and their Applications.


• Kenshi Miyabe and Jason Rute. Van Lambalgen's Theorem for uniformly relative Schnorr and computable randomness
  to appear in Proceedings of the Twelfth Asian Logic Conference.


• Kenshi Miyabe An optimal superfarthingale and its convergence over a computable topological space.
  to appear in Lecture Notes in Artificial Intelligence.


• Kenshi Miyabe. Characterizing randomness of Kurtz randomness by a differentiation theorem.
  Theory of Computing Systems, 52(1):113-132, 2013.

• Masahito Hasegawa. A quantum double construction in Rel.
  Mathematical Structures in Computer Science 22(4):618-650, 2012.


• Norihiro Tsumagari. Probabilistic Relational Models of Complete IL-semirings.
  Bulletin of Informatics and Cybernetics, vol.44, pp.87--109, 2012.


• Kazushige Terui. Semantic evaluation, intersection types and complexity of simply typed lambda calculus.
  In Proceedings of RTA'12, pp. 323-338, 2012.


• Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Algebraic proof theory for substructural logics: Cut-elimination and completions.
  Annals of Pure and Applied Logic, Vol. 163, No. 3, pp. 266-290, 2012.


• Kenshi Miyabe and Akimichi Takemura. Convergence of random series and the rate of convergence of the strong law of large numbers in game-theoretic probability, .
  Stochastic Processes and their Applications, 122:1-30, 2012.


• Kenshi Miyabe The difference between optimality and universality, .
  Logic Journal of the IGPL, 20(1):222-234, 2012.


• Naohiko Hoshino. Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects..
  In Proceedings of LICS 2012.


• Naohiko Hoshino. A Representation Theorem for Unique Decomposition Categories..
  In Proceedings of MFPS 2012.


• Koji Nakazawa and Shin-ya Katsumata. Extensional Models of Untyped Lambda-Mu Calculus..
  In Proc. Fourth International Workshop on Classical Logic andComputation 2012, To appear.


• Takanori Hida. A Computational Interpretation of the Axiom of Determinacy in Arithmetic.
  In proceedings of CSL 2012, LIPICS vol.16, pp 335-349, Dagstuhl Publishing.

• Kazushige Terui. Computational ludics.
  Theoretical Computer Science, Vol. 412, No. 20, pp. 2048-2071, 2011.


• Rostislav Horcik and Kazushige Terui. Disjunction property and complexity of substructural logics.
  Theoretical Computer Science, Vol. 412, No. 31, pp. 3992-4006, 2011.


• Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. Macneille completions of FL-algebras.
  Algebra Universalis, Vol. 66, No. 4, pp. 405-420, 2011.


• Ichiro Hasuo and Naohiko Hoshino. Semantics of Higher-Order QuantumComputation via Geometry of Interaction.
  In Proceedings of LICS 2011, page 237-246, IEEE Computer Society.


• 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.


• Naohiko Hoshino. A modified GoI interpretation for a linear functional programming language and its adequacy.
  In proceedings of FoSSaCS 2011, LNCS 6604, pp 340-334, Springer.

• Ichiro Hasuo and Bart Jacobs. Traces for Coalgebraic Components.
  To appear in Mathematical Structures in Computer Science.
  


• Kenshi Miyabe An extension of van Lambalgen's Theorem to infinitely many relative 1-random reals.
  Notre Dame Journal of Formal Logic, 51(3):337-349, 2010.


• Masahito Hasegawa. Bialgebras in Rel.
  Proc. Mathematical Foundations of Programming Semantics (MFPS XXVI),Electr. Notes Comp. Sci. 265, 337-359, 2010.


• Shin-ya Katsumata. Categorical Descriptional Composition.
  In Proc. APLAS 2010, LNCS 6461, pp.222-238, Springer 2010. (Springer)


• Rostislav Horcik and Kazushige Terui. Disjunction Property and Complexity of Substructural Logics.
  To appear in Theoretical Computer Science.


• Michele Basaldella, Alexis Saurin and Kazushige Terui. From focalization of logic to the logic of focalization.
  In Proceedings of MFPS' 10, ETCS 265 pp. 161-176, 2010.


• Michele Basaldella and Kazushige Terui. Infinitary completeness in ludics.
  In Proceedings of LICS' 10, pp. 294-303, 2010.


• Michele Basaldella and Kazushige Terui. On the meaning of logical completeness.
  Logical Methods in Computer Science 6(4:11), 2010.


• Kazuyuki Asada and Ichiro Hasuo. Categorifying Computations into Components via Arrows as Profunctors.
  Proc. Coalgebraic Methods Comp. Sci. (CMCS 2010), Electr. Notes Comp. Sci. 264(2):25-45, 2010.
  


• Alois Brunel and Kazushige Terui. Church => Scott = Ptime: an application of resource-sensitive realizability.
  Proceedings of International Workshop on Developments in Implicit Computational Complexity, EPTCS 23, pp.31-46, 2010..
  


• Masahito Hasegawa and Shin-ya Katsumata, A note on the biadjunction between 2-categories of traced monoidal categories and tortile monoidal categories.
  Mathematical Proceedings of the Cambridge Philosophical Society 148(1): 107-109, 2010.


• Ichiro Hasuo. Generic Forward and Backward Simulations II: Probabilistic Simulation.
  Proc. CONCUR 2010, LNCS 6269, p. 447-461. Springer-Verlag.
  


• Ichiro Hasuo, Bart Jacobs and Milad Niqui. Coalgebraic Representation Theory of Fractals.
  Proc. MFPS XXVI, Electr. Notes Comp. Sci. 265:351-368.
  


• Ichiro Hasuo, Yoshinobu Kawabe and Hideki Sakurada. Probabilistic Anonymity via Coalgebraic Simulations.
  Theoretical Computer Science, 411(22-24):2239-2259, 2010.
  


• Kenshi Miyabe. Truth-table Schnorr randomness and truth-table reducibly randomness.
  To appear in Mathematical Logic Quarterly.
  

• Michele Basaldella and Claudia Faggian. Ludics with repetitions: Exponentials, Interactive Types and Completeness..In Proceedings of LICS' 09, pp. 375-384, 2009.


• Patrick Baillot and Kazushige Terui. Light types for polynomial time computation in lambda calculus.
  Information and Computation, Vol. 207, No. 1, pp. 41-62, 2009.
  


• Michele Basaldella and Kazushige Terui. On the meaning of logical completeness.
  In Proceedings of TLCA'09, LNCS 5608 pp. 50-64, 2009.
  


• Agata Ciabattoni, Lutz Strassburger and Kazushige Terui. Expanding the realm of systematic proof theory.
  In Proceedings of CSL'09, pp. 163-178, 2009.
  


• Masahito Hasegawa, On traced monoidal closed categories.
  Mathematical Structures in Computer Science, 19(2):217-244, 2009.


• Ichiro Hasuo, Chris Heunen, Bart Jacobs and Ana Sokolova, Coalgebraic Components in a Many-Sorted Microcosm.
  In Proc. Conference on Algebra and Coalgebra in Computer Science (CALCO 2009), Springer LNCS.


• Bart Jacobs and Ichiro Hasuo. Semantics and logic for security protocols.
  Journal of Computer Security, 17(6):909-944, 2009.


• Bart Jacobs, Chris Heunen and Ichiro Hasuo, Categorical Semantics for arrows.
  Journal of Functional Programming, 19(3-4):403-438, 2009.


• Keiko Nakata and Masahito Hasegawa. Small-step and big-step semantics for call-by-need.
  Journal of Functional Programming 19(6): 699-722, 2009.
  

• Kazuyuki Asada. Extensional universal types for call-by-value.
  In Proc. ASIAN Symposium on Programming Languages and Systems (APLAS 2008), Springer LNCS 5356.


• Agata Ciabattoni, Nikolaos Galatos and Kazushige Terui. From axioms to analytic rules in nonclassical logics.
  In Proc. Logic in Computer Science (LICS'08).


• J.R.B. Cockett and Craig Pastro. The logic of message passing.
  To appear in Science of Computer Programming


• Brian Day and Craig Pastro. Note on Frobenius monoidal functors.
  New York Journal of Mathematics 14, 733-742.


• Masahito Hasegawa, Martin Hofmann and Gordon Plotkin, Finite dimensional vector spaces are complete for traced symmetric monoidal categories.
  In Festschrift in Honor of Boaz Trakhtenbrot, Springer LNCS 4800.


• Ichiro Hasuo, Bart Jacobs and Ana Sokolova, The microcosm principle and concurrency in coalgebra.
  In Proc. Foundations of Software Science and Computation Structures(FoSSaCS 2008), Springer LNCS 4962.


• Shin-ya Katsumata, Attribute grammars and categorical semantics.
  InProc. International Colloquium on Automata, Languages and Programming(ICALP'08), Springer LNCS 5126.


• Shin-ya Katsumata, A characterisation of lambda definability with sums via TT-closure operators.
  In Proc. Computer Science Logic (CSL'08), Springer LNCS.


• Shin-ya Katsumata and Susumu Nishimura, Algebraic fusion of functions with an accumulating parameter and its improvement.
  To appear in Journal of Functional Programming.



• Craig Pastro and Ross Street. Closed categories, star-autonomy, and monoidal comonads.
  To appear in Journal of Algebra.


• Craig Pastro and Ross Street. Weak Hopf monoids in braided monoidal categories.
  To appear in Algebra and Number Theory

• Ichiro Hasuo, Bart Jacobs and Ana Sokolova, Generic trace semantics via coinduction.
  Logical Methods in Computer Science, 3(4:11):1-36, 2007.

• Ichiro Hasuo, Bart Jacobs and Tarmo Uustalu, Categorical views on computations on trees.
  In Proc. International Colloquium on Automata, Languages and Programming (ICALP'07), Springer LNCS 4596.

• Naohiko Hoshino, Linear realizability.
  In Proc. Computer Science Logic (CSL'07), Springer LNCS 4646.

• Robin Cockett, Masahito Hasegawa and Robert Seely, Coherence of the double involution on *-autonomous categories.
  Theory and Applications of Categories, 17(2):17-29, 2006.

• Masahito Hasegawa, Relational parametricity and control.
  Logical Methods in Computer Science, 2(3:3):1-22, 2006.

• Shin-ya Katsumata and Susumu Nishimura, Algebraic fusion of functions with an accumulating parameter and its improvement.
  In Proc. International Conference on Functional Programming (ICFP 2006).

• Keiko Nakata and Jacques Garrigue, Recursive modules for programming.
  In Proc. International Conference on Functional Programming (ICFP 2006).

• Yo Ohta and Masahito Hasegawa, A terminating and confluent linear lambda calculus.
  In Proc. Rewriting Techniques and Applications (RTA'06), Springer LNCS 4098.

• Masahito Hasegawa, Classical linear logic of implications.
  Mathematical Structures in Computer Science, 15(2):323-342, 2005.

• Masahito Hasegawa, Relational parametricity and control (extended abstract).
  In Proc. Logic in Computer Science (LICS'05).

• Yoshihiko Kakutani and Masahito Hasegawa, Parameterizations and fixed-point operators on control categories.
  Fundamenta Informaticae, 65(1-2):153-172, 2005.

• Shin-ya Katsumata, A semantic formulation of TT-lifting and logical predicates for computational metalanguage.
  In Proc. Computer Science Logic (CSL'05), Springer LNCS 3641.

• Keiko Nakata, Akira Ito and Jacques Garrigue, Recursive object-oriented modules.
  In Proc. International Workshop on Foundations of Object-Oriented Languages (FOOL 12).

• Nobuaki Yoshida, Yoshio Hayashi, Yutaka Tamagaki, Shoji Urashita, Makoto Kakuta, Masahiro Watanabe, Jacques Garrigue, Reiji Nakajima, SOBA framework: an application framework for broadband network environment.
  In Proc. IEEE/IPSJ International Symposium on Applications and the Internet (SAINT 2005).

• Jacques Garrigue, Relaxing the value restriction.
  In Proc. Functional and Logic Programming (FLOPS2004), Springer LNCS 2998.

• Masahito Hasegawa, Semantics of linear continuation-passing in call-by-name.
  In Proc. Functional and Logic Programming (FLOPS2004), Springer LNCS 2998.

• Masahito Hasegawa, The uniformity principle on traced monoidal categories.
  Publications of RIMS, 40(3): 991-1014, 2004.

• Shin-ya Katsumata, A generalisation of prelogical predicates to simply typed formal systems.
  In Proc. International Colloquium on Automata, Languages and Programming (ICALP'04), Springer LNCS 3142.

• Masahito Hasegawa, The uniformity principle on traced monoidal categories.
  In Proc. Category Theory and Computer Science (CTCS'02), Electronic Notes in Theoretical Computer Science 69.

• Haruo Hosoya and Benjamin C. Pierce, XDuce: A statically typed XML processing language.
  ACM Transactions on Internet Technology, 3(2):117-148, 2003.

• Yoshihiko Kakutani and Masahito Hasegawa, Parameterizations and fixed-point operators on control categories.
  In Proc. Typed Lambda Calculi and Applications (TLCA'03), Springer LNCS 2701.

• Yukiyoshi Kameyama and Masahito Hasegawa, A sound and complete axiomatization of delimited continuations.
  In Proc. International Conference on Functional Programming (ICFP 2003).

• Susumu Nishimura, Correctness of a higher-order removal transformation through a relational reasoning.
  In Proc. Asian Symposium on Programming Languages and Systems (APLAS'03), Springer LNCS 2895.

• Jacques Garrigue, Simple type inference for structural polymorphism.
  In Proc. International Workshop on Foundations of Object-Oriented Languages (FOOL 9).

• Masahito Hasegawa, Linearly used effects: monadic and CPS transformations into the linear lambda calculus.
  In Proc. Functional and Logic Programming (FLOPS2002), Springer LNCS 2441.

• Masahito Hasegawa, Classical linear logic of implications.
  In Proc. Computer Science Logic (CSL'02), Springer LNCS 2471.

• Masahito Hasegawa and Yoshihiko Kakutani, Axioms for recursion in call-by-value.
  Higher-Order and Symbolic Computation, 15(2/3):235-264, 2002.

• Haruo Hosoya and Makoto Murata, Validation and boolean operations for attribute-element constraints.
  In Proc. Programming Languages Technologies for XML (PLAN-X).

• Yoshihiko Kakutani, Duality between call-by-name recursion and call-by-value iteration.
  In Proc. Computer Science Logic (CSL'02), Springer LNCS 2471.

• Masahito Hasegawa and Yoshihiko Kakutani, Axioms for recursion in call-by-value (extended abstract).
  In Proc. Foundations of Software Science and Computation Structures (FoSSaCS 2001), Springer LNCS 2030.

• Shin-ya Katsumata and Atsushi Ohori, Proof-directed de-compilation of low-level code.
  In Proc. European Symposium on Programming (ESOP 2001), Springer LNCS 2028.

• Keisuke Nakano and Susumu Nishimura, Deriving event-based document transformers from tree-based specifications.
  In Proc. Workshop on Language Descriptions, Tools and Applications (LDTA 2001), Electronic Notes in Theoretical Computer Science 44(2).

• Masahito Hasegawa, Girard translation and logical predicates.
  Journal of Functional Programming, 10(1): 77-89, 2000.

• Martin Müller and Susumu Nishimura, Type inference for first-class messages with feature constraints.
  International Journal of Foundations of Computer Science, 11(1): 29-63, 2000.

• Matthias Blume, Dependency analysis for Standard ML.
  ACM Transactions on Programming Languages and Systems, 21(4):790-812, 1999.

• Matthias Blume and Andrew W. Appel, Hierarchical modularity.
  ACM Transactions on Programming Languages and Systems, 21(4):813-847, 1999.

• Jacques Garrigue and Didier Remy, Semi-explicit first-class polymorphism for ML.
  Journal of Information and Computation, 155:134-169, 1999.

• Masahito Hasegawa, Logical predicates for intuitionistic linear type theories.
  In Proc. Typed Lambda Calculi and Applications (TLCA'99), Springer LNCS 1581.

• Masahito Hasegawa, Models of Sharing Graphs: A Categorical Semantics of let and letrec.
  Distinguished Dissertation Series, Springer-Verlag, 1999.

• Susumu Nishimura and Atsushi Ohori, Parallel functional programming via data-parallel recursion.
  Journal of Functional Programming, 9(4):427-462, 1999.

• Atsushi Ohori, A Curry-Howard isomorphism for compilation and program execution.
  In Proc. Typed Lambda Calculi and Applications (TLCA'99), Springer LNCS 1581.

• Atsushi Ohori, The logical abstract machine: a Curry-Howard isomorphism for machine code.
  In Proc. Fuji International Symposium on Functional and Logic Programming (FLOPS'99) (invited paper), Springer LNCS 1722.

• Atsushi Ohori, Type-directed specialization of polymorphism.
  Journal of Information and Computation, 155:64-107, 1999.

• Atsushi Ohori and Nobuaki Yoshida, Type inference with rank 1 polymorphism for type-directed compilation of ML.
  In Proc. International Conference on Functional Programming (ICFP'99).

• Andrew Barber, Philippa Gardner, Masahito Hasegawa and Gordon Plotkin, From action calculi to linear logic.
  In Computer Science Logic (CSL'97), Selected Papers, Springer LNCS 1414.

• Jacques Garrigue, Programming with polymorphic variants.
  In Proc. ML Workshop '98.

• Jacques Garrigue and Yasuhiko Minamide, On the runtime complexity of type-directed unboxing.
  In Proc. International Conference on Functional Programming (ICFP'98).

• Masatomo Hashimoto, First-class contexts in ML.
  In Proc. ASIAN Computing Science Conference (ASIAN 98), Springer LNCS 1538.

• Yasuhiko Minamide, A functional represention of data structures with a hole.
  In Proc. 25th Symposium on Principles of Programming Languages (POPL'98).

• Martin Müller and Susumu Nishimura, Type inference for first-class messages with feature constraints.
  In Proc. ASIAN Computing Science Conference (ASIAN 98), Springer LNCS 1538.

• Susumu Nishimura, Static typing for dynamic messages.
  In Proc. 25th Symposium on Principles of Programming Languages (POPL'98).

• Patrick Viry, A user-interface for Knuth-Bendix completion.
  In Proc. 4th Workshop on User Interfaces for Theorem Provers (UITP'98).

• Patrick Viry, Adventures in sequent calculus modulo equations.
  In Proc. 2nd Workshop on Rewriting Logic and its Applications (WRLA'98), Electronic Notes in Theoretical Computer Science 15.

• Philippa Gardner and Masahito Hasegawa, Types and models for higher-order action calculi.
  In Proc. Theoretical Aspects of Computer Software (TACS'97), Springer LNCS 1281.

• Jacques Garrigue and Didier Remy, Extending ML with semi-explicit higher order polymorphism.
  In Proc. Theoretical Aspects of Computer Software (TACS'97), Springer LNCS 1281.

• Susumu Nishimura, A strict functional language with cyclic recursive data.
  Formal Aspects of Computing, 9(1):78-97, 1997.

• Atsushi Ohori, Type system for specializing polymorphism.
  In Proc. Theoretical Aspects of Computer Software (TACS'97) (invited paper), Springer LNCS 1281.

• Atsushi Ohori and Tomonobu Takamizawa, An unboxed operational semantics for ML polymorphism.
  Journal of Lisp and Symbolic Computation, 10(1):61 - 91, 1997.

• Makoto Tanabe, Timed petri nets and temporal linear logic.
  In Proc. Application and Theory of Petri Nets (ICATPN '97), Springer LNCS 1238.

• Peter Buneman and Atsushi Ohori, Polymorphism and type inference in database programming.
  ACM Transactions on Database Systems, 21(1):30-76, 1996.

• Yasuhiko Minamide, Greg Morrisett and Robert Harper, Typed closure conversion.
  In Proc. 23rd Symposium on Principles of Programming Languages (POPL'96).

• Yasuhiko Minamide, Compilation based on a calculus for explicit type passing.
  In Proc. 2nd Fuji International Workshop on Functional and Logic Programming (FLOPS'96).

• Susumu Nishimura, Integrating different versions of programs with backward and forward slices.
  Science of Computer Programming, 27(1):1-35, 1996.

• Susumu Nishimura, Atsushi Ohori and Keishi Tajima, An equational object-oriented data model and its data-parallel query language.
  In Proc. ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA'96).

Research Institute for Mathematical Sciences, Kyoto University, 606-8502 Japan.