Dohan Kim

Research Interests

  • Term rewriting and string rewriting
  • Equational theorem proving and reasoning
  • Theorem proving with Isabelle/HOL
  • Group-theoretical methods in computer science

Publications

  1. An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
    Dohan Kim, Teppei Saito, René Thiemnn, and Akihisa Yamada, Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, to appear.
  2. Equational Theorem Proving for Clauses over Strings
    Dohan Kim, Mathematical Structures in Computer Science (special issue: LSFA 2021 and 2022), Cambridge University Press, published online, 2024.
    [Publisher's link (Cambridge University Press)]
  3. Finding k Shortest Paths in Cayley Graphs of Finite Groups
    Dohan Kim, Graphs and Combinatorics, Springer, vol. 40, article no. 120, 2024.
    [Publisher's link (Springer)]
  4. An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility
    Dohan Kim, 15th International Conference on Interactive Theorem Proving, ITP 2024, Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 24:1-24:19, 2024.
    [Publisher's link (Schloss Dagstuhl)]
  5. Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
    Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, pp. 147-161, 2024.
    [Publisher's link (ACM)]
  6. Equational Theorem Proving for Clauses over Strings
    Dohan Kim, Proc. of the 17th Logical and Semantic Frameworks with Applications (LSFA 2022), Electronic Proceedings in Theoretical Computer Science (EPTCS), vol 376, pp. 49-66, 2022.
    [Publisher's link (PDF)]
  7. Equational Theorem Proving Modulo
    Dohan Kim and Christopher Lynch, In: Platzer A., Sutcliffe G. (eds) Proc. of the 28th International Conference on Automated Deduction – CADE 28, Lecture Notes in Artificial Intelligence (LNAI/LNCS), vol 12699, Springer, 2021.
    [PDF, Publisher's link (Springer)]
  8. An RPO-based ordering modulo permutation equations and its applications to rewrite systems
    Dohan Kim and Christopher Lynch, In: Kobayashi N. (eds) Proc. of the 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, Leibniz International Proceedings in Informatics (LIPIcs), vol 195, pp. 19:1–19:17, Schloss Dagstuhl, 2021.
    [PDF, Publisher's link (Schloss Dagstuhl)]
  9. Congruence Closure Modulo Permutation Equations
    Dohan Kim and Christopher Lynch, In: Kutsia T. (eds) Proc. of the 9th International Conference on Symbolic Computation in Software Science (SCSS 2021), Electronic Proceedings in Theoretical Computer Science (EPTCS), vol 342, pp. 86–98, 2021.
    [PDF, Publisher's link]
  10. Reviving Basic Narrowing Modulo
    Dohan Kim, Christopher Lynch, and Paliath Narendran, In: Herzig A., Popescu A. (eds) Proc. of the 12th International Symposium on Frontiers of Combining Systems, FroCoS 2019, Lecture Notes in Artificial Intelligence (LNAI/LNCS), vol 11715, Springer, 2019.
    [Publisher's link (Springer)]
  11. Sorting on graphs by adjacent swaps using permutation groups
    Dohan Kim, Computer Science Review, vol. 22, pp. 89-105, 2016.
    [PDF, Publisher's link (Elsevier)]
  12. Representations of task assignments in distributed systems using Young tableaux and symmetric groups
    Dohan Kim, International Journal of Parallel, Emergent and Distributed Systems, vol. 31, no. 2, pp. 152-175, 2016.
    [PDF, Publisher's link (Taylor & Francis)]
  13. Group-theoretical vector space model
    Dohan Kim, International Journal of Computer Mathematics, vol. 92, no. 8, pp. 1536-1550, 2015.
    [PDF, Publisher's link (Taylor & Francis)]
  14. Priority-based task reassignments in hierarchical 2D mesh-connected systems using tableaux
    Dohan Kim, Discrete Mathematics, Algorithms and Applications, vol. 6, no. 2 (2014) 1450022 (16 pages).
    [PDF, Publisher's link (World Scientific)]
  15. Task swapping networks in distributed systems
    Dohan Kim, International Journal of Computer Mathematics, vol. 90, no. 11, pp. 2221-2243, 2013.
    [PDF, Publisher's link (Taylor & Francis)]

Dissertation

  • Equational Reasoning Modulo Background Theories
    Ph.D. Dissertation, Clarkson University, Potsdam, New York, USA, 2021 (Advisor: Christopher Lynch).

Program Developments

  • The AdjacentSwaps Package, Version 1.0, Dohan Kim [GitHub]
  • The Geodesics Package, Version 1.0, Dohan Kim [GitHub]
  • The STG Package, Version 1.0, Dohan Kim [GitHub]

Technical Skills

  • C, C++, Java, Isabelle/HOL, Haskell, Linux, SageMath (for Groebner basis computation), GAP (for computational groups), etc.