Kyoto Univ. > RIMS > Computer Science > People > Hassei's Home Page (English / Japanese)

"Hassei" = Masahito Hasegawa's Research       trace   convolution product

Research Interests Publications PhD Thesis Manuscripts In Japanese People and Places

Research Interests sliding

General
I have been working on semantic models of computation, with particular emphasis on the analysis of programming languages. More specifically, I am using category-theoretic (perhaps better to say "algebraic") tools for studying the semantic aspects of computation arising from programming languages, including the notions of names and variables (my earliest research topic, see "Decomposing Typed Lambda Calculus" (1995)), shared resources, cyclic structures and recursion, as well as computational effects like continuations, and parametric polymorphism.

Action Calculi (1995-1997)
Some of these techniques were successfully applied for clarifying the semantic structure of action calculi, a proposed framework for interactive computation. There are a few joint papers on these results with people in Cambridge and Edinburgh; see "Types and Models for Higher-order Action Calculi" (1997) and "From Action Calculi to Linear Logic" (1998).

Recursion and Traced Monoidal Categories (1995-)
Also I have been developing a new class of models of recursive computation in terms of traced monoidal categories. This work provides a precise connection between cyclic structures and recursive computation, as described in the paper "Recursion from Cyclic Sharing" (1997). You can obtain introductory slides and article on this topic from this page. In "The Uniformity Principle on Traced Monoidal Categories" (2002/2004) some constructions of traced monoidal categories using the uniformity principle are discussed. Some additional observations on traced monoidal closed categories are given in the paper "On Traced Monoidal Closed Categories" (2008) (which is based on a talk at TMCNAA (2007)).

PhD Thesis (1997)
A unified view of my results (up to 1997) is given in my PhD thesis "Models of Sharing Graphs" (1997, Book from Springer 1999), where I present a category-theoretic account of the notion of sharing.

Model Construction Techniques for Linear (and More General) Type Theories (1998-)
Another topic I have been interested in is the model-construction techniques (categorical glueing, also known as logical predicates) for linear type theories - more generally, type theories whose models are described in terms of 2-monads and adjunctions on a suitable 2-category. Progresses in this direction are reported in "Logical Predicates for Intuitionistic Linear Type Theories" (1999) and also in a technical report "Categorical Glueing and Logical Predicates for Models of Linear Logic" (1999). An (entirely syntactic) application of logical predicates is found in a short article "Girard Translation and Logical Predicates" (2000). A manuscript "Glueing Algebraic Structures on a 2-Category" describes a 2-categorical approach on this topic.

Semantics of Call-by-Value: Recursion, Computational Effects, and Linearity (2000-)
I am interested in the semantic aspects of call-by-value programming languages with non-trivial control structures and computational effects. In particular, I worked jointly with Y. Kakutani on the characterization of call-by-value recursion, which is reported in "Axioms for Recursion in Call-by-Value" (2001/2002). This work also offers a semantic account on the relation between recursion and first-class continuations discovered by Filinski. I am also studying the semantic aspects and generalizations of linearly used continuations proposed by Berdine, O'Hearn, Reddy and Thielecke, and a first step towards this direction is described in "Linearly Used Effects" (2002). Largely motivated by this work, I also introduced a simple term calculus for classical linear logic in "Classical Linear Logic of Implications" (2002/2005). Some aspects of the linearly used continuations are also reflected in a joint work with Y. Kameyama on "A Sound and Complete Axiomatization of Delimited Continuations" (2003). An attempt to model linearly used continuations in the call-by-name setting is found in "Semantics of Linear Continuation-Passing in Call-by-Name" (2004).

Relational Parametricity and Computational Effects (2005-)
Experiences on the semantics of computational effects naturally led me to the topic of relational parametricity for computational effects, in particular the case of first-class continuations. Preliminary results about the relational parametricity principle on the second-order lambda-mu calculus (system F with first-class continuations) is reported in "Relational Parametricity and Control" (2005/2006).

[ List of publications from DBLP | AMS MathSciNet ]

line

