Chung-Kil Hur

Chung-Kil Hur

University of Cambirdge
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD

ckh25#cam:ac:uk
where # is @ and : is .

Tel: +44 (0)1223 763626
Fax: +44 (0)1223 334678

I am a PhD student in Theory and Semantics Group of the Computer Laboratory, University of Cambirdge and a member of Churchill College. My supervisor is Marcelo Fiore.

My specific interests include: category theory, especially categorical algebra; equational logic and term rewriting; logical relation and compiler correctness.

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

Publications

Compositional compiler correctness with quantified types (with Nick Benton).
Submitted.
[preprint: 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).
[abstract: 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]

Non-refereed Publications

Mathematical synthesis of equational deduction systems (with Marcelo Fiore).
Marcelo's invited address at the 9th International Conference on Typed Lambda Calculi and Applications (TLCA 2009).
[abstract: pdf]

Talks

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.
[slides: pdf]
Biorthogonality, step-indexing and compiler correctness
ICFP 2009, Royall College of Physicians, Edinburgh, UK, 31 Aug 2009.
[slides: pdf]
Compiler correctness and observational equivalence on machine code.
Semantics Lunch, Computer Laboratory, Cambridge, UK, 16 Mar 2009.
[slides: pdf]
Categorical equational systems.
PhD Seminar, University of Leicester, Leicester, UK, 02 Dec 2008.
[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.
[slides: pdf]
Term equational systems and logics.
MFPS 2008, University of Pennsylvania, Philadelphia, USA, 24 May 2008.
[slides: pdf]
Term equational rewrite systems and logics.
Semantics Lunch, Computer Laboratory, Cambridge, UK, 11 Feb 2008.
[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.
[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.
[slides: pdf]
Abstract models for structural data and its substitution.
Extreme Theory Meeting, Computer Laboratory, Cambridge, UK, 19 Oct 2005.

Last modified: 4 Nov 2009