Publications

2018

2017

2016

2015

2014

2013

2012

2011

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

2007