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