Travelled to:1 × Brazil
1 × Czech Republic
1 × Italy
1 × Poland
2 × Canada
2 × United Kingdom
3 × USA
Collaborated with:D.Dreyer V.Vafeiadis M.P.Fiore J.Kang J.Lee G.Neis N.P.Lopes N.Benton Yoonseung Kim O.Lahav Youngju Song S.Zdancewic J.Regehr Yonghyun Kim A.V.Nori S.K.Rajamani S.Samuel Christopher Pulte J.Pichon-Pharabod Sung Hwan Lee J.Kaiser C.McLaughlin W.Mansky D.Garbuzov R.J.0002 Zhengyang Liu M.Cho Dongjoo Kim L.Xia Yannick Zakowski Paul He G.Malecha B.C.Pierce S.Das David Majnemer Sanghoon Park Mark Dongyeon Shin S.Cho Joonwon Choi K.Yi
Talks about:verifi (4) compil (4) logic (4) llvm (4) equat (3) lightweight (2) program (2) concurr (2) assembl (2) system (2)
Person: Chung-Kil Hur
DBLP: Hur:Chung=Kil
Contributed to:
2015
20152014
20132012
20112011
20102009
2009
2007
2019
2018201620172017201820192020Wrote 21 papers:
- ICFP-2015-NeisHKMDV #compilation #higher-order #imperative #named
- Pilsner: a compositionally verified compiler for a higher-order imperative language (GN, CKH, JOK, CM, DD, VV), pp. 166–178.
- PLDI-2015-KangHMGZV #c #memory management
- A formal C memory model supporting integer-pointer casts (JK, CKH, WM, DG, SZ, VV), pp. 326–335.
- PLDI-2014-HurNRS #probability #slicing #source code
- Slicing probabilistic programs (CKH, AVN, SKR, SS), p. 16.
- POPL-2013-HurNDV #induction #power of #proving
- The power of parameterization in coinductive proof (CKH, GN, DD, VV), pp. 193–206.
- POPL-2012-HurDNV #bisimulation #logic
- The marriage of bisimulations and Kripke logical relations (CKH, DD, GN, VV), pp. 59–72.
- LICS-2011-HurDV #garbage collection #logic
- Separation Logic in the Presence of Garbage Collection (CKH, DD, VV), pp. 247–256.
- POPL-2011-HurD #assembly #logic #ml
- A kripke logical relation between ML and assembly (CKH, DD), pp. 133–146.
- CSL-2010-FioreH #equation #higher-order #logic
- Second-Order Equational Logic (MPF, CKH), pp. 320–335.
- ICFP-2009-BentonH #compilation #correctness
- Biorthogonality, step-indexing and compiler correctness (NB, CKH), pp. 97–108.
- TLCA-2009-FioreH #deduction #equation #synthesis
- Mathematical Synthesis of Equational Deduction Systems (MPF, CKH), pp. 1–2.
- ICALP-2007-FioreH #equation
- Equational Systems and Free Constructions (MPF, CKH), pp. 607–618.
- CAV-2019-LeeHL #named #optimisation #verification
- AliveInLean: A Verified LLVM Peephole Optimization Verifier (JL, CKH, NPL), pp. 445–455.
- OOPSLA-2018-LeeHJLRL #low level #optimisation
- Reconciling high-level optimizations and low-level code in LLVM (JL, CKH, RJ0, ZL, JR, NPL), p. 28.
- POPL-2016-KangKHDV #compilation #lightweight #verification
- Lightweight verification of separate compilation (JK, YK, CKH, DD, VV), pp. 178–190.
- PLDI-2017-LahavVKHD #consistency
- Repairing sequential consistency in C/C++11 (OL, VV, JK, CKH, DD), pp. 618–632.
- PLDI-2017-LeeKSHDMRL #behaviour
- Taming undefined behavior in LLVM (JL, YK, YS, CKH, SD, DM, JR, NPL), pp. 633–647.
- POPL-2017-KangHLVD #concurrent #semantics
- A promising semantics for relaxed-memory concurrency (JK, CKH, OL, VV, DD), pp. 175–189.
- PLDI-2018-KangKSLPSKCCHY #compilation #named
- Crellvm: verified credible compilation for LLVM (JK, YK, YS, JL, SP, MDS, YK, SC, JC, CKH, KY), pp. 631–645.
- PLDI-2019-PultePKLH #concurrent #named #performance
- Promising-ARM/RISC-V: a simpler and faster operational concurrency model (CP, JPP, JK, SHL, CKH), pp. 1–15.
- POPL-2020-SongCKKKH #composition #lightweight #named #verification
- CompCertM: CompCert with C-assembly linking and lightweight modular verification (YS, MC, DK, YK, JK, CKH), p. 31.
- POPL-2020-XiaZHHMPZ #coq #interactive #recursion #representation #source code
- Interaction trees: representing recursive and impure programs in Coq (LyX, YZ, PH, CKH, GM, BCP, SZ), p. 32.