Publications

 denotes that the paper is published at a flagship conference.
[according to both the core conference ranking and the Korean Institute of Information Scientists and Engineers (KIISE)]

2017

  • Taming Undefined Behavior in LLVM.
    Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur
    , Sanjoy Das (Azul Systems), David Majnemer (Google), John Regehr, Nuno P. Lopes.
    Proceedings of the 38th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2017).
    [paper: pdf] [project page]
  • Repairing Sequential Consistency in C/C++11.
    Ori LahavViktor Vafeiadis, Jeehoon Kang, Chung-Kil HurDerek Dreyer.
    Proceedings of the 38th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2017).
    PLDI 2017 Distinguished Paper Award.
    [paper: pdf] [project page]
  • A Promising Semantics for Relaxed-Memory Concurrency
    Jeehoon Kang, Chung-Kil HurOri LahavViktor VafeiadisDerek Dreyer.
    Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2017).
    [paper: pdf] [project page]

2016

  • Lightweight Verification of Separate Compilation
    Jeehoon Kang, Yoonseung KimChung-Kil HurDerek DreyerViktor Vafeiadis.
    Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016).
    [paper: pdf] [project page]

2015

2014

  • Towards Scalable Translation Validation of Static Analyzers. [Link]
    Jeehoon Kang, Sungkeun Cho, Joonwon ChoiChung-Kil HurKwangkeun Yi.
    ROSAEC Technical Report ROSAEC-2014-003, Nov 2014.
    [paper: pdf]
  • An Extensible Verified Validator For Simple Optimizations in LLVM. [Link]
    Sungkeun Cho, Joonwon Choi, Jeehoon KangChung-Kil HurKwangkeun Yi.
    ROSAEC Technical Report ROSAEC-2014-002, Sep 2014.
    [paper: pdf]
  • R2: An Efficient MCMC Sampler for Probabilistic Programs. [Link]
    Aditya Nori, Chung-Kil Hur, Sriram Rajamani, Selva Samuel.
    Proceedings of the 28th AAAI conference on Artificial Intelligence (AAAI 2014). (oral presentation)
    [paper: pdf] [project page]
  • Slicing Probabilistic Programs. [Link
    Chung-Kil Hur, Aditya Nori, Sriram Rajamani, Selva Samuel.
    Proceedings of the 35th annual ACM SIGPLAN conference on Programming Languages Design and Implementation (PLDI 2014).
    [paper: pdf] [project page]
  • A Logical Step Forward in Parametric Bisimulations. [Link]
    Chung-Kil Hur, Georg Neis, Derek DreyerViktor Vafeiadis.
    MPI-SWS Technical Report MPI-SWS-2014-003, January 2014.
    [paper: pdf] [coq script: zip]

2013

  • Semantic sensitive sampling for probabilistic programs. [Link]
    Aditya Nori, Chung-Kil Hur, Sriram Rajamani, Selva Samuel.
    Microsoft Research Technical Report MSR-TR-2013-109. Oct 2013.
    [paper: pdf]
  • The power of parameterization in coinductive proof. [Link]
    Chung-Kil Hur, Georg Neis, Derek DreyerViktor Vafeiadis.
    Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013).
    [paper: pdf] [slides: pdf] [coq script: zip]

2012

  • Strongly typed term representations in Coq. [Link]
    Chung-Kil Hur with Nick Benton, Andrew KennedyConor McBride.
    Journal of Automated Reasoning (JAR), 49(2):141-159, August 2012.
    Special issue on Theory and Applications of Abstraction, Substitution and Naming.
    This is a significantly revised and expanded version of our WMM 2009 paper.
    [paper: pdf] [coq script: zip]
  • The transitive composability of relation transition systems. [Link]
    Chung-Kil Hur, Georg Neis, Derek DreyerViktor Vafeiadis.
    MPI-SWS Technical Report MPI-SWS-2012-002, May 2012.
    [paper: pdf] [coq script: zip]
  • The marriage of bisimulations and Kripke logical relations. [Link]
    Chung-Kil Hur, Derek Dreyer, Georg NeisViktor Vafeiadis.
    Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), January 2012.
    [paper: pdf] [appendix: pdf] [coq script: zip] [slides: pdf]

2011

  • On the mathematical synthesis of equational logic. [Link]
    Chung-Kil Hur 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 DreyerViktor 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 HurDerek 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)]

2010

  • Step-indexing: the good, the bad and the ugly. [Link]
    Chung-Kil Hur 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]
    Chung-Kil Hur 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.
    Chung-Kil Hur 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]
    Chung-Kil Hur with Nick Benton.
    Microsoft Research Technical Report MSR-TR-2010-62. May 2010.
    [paper: pdf] [coq script: zip]

2009

  • Strongly typed term representations in Coq.
    Chung-Kil Hur with Nick BentonAndrew Kennedy.
    The 4th informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM 2009), September 2009.
    [paper: pdf]
  • Biorthogonality, step-indexing and compiler correctness. [Link]
    Chung-Kil Hur 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]
    Chung-Kil Hur with Marcelo Fiore.
    Theoretical Computer Science (TCS), 410(18):1704-1729, April 2009.
    Special issue devoted to selected papers from ICALP 2007.
    [paper: pdf]

2008

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

2007

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