General
I have been working on
semantic models of computation,
with particular emphasis on the analysis of
programming languages.
More specifically, I am using categorytheoretic
(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 (19951997)
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 Higherorder 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 categorytheoretic
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
modelconstruction techniques
(categorical glueing,
also known as logical predicates)
for linear type theories
 more generally, type theories whose models are described in terms of
2monads and adjunctions on a suitable 2category.
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
2Category" describes a 2categorical approach
on this topic.
Semantics of CallbyValue: Recursion,
Computational Effects, and Linearity (2000)
I am interested in the semantic aspects of
callbyvalue programming languages
with nontrivial control structures
and computational effects.
In particular, I worked jointly with Y. Kakutani
on the characterization of
callbyvalue recursion,
which is reported in
"Axioms for Recursion in CallbyValue"
(2001/2002). This work also offers
a semantic account on the relation between
recursion and firstclass 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 callbyname setting is found in
"Semantics of Linear ContinuationPassing in
CallbyName" (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 firstclass continuations.
Preliminary results about the relational parametricity principle on
the secondorder lambdamu calculus (system F with firstclass continuations)
is reported in
"Relational Parametricity and Control"
(2005/2006).
[
List of publications from DBLP 
AMS MathSciNet
]
 T. Hajgato and M. Hasegawa,
Traced *autonomous categories are compact closed.
Theory and Applications of Categories 28(7):206212, April 2013.
[information]
[pdf file]
 M. Hasegawa,
A quantum double construction in Rel.
Mathematical Structures in Computer Science 22(4):618650, 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
 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 337359, September 2010.
[information]
[pdf file (ver. 25 June 2010)]
[slides (pdf file)]

M. Hasegawa and S. Katsumata,
A note on the biadjunction between 2categories of
traced monoidal categories and tortile monoidal categories.
Mathematical Proceedings of the Cambridge Philosophical Society,
148(1): 107109, January 2010 (published online on 5 May 2009).
[information]
[pdf file]
© 2009 Cambridge Philosophical Society

K. Nakata and M. Hasegawa,
Smallstep and bigstep semantics for callbyneed.
Journal of Functional Programming 19(6): 699722, November 2009 (published online on 7 September 2009).
[information]
[pdf file]
© 2009 Cambridge University Press
[extended version at ArXiv]

M. Hasegawa,
On traced monoidal closed categories.
Mathematical Structures in Computer Science 19(2):217244, April 2009
(published online on 27 October 2008).
Based on a talk given at TMCNAA.
[information]
[pdf file]
© 2008 Cambridge University Press
 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 367385, February 2008.
[information]
[pdf file]
© SpringerVerlag 2008
 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):1729, December 2006.
[information]
[pdf file]
 M. Hasegawa,
Relational parametricity and control.
Logical Methods in Computer Science
2(3:3):122, July 2006.
Revised and Extended version of the LICS'05 paper.
[information]
 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 166180, August 2006.
[information]
[pdf file]
© SpringerVerlag 2006
 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 7281, June 2005.
[information]
[pdf file]
 M. Hasegawa,
Classical linear logic of implications.
Mathematical
Structures in Computer Science 15(2):323342, April 2005.
Extended version of the CSL'02 paper.
[information]
[pdf file (ver. June 2004)]
 Y. Kakutani and M. Hasegawa,
Parameterizations and fixedpoint operators on control categories.
Fundamenta Informaticae
65(12): 153172, March 2005.
Journal version of the TLCA'03 paper.
[information]
IOS Press
 M. Hasegawa,
The uniformity principle on traced monoidal categories.
Publications of the
Research Institute for Mathematical Sciences 40(3): 9911014,
September 2004.
Extended version of the CTCS'02 paper.
[information]
[pdf file]
 M. Hasegawa,
Semantics of linear continuationpassing in callbyname.
In
Proc. 7th
International Symposium on Functional and Logic Programming
(FLOPS2004), Nara.
Springer
LNCS 2998, pages 229243, April 2004.
[information]
[pdf file]
© SpringerVerlag 2004
 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 177188, August 2003.
[information]
[pdf file]
© ACM 2003
 Y. Kakutani and M. Hasegawa,
