>>> Google Scholar

Draft Thesis

• Draft Thesis (April 2023).
• Thesis proposal (July 2020).

2022

• Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic. Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer. In PLDI 2022.
• Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations. Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer. In POPL 2022.

2021

• GhostCell: Separating Permissions from Data in Rust. Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, Derek Dreyer. In ICFP 2021.

2020

• Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn, Jules Villard. In CAV 2020.
• RustBelt Meets Relaxed Memory. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer. In POPL 2020. (Slides | Talk)
• Stacked Borrows: An Aliasing Model for Rust. Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer. In POPL 2020.

2017

• Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis. In ECOOP 2017, with Best Paper Award.

Presentations

• Talk at Google Munich about RustBelt, October 2018, as part of my internship at V8.
• Talk at the 1st Iris Workshop on RustBelt Relaxed, October 2019.

Pre-MPI Publications

• Learning and practicing object-oriented programming using a collaborative web-based IDE. Vu Nguyen, Hai H. Dang, Kha N. Do, Thu D. Tran. In Frontiers in Education Conference (FIE) 2014.
• EduCo: An Integrated Social Environment for Teaching and Learning Software Engineering Courses. Hai H. Dang, Vu Nguyen, Kha N. Do, Thu D. Tran. In iiWAS 2014.
• An interactive Web-based IDE towards teaching and learning in programming courses. Hai T. Tran, Hai H. Dang, Kha N. Do, Thu D. Tran, Vu Nguyen. In TALE 2013.