Подписаться
Chung-Kil Hur
Chung-Kil Hur
Seoul National University
Подтвержден адрес электронной почты в домене sf.snu.ac.kr - Главная страница
Название
Процитировано
Процитировано
Год
Repairing sequential consistency in C/C++ 11
O Lahav, V Vafeiadis, J Kang, CK Hur, D Dreyer
ACM SIGPLAN Notices 52 (6), 618-632, 2017
2622017
A promising semantics for relaxed-memory concurrency
J Kang, CK Hur, O Lahav, V Vafeiadis, D Dreyer
ACM SIGPLAN Notices 52 (1), 175-189, 2017
2432017
Interaction trees: representing recursive and impure programs in Coq
L Xia, Y Zakowski, P He, CK Hur, G Malecha, BC Pierce, S Zdancewic
Proceedings of the ACM on Programming Languages 4 (POPL), 1-32, 2019
1952019
Biorthogonality, step-indexing and compiler correctness
N Benton, CK Hur
ACM Sigplan Notices 44 (9), 97-108, 2009
1442009
R2: An efficient MCMC sampler for probabilistic programs
A Nori, CK Hur, S Rajamani, S Samuel
Proceedings of the AAAI Conference on Artificial Intelligence 28 (1), 2014
1412014
The power of parameterization in coinductive proof
CK Hur, G Neis, D Dreyer, V Vafeiadis
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013
1412013
A Kripke logical relation between ML and assembly
CK Hur, D Dreyer
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2011
1192011
Strongly typed term representations in Coq
N Benton, CK Hur, AJ Kennedy, C McBride
Journal of automated reasoning 49 (2), 141-159, 2012
1172012
Pilsner: A compositionally verified compiler for a higher-order imperative language
G Neis, CK Hur, JO Kaiser, C McLaughlin, D Dreyer, V Vafeiadis
Proceedings of the 20th ACM SIGPLAN International Conference on Functional …, 2015
1042015
Alive2: bounded translation validation for LLVM
NP Lopes, J Lee, CK Hur, Z Liu, J Regehr
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021
1002021
The marriage of bisimulations and Kripke logical relations
CK Hur, D Dreyer, G Neis, V Vafeiadis
ACM SIGPLAN Notices 47 (1), 59-72, 2012
1002012
Taming undefined behavior in LLVM
J Lee, Y Kim, Y Song, CK Hur, S Das, D Majnemer, J Regehr, NP Lopes
ACM SIGPLAN Notices 52 (6), 633-647, 2017
912017
Second-order equational logic
M Fiore, CK Hur
Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual …, 2010
882010
Lightweight verification of separate compilation
J Kang, Y Kim, CK Hur, D Dreyer, V Vafeiadis
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2016
792016
A formal C memory model supporting integer-pointer casts
J Kang, CK Hur, W Mansky, D Garbuzov, S Zdancewic, V Vafeiadis
ACM SIGPLAN Notices 50 (6), 326-335, 2015
792015
Promising 2.0: global optimizations in relaxed memory concurrency
SH Lee, M Cho, A Podkopaev, S Chakraborty, CK Hur, O Lahav, ...
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020
702020
Promising-ARM/RISC-V: a simpler and faster operational concurrency model
C Pulte, J Pichon-Pharabod, J Kang, SH Lee, CK Hur
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019
662019
Slicing probabilistic programs
CK Hur, AV Nori, SK Rajamani, S Samuel
ACM SIGPLAN Notices 49 (6), 133-144, 2014
652014
CompCertM: CompCert with C-assembly linking and lightweight modular verification
Y Song, M Cho, D Kim, Y Kim, J Kang, CK Hur
Proceedings of the ACM on Programming Languages 4 (POPL), 1-31, 2019
482019
Crellvm: verified credible compilation for LLVM
J Kang, Y Kim, Y Song, J Lee, S Park, MD Shin, Y Kim, S Cho, J Choi, ...
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018
462018
В данный момент система не может выполнить эту операцию. Повторите попытку позднее.
Статьи 1–20