Pointers: [2021] [2020] [2019] [2018] [2017] [2016] [2015] [2014] [2013] [2012] [2011] [2010] [2009] [2008] [2007] [PhD Theses]

“with coauthors” denotes that the authors are listed alphabetically.

2021



2020



2019



2018



2017



2016



2015



2014



2013



2012



2011



2010


  • Step-indexing: the good, the bad and the ugly.
    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] [publisher page]
  • (CSL 2010) Second-order equational logic.
    with Marcelo Fiore.
    Proceedings of the 19th EACSL Annual Conference on Computer Science Logic, August 2010.
    [paper: pdf] [publisher page]
  • (LOLA 2010) Step-indexing: the good, the bad and the ugly.
    with Nick Benton.
    Workshop on Syntax and Semantics of Low Level Languages, satellite workshop of LICS 2010, July 2010.
    [paper: pdf]
  • (Coq 2010) Heq: a Coq library for heterogeneous equality.
    Chung-Kil Hur.
    The 2nd Coq Workshop, satellite workshop of ITP 2010, July 2010.
    [paper: pdf] [coq script: script] [slides: pdf]
  • Realizability and compositional compiler correctness for a polymorphic language.
    with Nick Benton.
    Microsoft Research Technical Report MSR-TR-2010-62. May 2010.
    [paper: pdf] [coq script: zip] [publisher page]

2009


  • (WMM 2009) Strongly typed term representations in Coq.
    with Nick Benton, Andrew Kennedy.
    The 4th informal ACM SIGPLAN Workshop on Mechanizing Metatheory, September 2009.
    [paper: pdf]
  • (ICFP 2009) Biorthogonality, step-indexing and compiler correctness.
    with Nick Benton.
    Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, August 2009.
    [paper: pdf] [coq script: zip] [slides: pdf] [publisher page]
  • (TCS) On the construction of free algebras for equational systems.
    with Marcelo Fiore.
    Theoretical Computer Science, 410(18):1704-1729, April 2009.
    Special issue devoted to selected papers from ICALP 2007.
    [paper: pdf] [publisher page]

2008


  • (MFPS 2008) Term equational systems and logics.
    with Marcelo Fiore.
    Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics, May 2008.
    [paper: pdf] [slides: pdf] [publisher page]

2007


  • (ICALP 2007) Equational systems and free constructions.
    with Marcelo Fiore.
    Proceedings of the 34th International Colloquium on Automata, Languages and Programming, July 2007.
    [paper: pdf] [errata: pdf] [slides: pdf] [publisher page]

PhD Theses


  • A Validated Semantics for LLVM IR.
    Juneyoung Lee.
    Department of Computer Science and Engineering, Seoul National University, Korea, 2021
    [thesis: pdf] [project page]
  • RUSC and CompCertM: A new foundation for modular verification and its application to compiler verification.
    Youngju Song.
    Department of Computer Science and Engineering, Seoul National University, Korea, 2021
    [thesis: pdf] [project page]
  • Reconciling low-level features of C with compiler optimizations.
    Jeehoon Kang.
    Department of Computer Science and Engineering, Seoul National University, Korea, 2019
    [thesis: pdf] [project page]
  • Categorical equational systems: algebraic models and equational reasoning.
    Chung-Kil Hur.
    Computer Laboratory, University of Cambridge, UK, 2009
    [summary: pdf] [thesis: pdf] [publisher page]