Interests: **computation & logic**

(categorical logic, type theory, domain theory, polymorphism, higher-order computability, intersection types, GoI, (co)algebra, bidirectional transformation, program verification)

CV

- Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano

**Streaming Ranked-Tree-to-String Transducers**

*Theoretical Computer Science, January 5, 2021*

(Journal version of CIAA 2019)

- Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada

**Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence**

*Logical Methods in Computer Science, February 22, 2019, Volume 15, Issue 1*

(Journal version of FoSSaCS 2017)

- Makoto Hamana, Kazutaka Matsuda, and Kazuyuki Asada

**The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics**

*Mathematical Structures in Computer Science, 28(2), February 2018, pp. 287-337.*

- Kazuyuki Asada, Ryosuke Sato, and Naoki Kobayashi

**Verifying Relational Properties of Functional Programs by First-Order Refinement**

*Science of Computer Programming, 137(1), April 2017, pp. 2-62*

(Journal version of PEPM 2015)

- Ryosuke Sato, Kazuyuki Asada, and Naoki Kobayashi

**Refinement Type Checking via Assertion Checking**

*Journal of Information Processing, 23(6), 2015, pp. 827-834*

- Kazuyuki Asada and Naoki Kobayashi

**Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars**

In Proc.*5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)*, Paris (online)

LIPIcs 167, 2020, pp. 22:1--22:22

- Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada

**On Average-Case Hardness of Higher-Order Model Checking**

In Proc.*5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)*, Paris (online)

LIPIcs 167, 2020, pp. 21:1--21:23

- Yuta Takahashi, Kazuyuki Asada, and Keisuke Nakano

**Streaming Ranked-Tree-to-String Transducers**

In Proc.*24th International Conference on Implementation and Application of Automata (CIAA 2019)*, Slovakia

Journal version is here.

- Kazuyuki Asada and Naoki Kobayashi

**Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered**

In Proc.*38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)*, India

LIPIcs 122, 2018, pp. 14:1--14:15

[full version]

- Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong

**Species, Profunctors and Taylor Expansion Weighted by SMCC --A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs--**

In Proc.*the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)*, United Kingdom

pp. 889-898. ACM

[full version]

- Kazuyuki Asada and Naoki Kobayashi

**Pumping Lemma for Higher-order Languages**

In Proc.*the 44th International Colloquium on Automata, Languages and Programming (ICALP 2017)*, Poland

LIPIcs 80, 2017, pp. 97:1--97:14

[full version]

- Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong

**Generalised Species of Rigid Resource Terms**

In Proc.*the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)*, Iceland

pp. 1-12. IEEE.

[pdf]

- Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, and Takeshi Tsukada

**Almost Every Simply Typed ƒÉ-Term Has a Long ƒÀ-Reduction Sequence**

In Proc.*the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017)*, Sweden

LNCS 10203, pp. 53-68. Springer-Verlag

[full version]

Journal version is here, where the infinite monkey theorem for the lambda-calculus is generalized to that for regular tree languages.

- Kazutaka Matsuda and Kazuyuki Asada

**A Functional Reformulation of UnCAL Graph-Transformations — Or, Graph Transformation as Graph Reduction**

In Proc.*ACM SIGPLAN 2017 Workshop on Partial Evaluation and Program Manipulation (PEPM 2017)*, Paris

pp. 71-82

- Kazuyuki Asada and Naoki Kobayashi

**On Word and Frontier Languages of Unsafe Higher-Order Grammars**

In Proc.*the 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016)*, Italy

LIPIcs 55, 2016, pp. 111:1--111:13

[full version]

- Sadaaki Kawata, Kazuyuki Asada, and Naoki Kobayashi

**Decision Algorithms for Checking Definability of Order-2 Finitary PCF**

In Proc.*the 13rd ASIAN Symposium on Programming Languages and Systems (APLAS 2015)*, Korea

LNCS 9458, pp. 313-331. Springer.

- Kazuyuki Asada, Ryosuke Sato, and Naoki Kobayashi

**Verifying Relational Properties of Functional Programs by First-Order Refinement**

In Proc.*ACM SIGPLAN 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM 2015)*, India

pp. 61-72

Journal version is here.

- Kazuyuki Asada, Soichiro Hidaka, Hiroyuki Kato, Zhenjiang Hu, and Keisuke Nakano

**A Parameterized Graph Transformation Calculus for Finite Graphs with Monadic Branches**

In Proc.*15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013)*, Spain

pp. 73-84

[pdf] Copyright ACM.

- Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, and Keisuke Nakano

**Structural Recursion for Querying Ordered Graphs**

In Proc.*18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013)*, USA

pp. 305-318

[pdf] Copyright ACM.

- Kazuyuki Asada

**Arrows are Strong Monads**

In Proc.*3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming (MSFP 2010)*, USA

pp. 33-42

[pdf] Copyright ACM.

- Kazuyuki Asada and Ichiro Hasuo

**Categorifying Computations into Components via Arrows as Profunctors**

In Proc.*10th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2010)*, Cyprus

Electr. Notes Comp. Sci., 264(2), pp. 25-45, 2010

[pdf] Copyright Elsevier

(Preprint of an extended version: [pdf])

- Kazuyuki Asada

**Extensional Universal Types for Call-by-Value**

In Proc.*the Sixth ASIAN Symposium on Programming Languages and Systems (APLAS 2008)*, India

LNCS 5356, pp. 122-137. Springer-Verlag

[pdf] (including Erratum) Copyright Springer-Verlag

(Manuscript on an example of*non*-models; this is nothing to do with the above erratum.)

- Kazuyuki Asada, Soichiro Hidaka, Hiroyuki Kato, Zhenjiang Hu, and Keisuke Nakano

**Parameterized Graph Transformation Languages with Monads**

Technical Report GRACE-TR-2012-07, GRACE Center, National Institute of Informatics, October 2012

[pdf].

- Soichiro Hidaka, Kazuyuki Asada, Hiroyuki Kato, Keisuke Nakano, Zhenjiang Hu

**Towards Bidirectional Transformations on Ordered Graphs**

Technical Report GRACE-TR-2011-07, GRACE Center, National Institute of Informatics, December 2011

[pdf].

- Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada

**Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence**

*14th workshop Computational Logic and Applications (CLA 2019)*

- Kazuyuki Asada and Takeshi Tsukada

**Strategies in HO/N games as profunctors**

*Games for Logic and Programming Languages XI (GaLoP 2016)*

- Ryosuke Sato, Kazuyuki Asada, Naoki Kobayashi

**Refinement Type Checking via Assertion Checking**

*Workshop on Higher-Order Program Analysis (HOPA 2015)*

- PC member of FSCD 2022
- PC member of PPL 2021
- Local co-chair of FLOPS 2020
- OC member of PPL 2020
- OC chair of PPL 2019
- PC member of PPL 2017
- PC member of PPL 2015

- Kiso Seminar, Tohoku University, (2019)
- Programming Exercise B, Tohoku University, (2019)
- Information-Logic Exercise, The University of Tokyo, (2018)
- Part-time Lecturer of Linear Algebra, Tokyo Institute of Technology (2016, 2017)
- Part-time Lecturer of Numerical Analysis, Doshisha University (2010)

I'm an Assistant Professor at Nakano Lab

(in Systems & Software Division,
Research Institute of Electrical Communication,
Tohoku University,
Japan).

Previously I belonged to Nishimura Lab, Hasegawa Lab (PhD), Takeichi Lab, BiG in Hu Lab, and Kobayashi Lab.

e-mail: let # = @ in asada#riec.tohoku.ac.jp