default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDChung-Kil Hur
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[i7]Simon Foster, Chung-Kil Hur, Jim Woodcock:
Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL. CoRR abs/2408.15817 (2024)- 2023
- [j9]Dongjae Lee
, Minki Cho, Jinwoo Kim, Soonwon Moon, Youngju Song, Chung-Kil Hur:
Fair Operational Semantics. Proc. ACM Program. Lang. 7(PLDI): 811-834 (2023) - [j8]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): 1872-1895 (2023) - [j7]Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, Derek Dreyer:
Conditional Contextual Refinement. Proc. ACM Program. Lang. 7(POPL): 1121-1151 (2023) - [e1]Chung-Kil Hur:
Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings. Lecture Notes in Computer Science 14405, Springer 2023, ISBN 978-981-99-8310-0 [contents] - 2022
- [c28]Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav:
Sequential reasoning for optimizing compilers under weak memory concurrency. PLDI 2022: 213-228 - [i6]Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur:
Conditional Contextual Refinement (CCR). CoRR abs/2203.07431 (2022) - 2021
- [c27]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: 752-776 - [c26]Simon Foster, Chung-Kil Hur, Jim Woodcock:
Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. CONCUR 2021: 20:1-20:18 - [c25]Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr:
Alive2: bounded translation validation for LLVM. PLDI 2021: 65-79 - [c24]Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav:
Modular data-race-freedom guarantees in the promising semantics. PLDI 2021: 867-882 - [i5]Simon Foster, Chung-Kil Hur, Jim Woodcock:
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. CoRR abs/2105.05133 (2021) - [i4]Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur:
Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic. CoRR abs/2109.02991 (2021) - 2020
- [j6]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): 23:1-23:31 (2020) - [j5]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): 51:1-51:32 (2020) - [c23]Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic:
An equational theory for weak bisimulation via generalized parameterized coinduction. CPP 2020: 71-84 - [c22]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: 362-376 - [i3]Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic:
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction. CoRR abs/2001.02659 (2020)
2010 – 2019
- 2019
- [c21]Juneyoung Lee, Chung-Kil Hur, Nuno P. Lopes:
AliveInLean: A Verified LLVM Peephole Optimization Verifier. CAV (2) 2019: 445-455 - [c20]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: 1-15 - [i2]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 abs/1906.00046 (2019) - 2018
- [j4]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): 125:1-125:28 (2018) - [c19]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: 631-645 - 2017
- [c18]Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer:
Repairing sequential consistency in C/C++11. PLDI 2017: 618-632 - [c17]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: 633-647 - [c16]Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer:
A promising semantics for relaxed-memory concurrency. POPL 2017: 175-189 - 2016
- [c15]Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis:
Lightweight verification of separate compilation. POPL 2016: 178-190 - 2015
- [c14]Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel:
A Provably Correct Sampler for Probabilistic Programs. FSTTCS 2015: 475-488 - [c13]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: 166-178 - [c12]Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis:
A formal C memory model supporting integer-pointer casts. PLDI 2015: 326-335 - 2014
- [c11]Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, Selva Samuel:
R2: An Efficient MCMC Sampler for Probabilistic Programs. AAAI 2014: 2476-2482 - [c10]Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, Selva Samuel:
Slicing probabilistic programs. PLDI 2014: 133-144 - 2013
- [c9]Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis:
The power of parameterization in coinductive proof. POPL 2013: 193-206 - 2012
- [j3]Nick Benton, Chung-Kil Hur, Andrew Kennedy, Conor McBride:
Strongly Typed Term Representations in Coq. J. Autom. Reason. 49(2): 141-159 (2012) - [c8]Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis:
The marriage of bisimulations and Kripke logical relations. POPL 2012: 59-72 - 2011
- [j2]Marcelo P. Fiore, Chung-Kil Hur:
On the mathematical synthesis of equational logics. Log. Methods Comput. Sci. 7(3) (2011) - [c7]Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis:
Separation Logic in the Presence of Garbage Collection. LICS 2011: 247-256 - [c6]Chung-Kil Hur, Derek Dreyer:
A kripke logical relation between ML and assembly. POPL 2011: 133-146 - 2010
- [b1]Chung-Kil Hur:
Categorical equational systems : algebraic models and equational reasoning. University of Cambridge, UK, 2010 - [c5]Marcelo P. Fiore, Chung-Kil Hur:
Second-Order Equational Logic (Extended Abstract). CSL 2010: 320-335 - [i1]Nick Benton, Chung-Kil Hur:
Step-Indexing: The Good, the Bad and the Ugly. Modelling, Controlling and Reasoning About State 2010
2000 – 2009
- 2009
- [j1]Marcelo P. Fiore, Chung-Kil Hur:
On the construction of free algebras for equational systems. Theor. Comput. Sci. 410(18): 1704-1729 (2009) - [c4]Nick Benton, Chung-Kil Hur:
Biorthogonality, step-indexing and compiler correctness. ICFP 2009: 97-108 - [c3]Marcelo P. Fiore, Chung-Kil Hur:
Mathematical Synthesis of Equational Deduction Systems. TLCA 2009: 1-2 - 2008
- [c2]Marcelo P. Fiore, Chung-Kil Hur:
Term Equational Systems and Logics: (Extended Abstract). MFPS 2008: 171-192 - 2007
- [c1]Marcelo P. Fiore, Chung-Kil Hur:
Equational Systems and Free Constructions (Extended Abstract). ICALP 2007: 607-618
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:21 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
