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