Chung-Kil Hur

Chung-Kil Hur

Laboratoire PPS
Université Paris Diderot - Paris 7
Case 7014
75205 PARIS Cedex 13
France

gil#pps:jussieu:fr
where # is @ and : is .

Tel: +33 (0)144 277767

I am a postdoc researcher in Laboratoire Preuves Programmes Systèmes, CNRS & Université Paris Diderot.

I received my phd degree from Computer Laboratory at University of Cambridge under the supervison of Marcelo Fiore.

My specific interests include: category theory, especially categorical algebra; equational logic and term rewriting; step-indexing, logical relation and compositional compiler correctness; Coq proof assistant.

I won a bronze medal in the International Mathematical Olympiad in 1994.

Tools

Heq
A Coq library to support reasoning about Heterogeneous Equality.

Thesis

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

Publications

A kripke logical relation between ML and assembly (with Derek Dreyer).
Submitted.
[preprint: pdf] [appendix: pdf]
Mathematical synthesis of equational logic (with Marcelo Fiore).
Submitted.
[preprint: pdf]
Strongly typed term representations in Coq (with Nick Benton, Andrew Kennedy and Conor McBride).
Submitted.
[preprint: pdf] [coq script: zip]
Realizability and compositional compiler correctness for a polymorphic language (with Nick Benton).
Microsoft Research Technical Report MSR-TR-2010-62. May 2010.
[preprint: pdf] [coq script: zip]
Second-order equational logic (with Marcelo Fiore).
Proceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010).
[preprint: pdf]
Heq: A Coq library for heterogeneous equality.
The 2nd Coq Workshop (Coq 2010), A satellite workshop of ITP 2010.
[preprint: pdf] [coq script: script]
Step-indexing: the good, the bad and the ugly (with Nick Benton).
Syntax and Semantics of Low Level Languages (LOLA 2010), A satellite workshop of LICS 2010.
[preprint: pdf]
Strongly typed term representations in Coq (with Nick Benton and Andrew Kennedy).
The 4th informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM 2009).
[preprint: pdf]
Biorthogonality, step-indexing and compiler correctness (with Nick Benton).
Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009).
[preprint: pdf] [coq script: zip]
On the construction of free algebras for equational systems (with Marcelo Fiore).
Theoretical Computer Science, 410(18):1704-1729, 2009.
[preprint: pdf]
Term equational systems and logics (with Marcelo Fiore).
Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2008).
[preprint: pdf]
Equational systems and free constructions (with Marcelo Fiore).
Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP 2007).
[preprint: pdf] [errata: pdf]

Talks

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, Saarbruecken, 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: 19 Jul 2010