Parameterizations and fixedpoint operators on control categories.
In
Proc. 6th
International Conference on
Typed Lambda Calculi and Applications
(TLCA'03), Valencia.
Springer
LNCS 2701, pages 180194, June 2003.
[information]
[pdf file]
© SpringerVerlag 2003
 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 137155, February 2003.
[information]
[gzipped ps file]
[pdf file]
[pictures from CTCS'02]
 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 458472, September 2002.
[information]
[slides]
[gzipped ps file]
[pdf file]
© SpringerVerlag 2002
 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 167182, September 2002.
[information]
[gzipped ps file]
[pdf file]
© SpringerVerlag 2002
 M. Hasegawa and Y. Kakutani,
Axioms for recursion in callbyvalue.
HigherOrder
and Symbolic Computation 15(2/3):235264, September 2002.
Extended version of the
FoSSaCS2001 paper.
[information]
[gzipped ps file]
[pdf file]
© 2002 Kluwer Academic Publishers
 M. Hasegawa and Y. Kakutani,
Axioms for recursion in callbyvalue (extended abstract).
In
Proc.
4th International Conference on
Foundations of Software Science and Computation Structures
(FoSSaCS 2001), Genova.
Springer
LNCS 2030, pages 246260, April 2001.
(Here is a picture
associated to this paper.)
Old Version: Preprint RIMS1288, Kyoto University, July 2000.
[information]
[gzipped ps file]
[pdf file]
© SpringerVerlag 2001
For an extended version, see above.
 M. Hasegawa,
Girard translation and logical predicates.
Journal
of Functional Programming 10(1): 7789, January 2000.
[information]
[gzipped ps file]
[pdf file]
 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 198213, April 1999.
[information]
[gzipped ps file]
[pdf file]
© SpringerVerlag 1999
 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 7897, 1998.
[information]
[gzipped ps file]
[pdf file]
 P. Gardner and
M. Hasegawa,
Types and models for higherorder action calculi.
In
Proc. 3rd International Symposium on
Theoretical Aspects of Computer Software
(TACS'97), Sendai.
Springer
LNCS 1281, pages 583603, September 1997.
[information]
[gzipped ps file]
[pdf file]
 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 196213, April 1997.
[information]
[gzipped ps file]
[pdf file]
 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 200219, August 1995.
[information]
[gzipped ps file]
[pdf file]
MSc Thesis

M. Hasegawa, On traced monoidal closed categories.
Invited talk at TMCNAA, July 2007.
[slides (pdf file)]
A paper based on this talk has appeared in MSCS.
 M. Hasegawa, Recursive programs in the abstract.
Talk at PPL2004,
March 2004.
[abstract (pdf file)]
[slides (pdf file)]
 M. Hasegawa,
{>,o} is full in {!,o}.
Proof of a result used in "Linearly used effects"
(FLOPS2002).
Mostly a straightforward reworking of the
JFP paper on Girard's
translation. January 2002.
[manuscript (pdf file)]
 M. Hasegawa,
Glueing algebraic structures on a 2category.
Working draft, April 2000 (slightly updated on February 2002).
[gzipped ps file]
[pdf file]
 M. Hasegawa,
Categorical glueing and logical predicates for models of
linear logic.
Preprint RIMS1223, Kyoto University, January 1999.
[gzipped ps file]
[pdf file]
The conference version is in
Proc. TLCA'99.
 A short proof of the uniqueness of trace on
tortile categories, July 2000.
[gif image file]
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.
 M. Hasegawa,
Program semantics and category theory
(長谷川真人「プログラム意味論と圏論 / 計算の「不変量」を圏論で捉える」).
数学セミナー No. 601: 9298, November 2011.
 M. Hasegawa,
Program semantics and topology  recursion, interaction, knots 
(長谷川真人「プログラム意味論とトポロジー  再帰, 相互作用, 結び目 ).
日本数学会２０１０年度秋季総合分科会企画特別講演アブストラクト, September 2010.
[pdf file]
 M. Hasegawa,
Computer science and knot invariants
(長谷川真人「計算機科学と結び目不変量」).
数理科学
No. 556: 5455, October 2009.
 M. Hasegawa,
On semantics of recursive programs
(長谷川真人「再帰プログラムの意味論について」).
数学
59(2): 180191, April 2007.
[JSTAGE]
[pdf file]
 M. Hasegawa,
On New Year's Eve
(長谷川真人「大晦日の草稿」).
コンピュータソフトウェア 17(1): 1518, January 2000.
[CiNii]
[pdf file]
 M. Tanabe,
R. Nakajima and M. Hasegawa,
Introduction to Computer Science: Logic and Program Semantics
(田辺誠、中島玲二、長谷川真人
「コンピュータサイエンス入門：論理とプログラム意味論」).
岩波書店, September 1999.
[情報]
 M. Hasegawa,
Semantics of recursive programs and traced monoidal categories
(長谷川真人 「再帰的プログラムの意味論とトレース付きモノイダルカテゴリ」).
コンピュータソフトウェア 16(2): 6266, March 1999.
[CiNii]
[pdf file]
 M. Hasegawa,
Models of recursive programs and invariants of links
(長谷川真人 「再帰的プログラムの意味論と絡み目の不変量」).
In
Proc. JSSST'98,
Univ. ElectroCommunications, Tokyo, pages 193196, September 1998.
[gzipped ps file]
[pdf file]
Masahito Hasegawa /
hassei at kurims.kyotou.ac.jp