Publications (Refereed Conference/Journal Papers)

  1. T. Hajgato and M. Hasegawa, Traced *-autonomous categories are compact closed.
    Theory and Applications of Categories 28(7):206-212, April 2013.
    [information] [pdf file]

  2. M. Hasegawa, A quantum double construction in Rel.
    Mathematical Structures in Computer Science 22(4):618-650, August 2012 (published online on 18 May 2012).
    A revised and expanded version of the MFPS2010 paper below.
    [information] [pdf file] © 2012 Cambridge University Press

  3. M. Hasegawa, Bialgebras in Rel.
    In Proc. 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVI), May 2010, Ottawa.
    Electronic Notes in Theoretical Computer Science 265, pages 337-359, September 2010.
    [information] [pdf file (ver. 25 June 2010)] [slides (pdf file)]

  4. M. Hasegawa and S. 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, January 2010 (published online on 5 May 2009).
    [information] [pdf file] © 2009 Cambridge Philosophical Society

  5. K. Nakata and M. Hasegawa, Small-step and big-step semantics for call-by-need.
    Journal of Functional Programming 19(6): 699-722, November 2009 (published online on 7 September 2009).
    [information] [pdf file] © 2009 Cambridge University Press
    [extended version at ArXiv]

  6. M. Hasegawa, On traced monoidal closed categories.
    Mathematical Structures in Computer Science 19(2):217-244, April 2009 (published online on 27 October 2008).
    Based on a talk given at TMCNAA.
    [information] [pdf file] © 2008 Cambridge University Press

  7. M. Hasegawa, M. Hofmann and G. Plotkin, Finite dimensional vector spaces are complete for traced symmetric monoidal categories.
    In Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, Springer LNCS 4800, pages 367-385, February 2008.
    [information] [pdf file] © Springer-Verlag 2008

  8. J.R.B. Cockett, M. Hasegawa and R.A.G. Seely, Coherence of the double involution on *-autonomous categories.
    Theory and Applications of Categories 17(2):17-29, December 2006.
    [information] [pdf file]

  9. M. Hasegawa, Relational parametricity and control.
    Logical Methods in Computer Science 2(3:3):1-22, July 2006.
    Revised and Extended version of the LICS'05 paper.
    [information]

  10. Y. Ohta and M. Hasegawa, A terminating and confluent linear lambda calculus.
    In Proc. 17th International Conference on Rewriting Techniques and Applications (RTA'06), Seattle.
    Springer LNCS 4098, pages 166-180, August 2006.
    [information] [pdf file] © Springer-Verlag 2006

  11. M. Hasegawa, Relational parametricity and control (extended abstract).
    In Proc. 20th Annual IEEE Symposium on Logic in Computer Science (LICS2005), Chicago.
    IEEE Computer Society, pages 72-81, June 2005.
    [information] [pdf file]

  12. M. Hasegawa, Classical linear logic of implications.
    Mathematical Structures in Computer Science 15(2):323-342, April 2005.
    Extended version of the CSL'02 paper.
    [information] [pdf file (ver. June 2004)]

  13. Y. Kakutani and M. Hasegawa, Parameterizations and fixed-point operators on control categories.
    Fundamenta Informaticae 65(1-2): 153-172, March 2005.
    Journal version of the TLCA'03 paper.
    [information] IOS Press

  14. M. Hasegawa, The uniformity principle on traced monoidal categories.
    Publications of the Research Institute for Mathematical Sciences 40(3): 991-1014, September 2004.
    Extended version of the CTCS'02 paper.
    [information] [pdf file]

  15. M. Hasegawa, Semantics of linear continuation-passing in call-by-name.
    In Proc. 7th International Symposium on Functional and Logic Programming (FLOPS2004), Nara.
    Springer LNCS 2998, pages 229-243, April 2004.
    [information] [pdf file] © Springer-Verlag 2004

  16. Y. Kameyama and M. Hasegawa, A sound and complete axiomatization of delimited continuations.
    In Proc. 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala.
    ACM Press, pages 177-188, August 2003.
    [information] [pdf file] © ACM 2003

  17. Y. Kakutani and M. Hasegawa, Parameterizations and fixed-point operators on control categories.
    In Proc. 6th International Conference on Typed Lambda Calculi and Applications (TLCA'03), Valencia.
    Springer LNCS 2701, pages 180-194, June 2003.
    [information] [pdf file] © Springer-Verlag 2003

  18. M. Hasegawa, The uniformity principle on traced monoidal categories.
    In Proc. International Conference on Category Theory and Computer Science (CTCS'02), Ottawa, August 2002.
    Electronic Notes in Theoretical Computer Science 69, pages 137-155, February 2003.
    [information] [gzipped ps file] [pdf file] [pictures from CTCS'02]

  19. M. Hasegawa, Classical linear logic of implications.
    In Proc. 11th Annual Conference of the European Association for Computer Science Logic (CSL'02), Edinburgh.
    Springer LNCS 2471, pages 458-472, September 2002.
    [information] [slides] [gzipped ps file] [pdf file] © Springer-Verlag 2002

  20. M. Hasegawa, Linearly used effects: monadic and CPS transformations into the linear lambda calculus.
    In Proc. 6th International Symposium on Functional and Logic Programming (FLOPS2002), Aizu.
    Springer LNCS 2441, pages 167-182, September 2002.
    [information] [gzipped ps file] [pdf file] © Springer-Verlag 2002

  21. M. Hasegawa and Y. Kakutani, Axioms for recursion in call-by-value.
    Higher-Order and Symbolic Computation 15(2/3):235-264, September 2002.
    Extended version of the FoSSaCS2001 paper.
    [information] [gzipped ps file] [pdf file] © 2002 Kluwer Academic Publishers

  22. M. Hasegawa and Y. Kakutani, Axioms for recursion in call-by-value (extended abstract).
    In Proc. 4th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2001), Genova.
    Springer LNCS 2030, pages 246-260, April 2001. (Here is a picture associated to this paper.)
    Old Version: Preprint RIMS-1288, Kyoto University, July 2000.
    [information] [gzipped ps file] [pdf file] © Springer-Verlag 2001
    For an extended version, see above.

  23. M. Hasegawa, Girard translation and logical predicates.
    Journal of Functional Programming 10(1): 77-89, January 2000.
    [information] [gzipped ps file] [pdf file]

  24. M. Hasegawa, Logical predicates for intuitionistic linear type theories.
    In Proc. 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), L'Aquila.
    Springer LNCS 1581, pages 198-213, April 1999.
    [information] [gzipped ps file] [pdf file] © Springer-Verlag 1999

  25. A. Barber, P. Gardner, M. Hasegawa and G. Plotkin, From action calculi to linear logic.
    In Annual Conference of the European Association for Computer Science Logic (CSL'97), Aarhus, August 1997, Selected Papers.
    Springer LNCS 1414, pages 78-97, 1998.
    [information] [gzipped ps file] [pdf file]

  26. P. Gardner and M. Hasegawa, Types and models for higher-order action calculi.
    In Proc. 3rd International Symposium on Theoretical Aspects of Computer Software (TACS'97), Sendai.
    Springer LNCS 1281, pages 583-603, September 1997.
    [information] [gzipped ps file] [pdf file]

  27. M. Hasegawa, Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi.
    In Proc. 3rd International Conference on Typed Lambda Calculi and Applications (TLCA'97), Nancy.
    Springer LNCS 1210, pages 196-213, April 1997.
    [information] [gzipped ps file] [pdf file]

  28. M. Hasegawa, Decomposing typed lambda calculus into a couple of categorical programming languages.
    In Proc. 6th International Conference on Category Theory and Computer Science (CTCS'95), Cambridge.
    Springer LNCS 953, pages 200-219, August 1995.
    [information] [gzipped ps file] [pdf file]

line

book imagePhD Thesis (Book)

line

MSc Thesis

line

Manuscripts and Slides

line

ALGI-13 Proceedings

An online version of the Proceedings of 13th Seminar on Algebra, Logic and Geometry in Informatics (Kyoto, December 2002) is available here (also from Kyoto Univ Repository).
Printed version: RIMS Kokyuroku 1318, May 2003.

line

Articles and Books in Japanese Japanese

line

Pointers to People, Places, and other Sources

People
Yohji Akama Zena Ariola Robin Cockett Andrzej Filinski
Marcelo Fiore Tsutomu Fujinami Ken-etsu Fujita Carsten Führmann
Philippa Gardner Tatsuya Hagino Esfandiar Hagverdi Martin Hofmann
Ryu Hasegawa Kohei Honda Martin Hyland Bart Jacobs
Alan Jeffrey Yukiyoshi Kameyama Yoshiki Kinoshita Naoki Kobayashi
Paul-Andre Mellies Gordon Plotkin Alex Rabinovich Robert Seely
Peter Selinger Alex Simpson Ross Street Hayo Thielecke
Hideki Tsuiki Hiroshi Watanabe Hongseok Yang Nobuko Yoshida
Places
LFCS (Edinburgh) Computer Laboratory (Cambridge)
DPMMS (Cambridge) Computing Laboratory (Oxford)
Informatics (Sussex) Dept. Computer Science (Queen Mary, U. London)
School of Comp. Sci. (Birmingham) Microsoft (Cambridge)
INRIA PPS (Paris)
BRICS (Aarhus)
SFC (Fujisawa, Keio Univ) Dept. Information Science (Univ. Tokyo)
JAIST (Ishikawa) Research Center for Verification and Semantics (AIST)
Sources
TLCA Home Page RTA Home Page
The Types Forum Categories Home Page
American Mathematical Society Abbreviations of Names of Serials (AMS)
Assocication for Computing Machinery Research Index (Computer Science)
ACM Digital Library IEEE Digital Library
Standard ML of New Jersey Haskell Home Page
Theoretical Computer Science (Elsevier) Information and Computation (Elsevier)
Mathematical Structures in Computer Science (CUP) Journal of Functional Programming (CUP)
Lecture Notes in Computer Science (Springer) Higher-Order and Symbolic Computation (Springer)
Logical Methods in Computer Science

line

Masahito Hasegawa / hassei at kurims.kyoto-u.ac.jp