Chung-Kil Hur

54 papers A* 19A 2B 6Journal 21Unranked 5
YearRankTypeTitle / Venue / Authors
2026 J jnl
Coco: Corecursion with Compositional Heterogeneous Productivity.
Proc. ACM Program. Lang.
Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur
2025 J jnl
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting.
Proc. ACM Program. Lang.
Yonghyun Kim, Minki Cho, Jaehyung Lee, Jinwoo Kim, TaeYoung Yoon, Youngju Song, Chung-Kil Hur
2025 B conf
CRIS: The Power of Imagination in Specification and Verification (Invited Talk).
CPP
Chung-Kil Hur
2025 J jnl
Coco: Corecursion with Compositional Heterogeneous Productivity.
CoRR
Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur
2025 J jnl
Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness.
Proc. ACM Program. Lang.
Dongjae Lee, Janggun Lee, TaeYoung Yoon, Minki Cho, Jeehoon Kang, Chung-Kil Hur
2025 A* conf
Pfeife: Automatic Pipeline Parallelism for PyTorch.
ICML
Ho Young Jhoo, Chung-Kil Hur, Nuno P. Lopes
2025 J jnl
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL.
ACM Trans. Softw. Eng. Methodol.
Simon Foster, Chung-Kil Hur, Jim Woodcock
2025 J jnl
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems.
Proc. ACM Program. Lang.
Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, Chung-Kil Hur
2024 J jnl
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL.
CoRR
Simon Foster, Chung-Kil Hur, Jim Woodcock
2023 J jnl
Conditional Contextual Refinement.
Proc. ACM Program. Lang.
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer
2023 J jnl
Fair Operational Semantics.
Proc. ACM Program. Lang.
Dongjae Lee, Minki Cho, Jinwoo Kim, Soonwon Moon, Youngju Song, Chung-Kil Hur
2023 B ed.
Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings
APLAS
Chung-Kil Hur
2023 J jnl
Putting Weak Memory in Order via a Promising Intermediate Representation.
Proc. ACM Program. Lang.
Sung-Hwan Lee, Minki Cho, Roy David Margalit, Chung-Kil Hur, Ori Lahav
2022 J jnl
Conditional Contextual Refinement (CCR).
CoRR
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur
2022 A* conf
Sequential reasoning for optimizing compilers under weak memory concurrency.
PLDI
Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav
2021 J jnl
Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic.
CoRR
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur
2021 A* conf
Alive2: bounded translation validation for LLVM.
PLDI
Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr
2021 — conf
An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation.
CAV (2)
Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes
2021 B conf
Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL.
CONCUR
Simon Foster, Chung-Kil Hur, Jim Woodcock
2021 J jnl
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL.
CoRR
Simon Foster, Chung-Kil Hur, Jim Woodcock
2021 A* conf
Modular data-race-freedom guarantees in the promising semantics.
PLDI
Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav
2020 J jnl
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction.
CoRR
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
2020 B conf
An equational theory for weak bisimulation via generalized parameterized coinduction.
CPP
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
2020 J jnl
CompCertM: CompCert with C-assembly linking and lightweight modular verification.
Proc. ACM Program. Lang.
Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, Chung-Kil Hur
2020 J jnl
Interaction trees: representing recursive and impure programs in Coq.
Proc. ACM Program. Lang.
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2020 A* conf
Promising 2.0: global optimizations in relaxed memory concurrency.
PLDI
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
2019 — conf
AliveInLean: A Verified LLVM Peephole Optimization Verifier.
CAV (2)
Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes
2019 J jnl
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress).
CoRR
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
2019 A* conf
Promising-ARM/RISC-V: a simpler and faster operational concurrency model.
PLDI
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur
2018 A* conf
Crellvm: verified credible compilation for LLVM.
PLDI
Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi
2018 J jnl
Reconciling high-level optimizations and low-level code in LLVM.
Proc. ACM Program. Lang.
Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes
2017 A* conf
A promising semantics for relaxed-memory concurrency.
POPL
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
2017 A* conf
Repairing sequential consistency in C/C++11.
PLDI
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
2017 A* conf
Taming undefined behavior in LLVM.
PLDI
Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, Nuno P. Lopes
2016 A* conf
Lightweight verification of separate compilation.
POPL
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2015 — conf
A Provably Correct Sampler for Probabilistic Programs.
FSTTCS
Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel
2015 A* conf
A formal C memory model supporting integer-pointer casts.
PLDI
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
2015 A conf
Pilsner: a compositionally verified compiler for a higher-order imperative language.
ICFP
Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis
2014 A* conf
R2: An Efficient MCMC Sampler for Probabilistic Programs.
AAAI
Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, Selva Samuel
2014 A* conf
Slicing probabilistic programs.
PLDI
Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel
2013 A* conf
The power of parameterization in coinductive proof.
POPL
Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
2012 J jnl
Strongly Typed Term Representations in Coq.
J. Autom. Reason.
Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride
2012 A* conf
The marriage of bisimulations and Kripke logical relations.
POPL
Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
2011 A* conf
A kripke logical relation between ML and assembly.
POPL
Chung-Kil Hur, Derek Dreyer
2011 J jnl
On the mathematical synthesis of equational logics
Log. Methods Comput. Sci.
Marcelo P. Fiore, Chung-Kil Hur
2011 A* conf
Separation Logic in the Presence of Garbage Collection.
LICS
Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
2010 — —
Categorical equational systems : algebraic models and equational reasoning.
Chung-Kil Hur
2010 B conf
Second-Order Equational Logic (Extended Abstract).
CSL
Marcelo P. Fiore, Chung-Kil Hur
2010 — conf
Step-Indexing: The Good, the Bad and the Ugly.
Modelling, Controlling and Reasoning About State
Nick Benton, Chung-Kil Hur
2009 A conf
Biorthogonality, step-indexing and compiler correctness.
ICFP
Nick Benton, Chung-Kil Hur
2009 — conf
Mathematical Synthesis of Equational Deduction Systems.
TLCA
Marcelo P. Fiore, Chung-Kil Hur
2009 J jnl
On the construction of free algebras for equational systems.
Theor. Comput. Sci.
Marcelo P. Fiore, Chung-Kil Hur
2008 B conf
Term Equational Systems and Logics: (Extended Abstract).
MFPS
Marcelo P. Fiore, Chung-Kil Hur
2007 A* conf
Equational Systems and Free Constructions (Extended Abstract).
ICALP
Marcelo P. Fiore, Chung-Kil Hur