Pointers: [2023] [2022] [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.

2023

• (OOPSLA 2023) Stuttering for Free.
  Minki Cho*, Youngju Song*, Dongjae Lee, Lennard Gäher, Derek Dreyer.
  * The first two authors contributed equally to this work and are listed alphabetically.
  Proceedings of the 2023 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 2023.
  [paper: pdf] [project page] [publisher page]
• (PLDI 2023) Fair Operational Semantics.
  Dongjae Lee*, Minki Cho*, Jinwoo Kim, Soonwon Moon, Youngju Song, Chung-Kil Hur.
  * The first two authors contributed equally to this work.
  Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2023.
  [paper: pdf] [project page] [publisher page]
• (PLDI 2023) Putting Weak Memory in Order via a Promising Intermediate Representation.
  Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav.
  Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2023.
  [paper: pdf] [project page] [publisher page]
• (POPL 2023) Conditional Contextual Refinement.
  Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer.
  Proceedings of the 50th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2023.
  [paper: pdf] [project page] [publisher page]

2022

• (PLDI 2022) Sequential Reasoning for Optimizing Compilers under Weak Memory Concurrency.
  Minki Cho*, Sung-Hwan Lee*, Dongjae Lee, Chung-Kil Hur, Ori Lahav.
  * The first two authors contributed equally to this work.
  Proceedings of the 43rd ACM SIGPLAN conference on Programming Language Design and Implementation, June 2022.
  [paper: pdf] [project page] [publisher page]

2021

• (CONCUR 2021) Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL.
  Simon Foster, Chung-Kil Hur, Jim Woodcock.
  Proceedings of the 32nd International Conference on Concurrency Theory, Aug 2021.
  [paper: pdf] [publisher page]
• (CAV 2021) An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation.
  Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes.
  Proceedings of the 33rd International Conference on Computer-Aided Verification, July 2021.
  [paper: pdf] [slides: pdf] [publisher page]
• (PLDI 2021) Modular Data-Race-Freedom Guarantees in the Promising Semantics.
  Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav.
  Proceedings of the 42nd ACM SIGPLAN conference on Programming Language Design and Implementation, June 2021.
  [paper: pdf] [project page] [publisher page]
• (PLDI 2021) Alive2: Bounded Translation Validation for LLVM.
  Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr.
  Proceedings of the 42nd ACM SIGPLAN conference on Programming Language Design and Implementation, June 2021.
  Recipient of PLDI 2021 Distinguished Paper Award.
  [paper: pdf] [project page] [publisher page]

2020

• (PLDI 2020) Promising 2.0: Global Optimizations in Relaxed Memory Concurrency.
  Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis.
  Proceedings of the 41st ACM SIGPLAN conference on Programming Language Design and Implementation, June 2020.
  [paper: pdf] [project page] [publisher page]
• (POPL 2020) CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification.
  Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, Chung-Kil Hur.
  Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2020.
  [paper: pdf] [project page] [publisher page]
• (POPL 2020) Interaction Trees: Representing Recursive and Impure Programs in Coq.
  Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic.
  Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2020.
  Recipient of POPL 2020 Distinguished Paper Award.
  [paper: pdf] [project page] [publisher page]
• (CPP 2020) An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction.
  Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic.
  Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2020.
  [paper: pdf] [development: zip] [project page] [publisher page]

2019

• (CAV 2019, Tool Paper) AliveInLean: A Verified LLVM Peephole Optimization Verifier.
  Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes.
  Proceedings of the 31st International Conference on Computer-Aided Verification (Tool Paper), July 2019.
  [paper: pdf] [project page] [publisher page]
• (PLDI 2019) Promising-ARM/RISC-V: a simpler and faster operational concurrency model.
  Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur.
  Proceedings of the 40th ACM SIGPLAN conference on Programming Language Design and Implementation, June 2019.
  [paper: pdf] [project page] [publisher page]

2018

• (OOPSLA 2018) Reconciling High-level Optimizations and Low-level Code in LLVM.
  Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes.
  The 2018 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, November 2018.
  [paper: pdf] [project page] [publisher page]
• (PLDI 2018) Crellvm: Verified Credible Compilation for LLVM.
  Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi.
  The first three authors contributed equally and are listed alphabetically.
  Proceedings of the 39th ACM SIGPLAN conference on Programming Language Design and Implementation, June 2018.
  [paper: pdf] [project page] [publisher page]

2017

• (PLDI 2017) Taming Undefined Behavior in LLVM.
  Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das (Azul Systems), David Majnemer (Google), John Regehr, Nuno P. Lopes.
  Proceedings of the 38th ACM SIGPLAN conference on Programming Language Design and Implementation, June 2017.
  [paper: pdf] [project page] [publisher page]
• (PLDI 2017) Repairing Sequential Consistency in C/C++11.
  Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
  Proceedings of the 38th ACM SIGPLAN conference on Programming Language Design and Implementation, June 2017.
  Recipient of PLDI 2017 Distinguished Paper Award.
  [paper: pdf] [project page] [publisher page]
• (POPL 2017) A Promising Semantics for Relaxed-Memory Concurrency.
  Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
  Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2017.
  [paper with appendix: pdf] [project page] [publisher page]

2016

• (POPL 2016) Lightweight Verification of Separate Compilation.
  Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
  Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2016.
  [paper: pdf] [project page] [publisher page]

2015

• (FSTTCS 2015) A Provably Correct Sampler for Probabilistic Programs.
  Chung-Kil Hur, Aditya Nori, Sriram Rajamani, Selva Samuel.
  Proceedings of the 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, December 2015.
  [paper: pdf (the proofs are now added in the appendix.)] [publisher page]
• (ICFP 2015) Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language.
  Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis.
  Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, September 2015.
  [paper: pdf] [appendix: pdf] [coq: zip] [project page] [publisher page]
• (PLDI 2015) A Formal C Memory Model Supporting Integer-Pointer Casts.
  Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis.
  Proceedings of the 36th ACM SIGPLAN conference on Programming Language Design and Implementation, June 2015.
  [paper: pdf] [project page] [publisher page]

2014

• Towards Scalable Translation Validation of Static Analyzers.
  Jeehoon Kang, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi.
  ROSAEC Technical Report ROSAEC-2014-003, November 2014.
  [paper: pdf] [publisher page]
• An Extensible Verified Validator For Simple Optimizations in LLVM.
  Sungkeun Cho, Joonwon Choi, Jeehoon Kang, Chung-Kil Hur, Kwangkeun Yi.
  ROSAEC Technical Report ROSAEC-2014-002, September 2014.
  [paper: pdf] [publisher page]
• (AAAI 2014) R2: An Efficient MCMC Sampler for Probabilistic Programs.
  Aditya Nori, Chung-Kil Hur, Sriram Rajamani, Selva Samuel.
  Proceedings of the 28th AAAI conference on Artificial Intelligence, Oral Presentation, July 2014.
  [paper: pdf] [project page] [publisher page]
• (PLDI 2014) Slicing Probabilistic Programs.
  Chung-Kil Hur, Aditya Nori, Sriram Rajamani, Selva Samuel.
  Proceedings of the 35th ACM SIGPLAN conference on Programming Language Design and Implementation, June 2014.
  [paper: pdf] [project page] [publisher page]
• A Logical Step Forward in Parametric Bisimulations.
  Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
  MPI-SWS Technical Report MPI-SWS-2014-003, January 2014.
  [paper: pdf] [coq script: zip] [publisher page]

2013

• Semantic sensitive sampling for probabilistic programs.
  Aditya Nori, Chung-Kil Hur, Sriram Rajamani, Selva Samuel.
  Microsoft Research Technical Report MSR-TR-2013-109, October 2013.
  [paper: pdf] [publisher page]
• (POPL 2013) The power of parameterization in coinductive proof.
  Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
  Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2013.
  [paper: pdf] [slides: pdf] [coq script: zip] [publisher page]

2012

• (JAR) Strongly typed term representations in Coq.
  with Nick Benton, Andrew Kennedy, Conor McBride.
  Journal of Automated Reasoning, 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] [publisher page]
