Kazuyuki Asada

Interests: computation & logic
(categorical logic, type theory, domain theory, polymorphism, parametricity, computational effects, linear logic, intersection types, (co)algebra, bidirectional transformation, program verification)
CV

Journal Papers

Conference Papers

  • Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo
    Compositional Probabilistic Model Checking with String Diagrams of MDPs
    In Proc. the 35th International Conference on Computer Aided Verification (CAV 2023), Paris
    LNCS 13966, pp. 40-61. Springer
    [full version]

  • Kazuyuki Asada, Hiroyuki Katsura, Naoki Kobayashi
    On Higher-Order Reachability Games vs May Reachability
    In Proc. the 16th International Conference on Reachability Problems (RP 2022), Germany
    LNCS 13608, pp. 108-124. Springer
    [full version]

  • Takeshi Tsukada and Kazuyuki Asada
    Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
    In Proc. the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022), Israel
    No. 60, pp. 1-13. ACM
    [full version]

  • Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo
    A Compositional Approach to Parity Games
    In Proc. the 37th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2021), Salzburg (online, hybrid)
    EPTCS 351, 2021, pp. 278-295

  • Kazuyuki Asada and Naoki Kobayashi
    Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars
    In Proc. the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Paris (online)
    LIPIcs 167, 2020, pp. 22:1--22:22
    [full version]

  • Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada
    On Average-Case Hardness of Higher-Order Model Checking
    In Proc. the 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. the 24th International Conference on Implementation and Application of Automata (CIAA 2019), Slovakia
    LNCS 11601, pp. 235-247. Springer, Cham
    Journal version is here.

  • Kazuyuki Asada and Naoki Kobayashi
    Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered
    In Proc. the 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. the 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. the 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. the 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. the 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.)

Technical Reports

Talks

  • 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
    the 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)

Academic Activities

Teaching Activities

  • Programming Exercise B, Tohoku University, (2019--2023)
  • Category Theory, Chiba University, (2022)
  • Kiso Seminar, Tohoku University, (2019, 2020)
  • 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