Koko Muroya (室屋 晃子)
- Project researcher in
NII
(September 2024 – present).
- Postal address:
Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502, Japan
Email:
kmuroya [at] nii.ac.jp
/ koko.muro.m [at] gmail.com
/ kmuroya [at] kurims.kyoto-u.ac.jp
/ k.muroya [at] cs.bham.ac.uk
/ muroykk [at] is.s.u-tokyo.ac.jp
- Alumna of:
News
- [June 2024] I'll be taking a part of Adjoint School 2024 as a mentor!
- [June 2024] A few papers will be published finally :-D
Research Interests
- Diagrammatic modelling of program execution,
for reasoning intensional, extensional and relational properties such as:
- Trade-off between space efficiency and time efficiency
- Observational (contextual) equivalence
- Dataflow manipulation in conventional programming
- More technically: interplay between interaction
(information-flow) semantics and rewriting
- Graph-rewriting abstract machines for functional programs,
guided by Girard's Geometry of Interaction
- Also, various approaches to proving observational equivalence, such as:
- an automata-theoretic approach using simulation notions
- a term-rewriting-theoretic approach exploiting critical pair analysis
Tools
Papers / Theses
[Publication (dblp)]
-
Koko Muroya, Takahiro Sanada and Natsuki Urabe.
Preorder-Constrained Simulations for Program Refinement with Effects.
To appear in Proc.
CMCS 2024.
[preprint pdf with appendix]
- Takahiro Sanada,
Ryota Kojima, Yuichi Komorida, Koko Muroya and
Ichiro Hasuo.
Explicit Hopcroft’s Trick in Categorical Partition Refinement.
To appear in Proc.
CMCS 2024.
- Ryota Kojima, Corina Cirstea, Koko Muroya and
Ichiro Hasuo.
Coalgebraic CTL: Fixpoint Characterization and Polynomial-time Model Checking.
To appear in Proc.
CMCS 2024.
-
Koko Muroya and
Makoto Hamana.
Term Evaluation Systems with Refinements: First-Order, Second-Order, and Contextual Improvement.
To appear in Proc.
FLOPS 2024.
[preprint pdf with appendix]
-
Steven W. T. Cheung,
Dan R. Ghica, and Koko Muroya.
Transparent Synchronous Dataflow.
Art Sci. Eng. Program.,
5(3):12, 2021.
[doi]
-
Koko Muroya.
Hypernet Semantics of Programming Languages.
PhD thesis, University of Birmingham, 2020.
[e-thesis
| pdf]
-
Koko Muroya and
Dan R. Ghica.
The Dynamic Geometry of Interaction Machine:
a Token-Guided Graph Rewriter.
Logical Methods in Computer Science,
15(4), 2019.
Expanded version of the CSL'17 paper and the WPTE'17 paper.
[lmcs
| arxiv]
-
Koko Muroya,
Steven W. T. Cheung and
Dan R. Ghica.
The Geometry of Computation-Graph Abstraction.
In Proc.
LICS 2018, p. 749–758, 2018.
Revised version of preprint
arXiv:1710.03984.
Twin paper of the FLOPS'18 paper.
[acm
| preprint pdf (extended version)]
[talk slides pdf]
-
Steven W. T. Cheung,
Victor Darvariu,
Dan R. Ghica,
Koko Muroya and
Reuben N. S. Rowe.
A Functional Perspective on Machine Learning
via Programmable Induction and Abduction.
In Proc.
FLOPS 2018,
LNCS 10818, p. 84–98, 2018.
Twin paper of the LICS'18 paper.
[springer
| preprint pdf]
[talk slides pdf]
- Koko Muroya and
Dan R. Ghica.
Efficient Implementation of Evaluation Strategies via
Token-Guided Graph Rewriting.
In Proc.
WPTE 2017,
EPTCS 265, p. 52–66, 2018.
Successor of the CSL'17 paper.
Expanded version published in LMCS, 15(4), 2019.
[eptcs
| arxiv]
[talk slides pdf]
- Koko Muroya and
Dan R. Ghica.
The Dynamic Geometry of Interaction Machine:
a Call-by-Need Graph Rewriter.
In Proc.
CSL 2017, p. 32:1–32:15, 2017.
Followed up by the WPTE'17 paper.
Expanded version published in LMCS, 15(4), 2019.
[lipics
|
arxiv (extended version)]
[talk slides pdf]
-
Koko Muroya.
Recursion and Adequacy
in Memoryful Geometry of Interaction.
Master thesis, University of Tokyo, 2016.
[pdf]
[talk slides pdf in Japanese]
- Koko Muroya,
Naohiko Hoshino and
Ichiro Hasuo.
Memoryful Geometry of Interaction II:
Recursion and Adequacy.
In Proc.
POPL 2016, p. 748–760, 2016.
[acm
| preprint pdf]
[talk slides pdf]
-
Naohiko Hoshino,
Koko Muroya and
Ichiro Hasuo.
Memoryful Geometry of Interaction: from Coalgebraic
Components to Algebraic Effects.
In Proc.
CSL-LICS 2014, p. 52:1–52:10, 2014.
[acm
| preprint pdf]
-
Koko Muroya.
Resumption-Based Categorical Geometry of Interaction for
Effects.
Bachelor thesis, University of Tokyo, 2014.
[pdf]
[talk slides pdf in Japanese]
Abstracts / Preprints / etc.
-
室屋 晃子.
5分で分かる!? 有名論文ナナメ読み Gordon Plotkin & John Power : Adequacy for Algebraic Effects.
情報処理学会誌,
65(6), p. 318-320, 2024.
[webpage]
-
室屋 晃子.
研究と私の紆余曲折.
日本バーチャルリアリティ学会誌,
28(2), p. 19–22, 2023.
[doi]
-
Koko Muroya,
Takahiro Sanada and
Natsuki Urabe.
Preorder-Constrained Simulation
(Early Ideas abstract).
Short abstract presented at
CALCO 2021.
[pdf]
-
Dan R. Ghica,
Koko Muroya and
Todd Waugh Ambridge.
Local Reasoning for Robust Observational Equivalence
(preliminary report).
Short abstract presented at
LOLA 2019.
Successor of the LOLA'18 talk.
[arxiv (working draft)]
[visualiser & online resources]
[talk slides pdf]
-
Dan R. Ghica,
Koko Muroya and
Todd Waugh Ambridge.
A Graph-Rewriting Perspective of the Beta-Law
(preliminary report).
Short abstract presented at
LOLA 2018.
Followed up by the LOLA'19 talk.
[pdf]
[talk slides pdf]
- Koko Muroya,
Steven W. T. Cheung and
Dan R. Ghica.
Abductive Functional Programming, a Semantic Approach.
Preprint.
Revised version published as the FLOPS'18 paper and the LICS'18 paper.
[arxiv]
- Koko Muroya.
Towards Abductive Functional Programming
(preliminary report).
Short abstract presented at
ML Family Workshop 2017.
Culminating in the FLOPS'18 paper.
[pdf]
[talk slides pdf]
- Koko Muroya,
Naohiko Hoshino and
Ichiro Hasuo.
Memoryful GoI with Recursion (preliminary report).
Short abstract presented at
LOLA 2015.
Culminating in the POPL'16 paper.
[pdf]
[talk slides pdf]
- Koko Muroya,
Toshiki Kataoka,
Ichiro Hasuo and
Naohiko Hoshino.
Compiling Effectful Terms to Transducers: Prototype
Implementation of Memoryful Geometry of Interaction
(preliminary report).
Short abstract presented at
LOLA 2014.
[pdf]
[talk slides pdf]
Talks
- Climbing Up a Ladder: an Evitcudnioc Approach to Contextual Refinement.
- Term Evaluation Systems with Refinements: First-Order, Second-Order, and Contextual Improvement.
- プログラムを質的かつ量的に比較する.
日本ソフトウェア学会第40回大会 40周年企画セッション「若手研究者特別講演」
in University of Tokyo, Japan (14 September 2023)
[スライド pdf]
- Preorder-Constrained Simulation for Program Refinement with Effects.
- Local Coherence and Program Refinement (work in progress).
58th TRS Meeting
in Niigata, Japan (20 February 2023)
[slides pdf]
- Program Semantics with Token Passing.
Linear Logic Winter School
online (28 January 2022)
[slides pdf]
- Local Reasoning for Robust Observational Equivalence.
Online LFCS Seminar
at Laboratory for Foundations of Computer Science (LFCS),
University of Edinburgh, United Kingdom (4 December 2020)
Improved presentation of the LOLA'19 work,
similar to the CMCS'20 talk, but with some examples.
[slides pdf]
- Hypernet Semantics and Robust Observational Equivalence.
Invited talk at
CMCS 2020
online (12 October 2020)
Improved presentation of the LOLA'19 work, with
some discussion on simulation notions.
[slides pdf]
- Modelling Program Execution with
Token-Guided (Hierarchical) Graph Rewriting.
Seminar at
Ueda Laboratory,
Waseda University, Japan (30 January 2020)
Overview of my research in Birmingham.
[slides pdf (in English except for the front page)]
- Understanding How You Should (Not) Mix Programming Features.
情報系 WINTER FESTA Episode 5
in Tokyo, Japan (26 December 2019)
[poster pdf]
- Local Reasoning for Robust Observational Equivalence
(preliminary report).
- Online seminar at
Kobayashi Laboratory,
University of Tokyo, Japan (22 April 2020)
- Talks at
Introduction & high-level description of technical development.
[slides pdf]
- Invited talk at
STRINGS 3 and SYCO 5
in Birmingham, United Kingdom (6 September 2019)
Introduction for people in applied category theory &
string diagram community.
[slides pdf]
-
LOLA 2019
in Vancouver, Canada (23 June 2019)
Overview of technical development.
[slides pdf]
- Diagrammatic Execution Models for Functional Languages.
Overview of my research with diagrams.
[slides (of my half) pdf]
- Token-Passing Semantics
with and without Rewriting.
Overview of the LICS'18 paper and more.
[slides pdf]
- The Geometry of Computation-Graph Abstraction.
LICS 2018
in Oxford, United Kingdom (12 July 2018)
[slides pdf]
- A Graph-Rewriting Perspective of the Beta-Law
(preliminary report).
- A Functional Perspective on Machine Learning via Programmable
Induction and Abduction.
FLOPS 2018
in Nagoya, Japan (9 May 2018)
[slides pdf]
- Dynamic Geometry of Interaction: Overview.
Bellairs Workshop on compositional methods for network diagrams and component-based systems
in Bellairs Research Institute, Barbados (18 March 2018)
- Efficient Implementation of Evaluation Strategies via
Token-Guided Graph Rewriting.
WPTE 2017
in Oxford, United Kingdom (8 September 2017)
[slides pdf]
- Towards Abductive Functional Programming
(preliminary report).
ML Family Workshop 2017
in Oxford, United Kingdom (7 September 2017)
[slides pdf]
- The Dynamic Geometry of Interaction Machine:
a Call-by-Need Graph Rewriter.
CSL 2017
in Stockholm, Sweden (21 August 2017)
[slides pdf]
- Dynamic GoI Machine:
Call-by-Need and Call-by-Value Graph Rewriter
(preliminary report).
- Recursion and Adequacy
in Memoryful Geometry of Interaction.
Master thesis presentation in University of Tokyo, Japan
(1 February 2016)
[slides pdf in Japanese]
- Memoryful Geometry of Interaction II:
Recursion and Adequacy.
POPL 2016
in St. Petersburg, Florida, United States
(22 January 2016)
[slides pdf]
- Memoryful GoI with Recursion.
- Compiling Effectful Terms to Transducers: Prototype
Implementation of Memoryful Geometry of Interaction
(preliminary report).
-
ALGI 25
in Kanagawa University, Japan (19 August 2014)
-
LOLA 2014
in Vienna, Austria (13 July 2014)
[slides pdf]
- Resumption-Based Categorical Geometry of Interaction
for Effects.
Bachelor thesis presentation in University of Tokyo, Japan
(12 February 2014)
[slides pdf in Japanese]
Education
Academic Career
- Project researcher in
NII
(September 2024 – present).
- Assistant professor in
RIMS,
Kyoto University
(April 2018 – August 2024).
Teaching
- (分担) 現代の数学と数理解析,
京都大学
(2020年度前期 1回)
- (分担) コンピュータサイエンス基礎,
京都大学
(2019年度前期 3回, 2020年度前期 3回, 2021年度前期 4回, 2023年度前期 4回)
- (TA) Functional Programming,
University of Birmingham
(October 2018 – March 2019)
Professional Services
- PC member for
- international conferences:
TFP 2024,
MFPS 2023,
FoSSaCS 2023,
ICFP 2022,
ICGT 2022,
FLOPS 2022,
POPL 2022,
CALCO 2021,
MFCS 2021,
ACT 2021,
ICGT 2021,
FORTE 2020
- international workshops:
YR-CONCUR 2023,
WPTE 2022,
SYCO 8,
WPTE 2021,
WiL 2021,
ML 2020,
WiL 2020,
TLLA-LINEARITY 2020,
STRINGS 2020 (event cancelled),
SYCO 7 (event postponed indefinitely),
SYCO 6,
GaLoP 2019,
SYCO 2
- domestic workshops:
PPL 2022,
PPL 2021
- Organiser of
- Co-organiser of
- Mentor of
Award
- Dean's Award of Graduate School of
Information Science and Technology
[東京大学大学院 情報理工学系研究科 研究科長賞],
University of Tokyo, 2016.
Research Grants
- Automated proving of simulation congruence on progams via critical pair analysis
(Project No. 22K17850),
Grant-in-Aid for Early-Career Scientists,
Grant-in-Aid for Scientific Research (KAKENHI),
Japan Society for the Promotion of Science (JSPS)
[科研費 若手研究
「プログラムの模倣合同性の危険対解析による自動判定」]
(April 2022 – March 2025)
- A Proof Assistant for Contextual Equivalences,
Using Hierarchical Graph Rewriting
(Grant No. JPMJAX190U),
ACT-X Program
"Frontier of Mathematics and Information Science",
Japan Science and Technology Agency (JST)
[ACT-X「数理・情報のフロンティア」研究領域
（研究課題名：階層的グラフの書き換え系での文脈等価性証明支援）].
(October 2019 – March 2023)
- Co-investigator,
Probabilistic Extension of Geometry of Interaction—from Categorical Semantics to Big Data
(Project No. 15K11984),
Challenging Exploratory Research,
Grant-in-Aid for Scientific Research (KAKENHI),
Japan Society for the Promotion of Science (JSPS)
[科研費 挑戦的萌芽研究
「相互作用の幾何の確率拡張––圏論的意味論からビッグデータへ」
研究分担者].
(May 2018 – March 2019)
Visits
Just to help us remember where we met :)
- 2024
- 2023
- Visit to
Agents, Interaction and Complexity Group,
University of Southampton, United Kingdom
(16–20 October 2023)
- Visit to
Laboratory for Foundations of Computer Science,
University of Edinburgh, United Kingdom
(9–13 October 2023)
- 日本ソフトウェア学会第40回大会
in University of Tokyo, Japan (September 2023)
- ACT-X 第1回成果報告会
in Tokyo, Japan (24–25 April 2023)
- Half-day visit to
Department of Computer Science,
University of Tokyo, Japan (12 April 2023)
-
PPL 2023
in Nagoya, Japan (March 2023)
-
58th TRS Meeting
in Niigata, Japan (February 2023)
- 2021
- 2020
- Online participation in
CMCS 2020
(September & October 2020)
- Half-day visit to
Ueda Laboratory,
Waseda University, Japan (30 January 2020)
- 2019
-
情報系 WINTER FESTA Episode 5
in Tokyo, Japan (December 2019)
-
Categorical Algebra and Computation
(a Workshop in Honour of John Power on the occasion of
his 60th Birthday)
in Kyoto University, Japan (December 2019)
- Visit to
Mobility Reading Group,
Imperial College London, United Kingdom
(13–22 September 2019)
- Visit to
Programming, Logic and Semantics Group,
Computer Laboratory, University of Cambridge, United Kingdom
(9–12 September 2019)
-
STRINGS 3 and SYCO 5
in Birmingham, United Kingdom (September 2019)
- Visit to
JST ERATO MMSD Project,
Tokyo, Japan (regularly from August 2019;
see record)
-
LICS 2019
in Vancouver, Canada (June 2019)
- Visit to
Informatics Theory Group,
University of Bamberg, Germany
(31 January – 1 February 2019)
- 2018
-
Shonan Meeting No.109 on
diagrammatic methods for linear and nonlinear systems
in Shonan Village Center, Japan (November 2018)
- Visit to
JST ERATO MMSD Project,
Tokyo, Japan (19–22 November 2018)
-
Lambda World Cadiz 2018
in Cadiz, Spain (October 2018)
-
CRECOGI Project Meeting 2018
in Paris, France (October 2018)
-
SYCO 1
in Birmingham, United Kingdom (September 2018)
-
CSL 2018
in Birmingham, United Kingdom (September 2018)
-
FLoC 2018
in Oxford, United Kingdom (July 2018)
-
S-REPLS 9
in University of Sussex, United Kingdom (May 2018)
-
FLOPS 2018
in Nagoya, Japan (May 2018)
- Bellairs Workshops on
in Bellairs Research Institute, Barbados (March 2018)
- 2017
- 2016
- 2015
- 2014