Chung-Kil (Gil) Hur (허충길)

Chung-Kil (Gil) 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 Sep. 2012, I am a post-doctoral researcher in Programming Principles and Tools group at Microsoft Research Cambridge.

My new web page is at http://research.microsoft.com/en-us/people/gil/.
From Oct. 2010 to Aug. 2012, I was 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 with financial support from Samsung Scholarship (formerly known as Samsung LeeKunHee Scholarship).
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:

Software Verification (especially, Compiler Verification)
Program Logic
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.
Paco
A Coq library for parameterized coinduction.

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.

Parametric bisimulations: a logical step forward.
Chung-Kil Hur, Georg Neis, Derek Dreyer and Viktor Vafeiadis.
Submitted.
[draft: pdf] [appendix: pdf] [coq script: zip]
The power of parameterization in coinductive proof.
Chung-Kil Hur, Georg Neis, Derek Dreyer and Viktor Vafeiadis.
To appear in Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013).
[paper: pdf] [slides: pdf] [coq script: zip]
Strongly typed term representations in Coq. [Link]
with Nick Benton, Andrew Kennedy and Conor 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.
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]
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 power of parameterization in coinductive proof.
- Chocola Seminar, Lyon, France, 14 Mar 2013.
- POPL 2013, Rome, Italy, 23 Jan 2013.
[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.

Last modified: 10 May 2013