Chung-Kil Hur

According to our database, Chung-Kil Hur authored at least 43 papers between 2007 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL.

Simon Foster, Chung-Kil Hur, Jim Woodcock

CoRR, 2024

2023

Conditional Contextual Refinement.

Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer

Proc. ACM Program. Lang., January, 2023

Fair Operational Semantics.

Dongjae Lee, Minki Cho, Jinwoo Kim, Soonwon Moon, Youngju Song, Chung-Kil Hur

Proc. ACM Program. Lang., 2023

Putting Weak Memory in Order via a Promising Intermediate Representation.

Sung-Hwan Lee, Minki Cho, Roy Margalit, Chung-Kil Hur, Ori Lahav

Proc. ACM Program. Lang., 2023

2022

Conditional Contextual Refinement (CCR).

Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur

CoRR, 2022

Sequential reasoning for optimizing compilers under weak memory concurrency.

Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic.

Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur

CoRR, 2021

Alive2: bounded translation validation for LLVM.

Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Modular data-race-freedom guarantees in the promising semantics.

Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 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, 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 Computer Aided Verification - 33rd International Conference, 2021

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

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

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 International Conference on Programming Language Design and Implementation, 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, 2020

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

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, 2019

AliveInLean: A Verified LLVM Peephole Optimization Verifier.

Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

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

Proc. ACM Program. Lang., 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

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

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 Symposium on Principles of Programming Languages, 2017

Taming undefined behavior in LLVM.

Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, Nuno P. Lopes

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 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, 2017

2016

Lightweight verification of separate compilation.

Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

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, 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, 2015

A Provably Correct Sampler for Probabilistic Programs.

Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel

Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

2014

Slicing probabilistic programs.

Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

R2: An Efficient MCMC Sampler for Probabilistic Programs.

Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, Selva Samuel

Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, 2014

2013

The power of parameterization in coinductive proof.

Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

2012

Strongly Typed Term Representations in Coq.

Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride

J. Autom. Reason., 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, 2012

2011

On the mathematical synthesis of equational logics

Marcelo P. Fiore, Chung-Kil Hur

Log. Methods Comput. Sci., 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, 2011

Separation Logic in the Presence of Garbage Collection.

Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010

Categorical equational systems : algebraic models and equational reasoning.

Chung-Kil Hur

PhD thesis, 2010

Step-Indexing: The Good, the Bad and the Ugly.

Nick Benton, Chung-Kil Hur

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

Second-Order Equational Logic (Extended Abstract).

Marcelo P. Fiore, Chung-Kil Hur

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

On the construction of free algebras for equational systems.

Marcelo P. Fiore, Chung-Kil Hur

Theor. Comput. Sci., 2009

Mathematical Synthesis of Equational Deduction Systems.

Marcelo P. Fiore, Chung-Kil Hur

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

Biorthogonality, step-indexing and compiler correctness.

Nick Benton, Chung-Kil Hur

Proceedings of the Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, 2009

2008

Term Equational Systems and Logics: (Extended Abstract).

Marcelo P. Fiore, Chung-Kil Hur

Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics, 2008

2007

Equational Systems and Free Constructions (Extended Abstract).

Marcelo P. Fiore, Chung-Kil Hur

Proceedings of the Automata, Languages and Programming, 34th International Colloquium, 2007