Chung-Kil Hur

ORCID

Publication Activity (10 Years)

Years Active: 2007-2023
Publications (10 Years): 25

Top Venues

PLDI

Proc. ACM Program. Lang.

CoRR

POPL

University of Cambridge, UK (PHD)

Education History

University of Cambridge, UK

PHD

Publications

Dongjae Lee, Minki Cho, Jinwoo Kim, Soonwon Moon, Youngju Song, Chung-Kil Hur
Fair Operational Semantics. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav
Putting Weak Memory in Order via a Promising Intermediate Representation. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer
Conditional Contextual Refinement. Proc. ACM Program. Lang. 7 (POPL) (2023)
Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav
Sequential reasoning for optimizing compilers under weak memory concurrency. PLDI (2022)
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur
Conditional Contextual Refinement (CCR). CoRR (2022)
Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr
Alive2: bounded translation validation for LLVM. PLDI (2021)
Simon Foster, Chung-Kil Hur, Jim Woodcock
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. CoRR (2021)
Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur
Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic. CoRR (2021)
Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav
Modular data-race-freedom guarantees in the promising semantics. PLDI (2021)
Juneyoung Lee, Dongjoo Kim, Chung-Kil Hur, Nuno P. Lopes
An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation. CAV (2) (2021)
Simon Foster, Chung-Kil Hur, Jim Woodcock
Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. CONCUR (2021)
Youngju Song, Minki Cho, Dongjoo Kim, Yonghyun Kim, Jeehoon Kang, Chung-Kil Hur
CompCertM: CompCert with C-assembly linking and lightweight modular verification. Proc. ACM Program. Lang. 4 (POPL) (2020)
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4 (POPL) (2020)
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
An equational theory for weak bisimulation via generalized parameterized coinduction. CPP (2020)
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction. CoRR (2020)
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
Promising 2.0: global optimizations in relaxed memory concurrency. PLDI (2020)
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). CoRR (2019)
Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes
AliveInLean: A Verified LLVM Peephole Optimization Verifier. CAV (2) (2019)
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung Hwan Lee, Chung-Kil Hur
Promising-ARM/RISC-V: a simpler and faster operational concurrency model. PLDI (2019)
Jeehoon Kang, Yoonseung Kim, Youngju Song, Juneyoung Lee, Sanghoon Park, Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, Kwangkeun Yi
Crellvm: verified credible compilation for LLVM. PLDI (2018)
Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, Nuno P. Lopes
Reconciling high-level optimizations and low-level code in LLVM. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer
A promising semantics for relaxed-memory concurrency. POPL (2017)
Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, Nuno P. Lopes
Taming undefined behavior in LLVM. PLDI (2017)
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer
Repairing sequential consistency in C/C++11. PLDI (2017)
Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
Lightweight verification of separate compilation. POPL (2016)
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
A formal C memory model supporting integer-pointer casts. PLDI (2015)
Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel
A Provably Correct Sampler for Probabilistic Programs. FSTTCS (2015)
Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis
Pilsner: a compositionally verified compiler for a higher-order imperative language. ICFP (2015)
Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, Selva Samuel
R2: An Efficient MCMC Sampler for Probabilistic Programs. AAAI (2014)
Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel
Slicing probabilistic programs. PLDI (2014)
Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis
The power of parameterization in coinductive proof. POPL (2013)
Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride
Strongly Typed Term Representations in Coq. J. Autom. Reason. 49 (2) (2012)
Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis
The marriage of bisimulations and Kripke logical relations. POPL (2012)
Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis
Separation Logic in the Presence of Garbage Collection. LICS (2011)
Marcelo P. Fiore, Chung-Kil Hur
On the mathematical synthesis of equational logics Log. Methods Comput. Sci. 7 (3) (2011)
Chung-Kil Hur, Derek Dreyer
A kripke logical relation between ML and assembly. POPL (2011)
Nick Benton, Chung-Kil Hur
Step-Indexing: The Good, the Bad and the Ugly. Modelling, Controlling and Reasoning About State (2010)
Marcelo P. Fiore, Chung-Kil Hur
Second-Order Equational Logic (Extended Abstract). CSL (2010)
Nick Benton, Chung-Kil Hur
Biorthogonality, step-indexing and compiler correctness. ICFP (2009)
Marcelo P. Fiore, Chung-Kil Hur
Mathematical Synthesis of Equational Deduction Systems. TLCA (2009)
Marcelo P. Fiore, Chung-Kil Hur
On the construction of free algebras for equational systems. Theor. Comput. Sci. 410 (18) (2009)
Marcelo P. Fiore, Chung-Kil Hur
Term Equational Systems and Logics: (Extended Abstract). MFPS (2008)
Marcelo P. Fiore, Chung-Kil Hur
Equational Systems and Free Constructions (Extended Abstract). ICALP (2007)

Chung-Kil Hur.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Chung-Kil Hur