Chung-Kil Hur 허충길

Chung-Kil Hur  SNU
Assistant Professor, Department of Computer Science and Engineering
Adjunct Professor, Department of Mathematical Sciences
Seoul National University
1 Gwanak-ro, Gwanak-gu
Seoul 08826
Republic of Korea
gil.hur#sf:snu:ac:kr where # is @ and : is .
Tel: +82 (0)2 880 1844


I lead the Software Foundations Laboratory.

Education

Research Experience

Honors and Awards

Teaching

See Courses

Professional Activities

  • Invited speaker and lecturer:
  • Invited participant:
    • Dagstuhl Seminar on Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl 15191), 2015
    • Dagstuhl Seminar on Challenges and Trends in Probabilistic Programming (Dagstuhl 15181), 2015
    • Dagstuhl Seminar on Modelling, Controlling and Reasoning About State (Dagstuhl 10351), 2010

Research Interests

  • Semantics of C/C++
  • Relaxed Memory Concurrency
  • Software (esp. Compiler) Verification
  • Probabilistic Programs & Bayesian Inference
  • Interactive Theorem Proving
  • Program Logic
  • Programming Language Theory
  • Category Theory

Research Advisees

See People.

Tools

  • Heq
    A Coq library to support reasoning about Heterogeneous Equality.
  • Hpattern
    A generalized version of the tactic ‘pattern’ in Coq.
  • Paco
    A Coq library for parameterized coinduction.
  • R2 Project
    Bayesian inference system for probabilistic programs.
  • SepCompCert
    Verification of separate compilation of CompCert

Publications

– “with coauthors” denotes that the authors are listed alphabetically.
– top denotes that the paper is published at a top conference.
[according to both the core conference ranking and the Korean Institute of Information Scientists and Engineers (KIISE)]

2017

2016

2015

2014

  • Towards Scalable Translation Validation of Static Analyzers. [Link]
    Jeehoon Kang, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun 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 Kang, Chung-Kil Hur, Kwangkeun Yi.
    ROSAEC Technical Report ROSAEC-2014-002, Sep 2014.
    [paper: pdf]
  • R2: An Efficient MCMC Sampler for Probabilistic Programs. [Link] top
    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] top
    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] top
    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]
    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] top
    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]
    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] top
    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] top
    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]
    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]

2009

  • Strongly typed term representations in Coq.
    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] top
    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]

2008

  • 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]

2007

  • 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]

Thesis

  • Categorical equational systems: algebraic models and equational reasoning. [Link]
    Computer Laboratory, University of Cambridge, UK, 2010
    [summary: pdf] [thesis: pdf]

Talks

[not updated since 2013]

  • The power of parameterization in coinductive proof.

    [slides: pdf]

  • Compositional inter-language relational verification (using interactive theorem prover).
    Seoul National University, Seoul, Korea, 10 Dec 2012.
  • The power of parameterization in coinductive proof.
    Semantics Lunch Seminar, University of Cambridge, Cambridge, UK, 22 Oct 2012.
  • Compositional inter-language relational verification.
    • Yale University, New Haven, USA, 14 May 2012.
    • KAIST, Daejeon, Korea, 23 Apr 2012.
    • University of Colorado at Boulder, Boulder, USA, 13 Apr 2012.
    • Microsoft Research Cambridge, Cambridge, UK, 30 Mar 2012.
  • Compositional software verification.
    Seoul National University, Seoul, Korea, 16 Dec 2011.
  • The marriage of bisimulations and Kripke logical relations.
    ROPAS Weekly Show & Tell, Seoul National University, Seoul, Korea, 9 Sep 2011.
  • A Kripke logical relation between ML and assembly.
    • PL/Verification Seminar, MPI-SWS, Saarbrücken, Germany, 25 Feb 2011.
    • POPL 2011, Austin, USA, 26 Jan 2011.

    [abstract: txt] [slides: pptx (powerpoint 2010)]

  • A Kripke logical relation between ML and assembly.
    Dagstuhl Seminar: Modelling, Controlling and Reasoning About State, Schloss Dagstuhl, Germany, 1 Sep 2010.
    [abstract: txt] [slides: pdf]
  • Heq: a Coq library for heterogeneous equality.
    Coq Workshop 2010, Edinburgh, U.K., 9 Jul 2010.
    [abstract: txt] [slides: pdf]
  • Program equivalence and compositional compiler correctness.
    Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany, 22 Mar 2010.
    [abstract: txt] [slides: pdf]
  • Observational equivalence on low-level programs and compositional compiler correctness.
    Type theory and realizability, PPS, Paris, France, 2 Dec 2009.
    [abstract: txt] [slides: pdf]
  • Logical relations and compositional compiler correctness.
    • ROSAEC Center Seminar, Seoul National University, Seoul, Korea, 14 Oct 2009.
    • Programming Languages Laboratory Seminar, KAIST, Daejeon, Korea, 21 Oct 2009.

    [abstract: txt] [slides: pdf]

  • Biorthogonality, step-indexing and compiler correctness.
    ICFP 2009, Royall College of Physicians, Edinburgh, UK, 31 Aug 2009.
    [abstract: txt] [slides: pdf]
  • Compiler correctness and observational equivalence on machine code.
    Semantics Lunch, Computer Laboratory, Cambridge, UK, 16 Mar 2009.
    [abstract: txt] [slides: pdf]
  • Categorical equational systems.
    PhD Seminar, University of Leicester, Leicester, UK, 02 Dec 2008.
    [abstract: txt] [slides: pdf]
  • Term equational systems and logics.
    • KAIST Discrete Math Seminar, KAIST, Daejeon, Korea, 11 Aug 2008.
    • Programming Languages Laboratory Seminar, KAIST, Daejeon, Korea, 12 Aug 2008.

    [abstract: txt] [slides: pdf]

  • Term equational systems and logics.
    MFPS 2008, University of Pennsylvania, Philadelphia, USA, 24 May 2008.
    [abstract: txt] [slides: pdf]
  • Term equational rewrite systems and logics.
    Semantics Lunch, Computer Laboratory, Cambridge, UK, 11 Feb 2008.
    [abstract: txt] [slides: pdf]
  • Applications of equational systems: nominal equational logic.
    Computational Applications of Nominal Sets (CANS) Meeting, Computer Laboratory, Cambridge, UK, 25 Oct 2007.
    [slides: pdf]
  • Equational systems and free constructions.
    ICALP 2007, University of Wroclaw, Poland, 12 Jul 2007.
    [abstract: txt] [slides: pdf]
  • Equational systems and free constructions.
    Extreme Theory Meeting, Computer Laboratory, Cambridge, UK, 28 Jun 2007.
  • Algebraic theories in the presence of binding operators, substitution, etc.
    Semantics Lunch, Computer Laboratory, Cambridge, UK, 20 Mar 2006.
    [abstract: txt] [slides: pdf]
  • Abstract models for structural data and its substitution.
    Extreme Theory Meeting, Computer Laboratory, Cambridge, UK, 19 Oct 2005.