Chung-Kil Hur (허충길)

Chung-Kil Hur (허충길)

MPI-SWS
Campus E1 4
66123 Saarbrücken
Germany

gil#mpi-sws:org
where # is @ and : is .

Tel: +49 (0)681 9303 8711

Since Oct. 2010, I am a post-doctoral researcher in Derek Dreyer's Type Systems and Functional Programming group at Max Planck Institute for Software Systems (MPI-SWS).
From Nov. 2009 to Sep. 2010, I was a post-doctoral researcher at Laboratoire Preuves, Programmes et Systèmes (PPS), CNRS & Université Paris Diderot.
From Nov. 2008 to Jan. 2009, I worked as a research intern in Programming Principles and Tools Group at Microsoft Research Cambridge.
From Oct. 2004 to Oct. 2009, I did my phd in Computer Laboratory at University of Cambridge under the supervison of Marcelo Fiore.
From Mar. 1995 to Feb. 2000, I did my undergraduate degree in both Mathematics and Computer Science at KAIST.
In July 1994, I won a bronze medal in the 35th International Mathematical Olympiad (IMO).

My specific interests include:

certified software (in particular, certified compiler),
program logic for software verification,
automated & interactive theorem proving,
programming language theory,
category theory.

Tools

Heq
A Coq library to support reasoning about Heterogeneous Equality.
Hpattern
A generalized version of the tactic 'pattern' in Coq.

Thesis

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

Publications

"with coauthors" denotes that the authors of the paper are listed alphabetically.

The transitive composability of relation transition systems.
Chung-Kil Hur, Georg Neis, Derek Dreyer and Viktor Vafeiadis.
MPI-SWS Technical Report MPI-SWS-2012-002, April 2012.
[paper: pdf] [coq script: zip]
The marriage of bisimulations and Kripke logical relations. [Link]
Chung-Kil Hur, Derek Dreyer, Georg Neis and Viktor 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]
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 and Viktor Vafeiadis.
Proceedings of the 26th annual IEEE Symposium on Logic in Computer Science (LICS 2011), June 2011.
[paper: pdf] [appendix: pdf] [slides: pdf]
Strongly typed term representations in Coq. [Link]
with Nick Benton, Andrew Kennedy and Conor McBride.
Journal of Automated Reasoning (JAR), doi:10.1007/s10817-011-9219-0 (Online First), March 2011.
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]
A Kripke logical relation between ML and assembly. [Link]
Chung-Kil Hur and 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 and 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]

Talks

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

Last modified: 14 Nov 2011