Pointers: [2020] [2019] [2018] [2017] [2016] [2015] [2014] [2013] [2012] [2011] [2010] [2009] [2008] [2007] [PhD Theses]

“with coauthors” denotes that the authors are listed alphabetically.











  • On the mathematical synthesis of equational logic. [Link]
    with Marcelo Fiore.
    Logical Methods in Computer Science (LMCS), 7(3:12), September 2011.
    [paper: pdf]
  • Separation logic in the presence of garbage collection. [Link]
    Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
    Proceedings of the 26th annual IEEE Symposium on Logic in Computer Science (LICS 2011), June 2011.
    [paper: pdf] [appendix: pdf] [slides: pdf]
  • A Kripke logical relation between ML and assembly. [Link]
    Chung-Kil Hur, Derek Dreyer.
    Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), January 2011.
    [paper: pdf] [appendix: pdf] [slides: pptx (powerpoint 2010), swf (flash)]


  • Step-indexing: the good, the bad and the ugly. [Link]
    with Nick Benton.
    Proceedings of Dagstuhl Seminar 10351: Modelling, Controlling and Reasoning About State (Dagstuhl 10351), September 2010.
    This is a corrected version of our LOLA 2010 paper.
    [paper: pdf]
  • Second-order equational logic. [Link]
    with Marcelo Fiore.
    Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), August 2010.
    [paper: pdf]
  • Step-indexing: the good, the bad and the ugly.
    with Nick Benton.
    Workshop on Syntax and Semantics of Low Level Languages (LOLA 2010), satellite workshop of LICS 2010, July 2010.
    [paper: pdf]
  • Heq: a Coq library for heterogeneous equality.
    Chung-Kil Hur.
    The 2nd Coq Workshop (Coq 2010), satellite workshop of ITP 2010, July 2010.
    [paper: pdf] [coq script: script] [slides: pdf]
  • Realizability and compositional compiler correctness for a polymorphic language. [Link]
    with Nick Benton.
    Microsoft Research Technical Report MSR-TR-2010-62. May 2010.
    [paper: pdf] [coq script: zip]


  • Strongly typed term representations in Coq.
    with Nick Benton, Andrew Kennedy.
    The 4th informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM 2009), September 2009.
    [paper: pdf]
  • Biorthogonality, step-indexing and compiler correctness. [Link]
    with Nick Benton.
    Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009), August 2009.
    [paper: pdf] [coq script: zip] [slides: pdf]
  • On the construction of free algebras for equational systems. [Link]
    with Marcelo Fiore.
    Theoretical Computer Science (TCS), 410(18):1704-1729, April 2009.
    Special issue devoted to selected papers from ICALP 2007.
    [paper: pdf]


  • Term equational systems and logics. [Link]
    with Marcelo Fiore.
    Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2008), May 2008.
    [paper: pdf] [slides: pdf]


  • Equational systems and free constructions. [Link]
    with Marcelo Fiore.
    Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP 2007), July 2007.
    [paper: pdf] [errata: pdf] [slides: pdf]

PhD Theses

  • Reconciling low-level features of C with compiler optimizations.
    Jeehoon Kang.
    Department of Computer Science and Engineering, Seoul National University, Korea, 2019
    [thesis: pdf] [project page]
  • Categorical equational systems: algebraic models and equational reasoning. [Link]
    Chung-Kil Hur.
    Computer Laboratory, University of Cambridge, UK, 2009
    [summary: pdf] [thesis: pdf]