Equational Systems and Free Constructions (Extended Abstract). - Marcelo P. Fiore; Chung-Kil Hur (ICALP, 2007)

Term Equational Systems and Logics: (Extended Abstract). - Marcelo P. Fiore; Chung-Kil Hur (MFPS, 2008)

Biorthogonality, step-indexing and compiler correctness. - Nick Benton; Chung-Kil Hur (ICFP, 2009)

Mathematical Synthesis of Equational Deduction Systems. - Marcelo P. Fiore; Chung-Kil Hur (TLCA, 2009)

On the construction of free algebras for equational systems. - Marcelo P. Fiore; Chung-Kil Hur (Theor. Comput. Sci., 2009)

Second-Order Equational Logic (Extended Abstract). - Marcelo P. Fiore; Chung-Kil Hur (CSL, 2010)

Step-Indexing: The Good, the Bad and the Ugly. - Nick Benton; Chung-Kil Hur (Modelling, Controlling and Reasoning About State, 2010)

Categorical equational systems : algebraic models and equational reasoning. - Chung-Kil Hur (2010)

Separation Logic in the Presence of Garbage Collection. - Chung-Kil Hur; Derek Dreyer; Viktor Vafeiadis (LICS, 2011)

A kripke logical relation between ML and assembly. - Chung-Kil Hur; Derek Dreyer (POPL, 2011)

On the mathematical synthesis of equational logics - Marcelo P. Fiore; Chung-Kil Hur (Log. Methods Comput. Sci., 2011)

The marriage of bisimulations and Kripke logical relations. - Chung-Kil Hur; Derek Dreyer; Georg Neis; Viktor Vafeiadis (POPL, 2012)

Strongly Typed Term Representations in Coq. - Nick Benton; Chung-Kil Hur; Andrew Kennedy; Conor McBride (J. Autom. Reason., 2012)

The power of parameterization in coinductive proof. - Chung-Kil Hur; Georg Neis; Derek Dreyer; Viktor Vafeiadis (POPL, 2013)

R2: An Efficient MCMC Sampler for Probabilistic Programs. - Aditya V. Nori; Chung-Kil Hur; Sriram K. Rajamani; Selva Samuel (AAAI, 2014)

Slicing probabilistic programs. - Chung-Kil Hur; Aditya V. Nori; Sriram K. Rajamani; Selva Samuel (PLDI, 2014)

A Provably Correct Sampler for Probabilistic Programs. - Chung-Kil Hur; Aditya V. Nori; Sriram K. Rajamani; Selva Samuel (FSTTCS, 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 (ICFP, 2015)

A formal C memory model supporting integer-pointer casts. - Jeehoon Kang; Chung-Kil Hur; William Mansky; Dmitri Garbuzov; Steve Zdancewic; Viktor Vafeiadis (PLDI, 2015)

Lightweight verification of separate compilation. - Jeehoon Kang; Yoonseung Kim; Chung-Kil Hur; Derek Dreyer; Viktor Vafeiadis (POPL, 2016)

Repairing sequential consistency in C/C++11. - Ori Lahav 001; Viktor Vafeiadis; Jeehoon Kang; Chung-Kil Hur; Derek Dreyer (PLDI, 2017)

Taming undefined behavior in LLVM. - Juneyoung Lee; Yoonseung Kim; Youngju Song; Chung-Kil Hur; Sanjoy Das; David Majnemer; John Regehr; Nuno P. Lopes (PLDI, 2017)

A promising semantics for relaxed-memory concurrency. - Jeehoon Kang; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis; Derek Dreyer (POPL, 2017)

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 (PLDI, 2018)

Reconciling high-level optimizations and low-level code in LLVM. - Juneyoung Lee; Chung-Kil Hur; Ralf Jung 002; Zhengyang Liu 003; John Regehr; Nuno P. Lopes (Proc. ACM Program. Lang., 2018)

AliveInLean: A Verified LLVM Peephole Optimization Verifier. - Juneyoung Lee; Chung-Kil Hur; Nuno P. Lopes (CAV (2), 2019)

Promising-ARM/RISC-V: a simpler and faster operational concurrency model. - Christopher Pulte; Jean Pichon-Pharabod; Jeehoon Kang; Sung-Hwan Lee 001; Chung-Kil Hur (PLDI, 2019)

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). - Li-yao Xia; Yannick Zakowski; Paul He; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (CoRR, 2019)

An equational theory for weak bisimulation via generalized parameterized coinduction. - Yannick Zakowski; Paul He; Chung-Kil Hur; Steve Zdancewic (CPP, 2020)

Promising 2.0: global optimizations in relaxed memory concurrency. - Sung-Hwan Lee 001; Minki Cho; Anton Podkopaev; Soham Chakraborty 001; Chung-Kil Hur; Ori Lahav 001; Viktor Vafeiadis (PLDI, 2020)

CompCertM: CompCert with C-assembly linking and lightweight modular verification. - Youngju Song; Minki Cho; Dongjoo Kim; Yonghyun Kim; Jeehoon Kang; Chung-Kil Hur (Proc. ACM Program. Lang., 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 (Proc. ACM Program. Lang., 2020)

An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation. - Juneyoung Lee; Dongjoo Kim; Chung-Kil Hur; Nuno P. Lopes (CAV (2), 2021)

Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. - Simon Foster 001; Chung-Kil Hur; Jim Woodcock 001 (CONCUR, 2021)

Modular data-race-freedom guarantees in the promising semantics. - Minki Cho; Sung-Hwan Lee 001; Chung-Kil Hur; Ori Lahav 001 (PLDI, 2021)

Alive2: bounded translation validation for LLVM. - Nuno P. Lopes; Juneyoung Lee; Chung-Kil Hur; Zhengyang Liu 003; John Regehr (PLDI, 2021)

Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic. - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur (CoRR, 2021)

Sequential reasoning for optimizing compilers under weak memory concurrency. - Minki Cho; Sung-Hwan Lee 001; Dongjae Lee; Chung-Kil Hur; Ori Lahav 001 (PLDI, 2022)

Conditional Contextual Refinement (CCR). - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur (CoRR, 2022)

Putting Weak Memory in Order via a Promising Intermediate Representation. - Sung-Hwan Lee 001; Minki Cho; Roy David Margalit; Chung-Kil Hur; Ori Lahav 001 (Proc. ACM Program. Lang., 2023)

Fair Operational Semantics. - Dongjae Lee; Minki Cho; Jinwoo Kim; Soonwon Moon; Youngju Song; Chung-Kil Hur (Proc. ACM Program. Lang., 2023)

Conditional Contextual Refinement. - Youngju Song; Minki Cho; Dongjae Lee; Chung-Kil Hur; Michael Sammler; Derek Dreyer (Proc. ACM Program. Lang., 2023)

CRIS: The Power of Imagination in Specification and Verification (Invited Talk). - Chung-Kil Hur (CPP, 2025)

Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting. - Yonghyun Kim; Minki Cho; Jaehyung Lee; Jinwoo Kim; Taeyoung Yoon; Youngju Song; Chung-Kil Hur (Proc. ACM Program. Lang., 2025)

VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems. - Yoonseung Kim; Sung-Hwan Lee 001; Yonghyun Kim; Chung-Kil Hur (Proc. ACM Program. Lang., 2025)

Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness. - Dongjae Lee; Janggun Lee; Taeyoung Yoon; Minki Cho; Jeehoon Kang; Chung-Kil Hur (Proc. ACM Program. Lang., 2025)

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL. - Simon Foster 001; Chung-Kil Hur; Jim Woodcock 001 (ACM Trans. Softw. Eng. Methodol., 2025)