Interests: **computation & logic**

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

CV

- 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*

- 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

to appear.

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

- 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]

- 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 ver. 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 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)*

- 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