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. 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]
  2. 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 (PDF)]
  3. 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 (Oral Presentation).
    [Publisher's link (PDF)]
  4. 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 (Oral Presentation).
    [PDF, Publisher's link (Springer)]
  5. 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 (Oral Presentation).
    [PDF, Publisher's link (Schloss Dagstuhl)]
  6. 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 (Oral Presentation).
    [PDF, Publisher's link]
  7. 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)]
  8. 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)]
  9. 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)]
  10. 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)]
  11. 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)]
  12. 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.