BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Hur:Chung=Kil

Contributed to:

ICFP 20152015
PLDI 20152015
PLDI 20142014
POPL 20132013
POPL 20122012
LICS 20112011
POPL 20112011
CSL 20102010
ICFP 20092009
TLCA 20092009
ICALP 20072007
CAV (2) 20192019
OOPSLA 20182018
POPL 20162016
PLDI 20172017
POPL 20172017
PLDI 20182018
PLDI 20192019
POPL 20202020

Wrote 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.