• The transitive composability of relation transition systems.
  Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
  MPI-SWS Technical Report MPI-SWS-2012-002, May 2012.
  [paper: pdf] [coq script: zip] [publisher page]
• (POPL 2012) The marriage of bisimulations and Kripke logical relations.
  Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis.
  Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2012.
  [paper: pdf] [appendix: pdf] [coq script: zip] [slides: pdf] [publisher page]

2011

• (LMCS) On the mathematical synthesis of equational logic.
  with Marcelo Fiore.
  Logical Methods in Computer Science, 7(3:12), September 2011.
  [paper: pdf] [publisher page]
• (LICS 2011) Separation logic in the presence of garbage collection.
  Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
  Proceedings of the 26th IEEE Symposium on Logic in Computer Science, June 2011.
  [paper: pdf] [appendix: pdf] [slides: pdf] [publisher page]
• (POPL 2011) A Kripke logical relation between ML and assembly.
  Chung-Kil Hur, Derek Dreyer.
  Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2011.
  [paper: pdf] [appendix: pdf] [slides: pptx (powerpoint 2010), swf (flash)] [publisher page]

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

• Understanding and Fulfilling the Desiderata for Relaxed Memory Models.
  Sung-Hwan Lee.
  Department of Computer Science and Engineering, Seoul National University, Korea, 2023
  [thesis: pdf] [project page]

• Simplifying Reasoning under Weak Memory Concurrency.
  Minki Cho.
  Department of Computer Science and Engineering, Seoul National University, Korea, 2023
  [thesis: pdf]

• Formal Verification Framework for Cyber-Physical Systems on PALSware.
  Yoonseung Kim.
  Department of Computer Science and Engineering, Seoul National University, Korea, 2021
  [thesis: pdf]

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