SFlab
Professor, Department of Computer Science and Engineering
Adjunct Professor, Department of Mathematical Sciences

Address
Department of Computer Science and Engineering
Seoul National University
1 Gwanak-ro, Gwanak-gu, Seoul 08826, Republic of Korea

Email: gil.hur#sf:snu:ac:kr where # is @ and : is .

Tel: +82 (0)2 880 1844
I am charing the Program Committee of APLAS 2023, which will take place on 26-29 November 2023 in Taipei, Taiwan.
Submit your papers by 15 June 2023, AoE!

Research Interests


Programming Languages in general. Specifically:
  • Relaxed Memory Concurrency
  • Semantics of Low-level Languages (LLVM, C/C++, Rust)
  • Software (esp. Compiler) Verification
  • Program Logic
  • Interactive Theorem Proving
  • Probabilistic Programs & Bayesian Inference
  • Category Theory

Education


  • 10.2004 ~ 10.2009 : Ph.D. in Computer Science at University of Cambridge (Supervisor: Marcelo Fiore).
  • 03.1995 ~ 02.2000 : B.S. in Mathematics and Computer Science at KAIST.

Research Experience


Honors and Awards


Professional Activities


Software


  • Heq
    A Coq library to support reasoning about Heterogeneous Equality.
  • Hpattern
    A generalized version of the tactic ‘pattern’ in Coq.
  • Paco
    A Coq library for parameterized coinduction.
  • R2 Project
    Bayesian inference system for probabilistic programs.
  • SepCompCert
    Verification of separate compilation of CompCert

Teaching


See Courses.

Research Advisees


See People.

Publications


See Publications.

Talks


Not updated since 2013.
  • The power of parameterization in coinductive proof. [slides: pdf]
  • Compositional inter-language relational verification (using interactive theorem prover).
    Seoul National University, Seoul, Korea, 10 Dec 2012.
  • The power of parameterization in coinductive proof.
    Semantics Lunch Seminar, University of Cambridge, Cambridge, UK, 22 Oct 2012.
  • Compositional inter-language relational verification.
    • Yale University, New Haven, USA, 14 May 2012.
    • KAIST, Daejeon, Korea, 23 Apr 2012.
    • University of Colorado at Boulder, Boulder, USA, 13 Apr 2012.
    • Microsoft Research Cambridge, Cambridge, UK, 30 Mar 2012.
  • Compositional software verification.
    Seoul National University, Seoul, Korea, 16 Dec 2011.
  • The marriage of bisimulations and Kripke logical relations.
    ROPAS Weekly Show & Tell, Seoul National University, Seoul, Korea, 9 Sep 2011.
  • A Kripke logical relation between ML and assembly.
    • PL/Verification Seminar, MPI-SWS, Saarbrücken, Germany, 25 Feb 2011.
    • POPL 2011, Austin, USA, 26 Jan 2011.
    [abstract: txt] [slides: pptx (powerpoint 2010)]
  • A Kripke logical relation between ML and assembly.
    Dagstuhl Seminar: Modelling, Controlling and Reasoning About State, Schloss Dagstuhl, Germany, 1 Sep 2010.
    [abstract: txt] [slides: pdf]
  • Heq: a Coq library for heterogeneous equality.
    Coq Workshop 2010, Edinburgh, U.K., 9 Jul 2010.
    [abstract: txt] [slides: pdf]
  • Program equivalence and compositional compiler correctness.
    Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany, 22 Mar 2010.
    [abstract: txt] [slides: pdf]
  • Observational equivalence on low-level programs and compositional compiler correctness.
    Type theory and realizability, PPS, Paris, France, 2 Dec 2009.
    [abstract: txt] [slides: pdf]
  • Logical relations and compositional compiler correctness.
    • ROSAEC Center Seminar, Seoul National University, Seoul, Korea, 14 Oct 2009.
    • Programming Languages Laboratory Seminar, KAIST, Daejeon, Korea, 21 Oct 2009.
    [abstract: txt] [slides: pdf]
  • Biorthogonality, step-indexing and compiler correctness.
    ICFP 2009, Royall College of Physicians, Edinburgh, UK, 31 Aug 2009.
    [abstract: txt] [slides: pdf]
  • Compiler correctness and observational equivalence on machine code.
    Semantics Lunch, Computer Laboratory, Cambridge, UK, 16 Mar 2009.
    [abstract: txt] [slides: pdf]
  • Categorical equational systems.
    PhD Seminar, University of Leicester, Leicester, UK, 02 Dec 2008.
    [abstract: txt] [slides: pdf]
  • Term equational systems and logics.
    • KAIST Discrete Math Seminar, KAIST, Daejeon, Korea, 11 Aug 2008.
    • Programming Languages Laboratory Seminar, KAIST, Daejeon, Korea, 12 Aug 2008.
    [abstract: txt] [slides: pdf]
  • Term equational systems and logics.
    MFPS 2008, University of Pennsylvania, Philadelphia, USA, 24 May 2008.
    [abstract: txt] [slides: pdf]
  • Term equational rewrite systems and logics.
    Semantics Lunch, Computer Laboratory, Cambridge, UK, 11 Feb 2008.
    [abstract: txt] [slides: pdf]
  • Applications of equational systems: nominal equational logic.
    Computational Applications of Nominal Sets (CANS) Meeting, Computer Laboratory, Cambridge, UK, 25 Oct 2007.
    [slides: pdf]
  • Equational systems and free constructions.
    ICALP 2007, University of Wroclaw, Poland, 12 Jul 2007.
    [abstract: txt] [slides: pdf]
  • Equational systems and free constructions.
    Extreme Theory Meeting, Computer Laboratory, Cambridge, UK, 28 Jun 2007.
  • Algebraic theories in the presence of binding operators, substitution, etc.
    Semantics Lunch, Computer Laboratory, Cambridge, UK, 20 Mar 2006.
    [abstract: txt] [slides: pdf]
  • Abstract models for structural data and its substitution.
    Extreme Theory Meeting, Computer Laboratory, Cambridge, UK, 19 Oct 2005.