Dohan Kim

Postdoctoral researcher (since September 2022) Room: 3M12 in the ICT building Email: dohan.kim__AT__uibk.ac.at Computational Logic Group of the University of Innsbruck ARI project

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. 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]
3. 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)]
   
4. 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)]
   
5. 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)]
   
6. 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)]
   
7. 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]
   
8. 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)]
   
9. 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)]
   
10. 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)]
    
11. 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)]
    
12. 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)]
    
13. 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.