Publication
An Introduction to Probabilistic Programming. Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. August 2019. (Draft)
Over-parameterised Shallow Neural Networks with Asymmetrical Node Scaling: Global Convergence Guarantees and Feature Learning. François Caron, Fadhel Ayed, Paul Jung, Hoil Lee, Juho Lee, and Hongseok Yang. September 2023. (Submitted)
Analysing Feature Learning of Gradient Descent Using Periodic Functions. Jaehui Hwang, Taeyoung Kim, and Hongseok Yang. 2nd Workshop on High-Dimensional Learning Dynamics (HiLD): The Emergence of Structure and Reasoning. June 2024. (To appear)
Transformers Can Perform Distributionally-robust Optimisation through In-context Learning. Taeyoung Kim and Hongseok Yang. 1st ICML Workshop on In-Context Learning (ICL @ ICML 2024), June 2024. (To appear)
Variational Partial Group Convolutions for Input-Aware Partial Equivariance of Rotations and Color-Shifts. Hyunsu Kim, Yegon Kim, Hongseok Yang, and Juho Lee. ICML 2024, June 2024. (To appear)
An Infinite-Width Analysis on the Jacobian-Regularised Training of a Neural Network. Taeyoung Kim and Hongseok Yang. ICML 2024, June 2024. (To appear)
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets. Nate Ackerman, Cameron Freer, Younesse Kaddar, Jacek Karwowski, Sean Moss, Daniel Roy, Sam Staton, and Hongseok Yang. POPL 2024, January 2024.
Alpha-stable Convergence of Heavy-tailed Infinitely-wide Neural Networks. Paul Jung, Hoil Lee, Jiho Lee, and Hongseok Yang. Advances of Applied Probability, Volume 55, Issue 4, December 2023.
Learning Symmetrization for Equivariance with Orbit Distance Minimization. Tien Dat Nguyen, Jinwoo Kim, Hongseok Yang, and Seunghoon Hong. Workshop on Symmetry and Geometry in Neural Representations (NeurReps 2023), December 2023.
Regularized Behavior Cloning for Blocking the Leakage of Past Action Information. Seokin Seo, HyeongJoo Hwang, Hongseok Yang, and Kee-Eung Kim. NeurIPS 2023, December 2023.
Deep neural networks with dependent weights: Gaussian Process mixture limit, heavy tails, sparsity and compressibility. Hoil Lee, Fadhel Ayed, Paul Jung, Juho Lee, Hongseok Yang, and François Caron. Journal of Machine Learning Research, 24(289):1-78, September 2023.
Regularizing Towards Soft Equivariance Under Mixed Symmetries. Hyunsu Kim, Hyungi Lee, Hongseok Yang, and Juho Lee. ICML 2023, July 2023.
Smoothness Analysis for Probabilistic Program with Application to Optimised Variational Inference. Wonyeol Lee, Xavier Rival, and Hongseok Yang. POPL 2023, January 2023.
LobsDICE: Offline Learning from Observation via Stationary Distribution Correction Estimation. Geon-Hyeong Kim, Jongmin Lee, Youngsoo Jang, Hongseok Yang, and Kee-Eung Kim. NeurIPS 2022, November 2022.
Learning Symmetric Rules with SATNet. Sangho Lim, Eun-Gyeol Oh, and Hongseok Yang. NeurIPS 2022, November 2022.
DemoDICE: Offline Imitation Learning with Supplementary Imperfect Demonstrations. Geon-Hyeong Kim, Seokin Seo, Jongmin Lee, Wonseok Jeon, HyeongJoo Hwang, Hongseok Yang, and Kee-Eung Kim. ICLR 2022, April 2022.
Scale Mixtures of Neural Network Gaussian Processes. Hyungi Lee, Eunggu Yun, Hongseok Yang, and Juho Lee. ICLR 2022, April 2022.
Meta-Learning an Inference Algorithm for Probabilistic Programs. Gwonsoo Che and Hongseok Yang. Workshop on Advances in Programming Languages and Neurosymbolic Systems (AIPLANS). December 2021.
Probabilistic Programs with Stochastic Conditioning. David Tolpin, Yuan Zhou, Tom Rainforth, and Hongseok Yang. ICML 2021, July 2021.
Specification and Space Complexity of Collaborative Text Editing. Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski. Theoretical Computer Science, vol 855, pp 141-160, February 2021. ©Elsevier.
Adaptive Strategy for Resetting a Non-stationary Markov Chain during Learning via Joint Stochastic Approximation. Hyunsu Kim, Juho Lee, and Hongseok Yang. AABI, 2021.
A Generalization of Hierarchical Exchangeability on Trees to Directed Acyclic Graphs. Paul Jung, Jiho Lee, Sam Staton, and Hongseok Yang. Annales Henri Lebesgue, 2021.
On Correctness of Automatic Differentiation for Non-Differentiable Functions. Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. NeurIPS 2020, December 2020. Spotlight.
Bayesian Policy Search for Stochastic Domains. David Tolpin, Yuan Zhou, and Hongseok Yang. PROBPROG 2020, October 2020.
Variational Inference for Sequential Data with Future Likelihood Estimates. Geon-Hyeong Kim, Youngsoo Jang, Hongseok Yang, and Kee-Eung Kim. ICML 2020, July 2020.
Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support. Yuan Zhou, Hongseok Yang, Yee Whye Teh, and Tom Rainforth. ICML 2020, July 2020.
Stochastically Differentiable Probabilistic Programs. David Tolpin, Yuan Zhou, and Hongseok Yang. Unpublished Archive Paper, March 2020.
Differentiable Algorithm for Marginalising Changepoints. Hyoungjin Lim, Gwonsoo Che, Wonyeol Lee, and Hongseok Yang. AAAI 2020, February 2020.
Towards Verified Stochastic Variational Inference for Probabilistic Programs. Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. POPL 2020, January 2020. [Slides]
Trust Region Sequential Variational Inference. Geon-Hyeong Kim, Youngsoo Jang, Jongmin Lee, Wonseok Jeon, Hongseok Yang, and Kee-Eung Kim. ACML 2019, November 2019.
Some Semantic Issues in Probabilistic Programming Languages. Hongseok Yang. Extended abstract of my FSCD'19 invited talk, June 2019.
Resource-aware Program Analysis via Online Abstraction Coarsening. Kihong Heo, Hakjoo Oh, and Hongseok Yang. ICSE 2019, May 2019. (Distinguished paper award.)
LF-PPL: A Low-Level First Order Probabilistic Programming Language for Non-Differentiable Models. Yuan Zhou, Bradley Gram-Hansen, Tobias Kohn, Tom Rainforth, Hongseok Yang, and Frank Wood. AISTATS 2019, April 2019.
Reparameterization Gradient for Non-differentiable Models. Wonyeol Lee, Hangyeol Yu, and Hongseok Yang. NIPS 2018, December 2018.
On Nesting Monte Carlo Estimators. Tom Rainforth, Rob Cornish, Hongseok Yang, Andrew Warrington, and Frank Wood. ICML 2018, July 2018.
The Beta-Bernoulli Process and Algebraic Effects. Sam Staton, Dario Stein, Hongseok Yang, Nathanael Ackerman, Cameron Freer, and Daniel M. Roy, ICALP 2018, July 2018. ©Springer-Verlag. The full version is available here.
Denotational Validation of Higher-Order Bayesian Inference. Adam Scibior, Ohad Kammar, Matthijs Vakar, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahrahmani. POPL 2018, January 2018. ©ACM
The Semantic Structure of Quasi-Borel Spaces. Chris Heunen, Ohad Kammar, Sean Moss, Adam Scibior, Sam Staton, Matthijs Vakar, and Hongseok Yang. Workshop on Probabilistic Programming Semantics (PPS 2018), January 2018.
Learning Analysis Strategies for Octagon and Context Sensitivity from Labeled Data Generated by Static Analyses. Kihong Heo, Hakjoo Oh, and Hongseok Yang. Formal Methods in System Design, 2018. ©Springer-Verlag. This is a journal version of our SAS'16 paper.
Adaptive Static Analysis via Learning with Bayesian Optimization. Kihong Heo, Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi. ACM Transactions on Programming Languages and Systems, 2018 . ©ACM. This is a journal version of our OOSPLA'15 paper.
Towards a Testable Notion of Generalisation for Generative Adversarial Networks. Robert Cornish, Frank Wood, and Hongseok Yang. NIPS Workshop on Deep Learning: Bridging Theory and Practice, December 2017.
Inference Trees: Adaptive Inference with Exploration. Tom Rainforth, Yuan Zhou, Xiaoyu Lu, Yee Whye Teh, Frank Wood, Hongseok Yang, and Jan-Willem van de Meent. NIPS Workshop on Advances in Approximate Bayesian Inference (AABI 2017), December 2017.
Automatically Generating Features for Learning Program Analysis Heuristics for C-like Languages. Kwonsoo Chae, Hakjoo Oh, Kihong Heo, and Hongseok Yang. OOPSLA 2017, October 2017. ©ACM
Algebraic Laws for Weak Consistency. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. CONCUR 2017, September 2017.
A Convenient Category for Higher-Order Probability Theory. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. LICS 2017, June 2017. ©IEEE
Design and Implementation of Probabilistic Programming Language Anglican. David Tolpin, Jan-Willem van de Meent, Hongseok Yang, and Frank Wood. Post-conference Proceedings of IFL 2016, February 2017. ©ACM. The full version is available here.
Exchangeable Random Processes and Data Abstraction. Sam Staton, Hongseok Yang, Nathanael Ackerman, Cameron Freer, and Daniel M. Roy. Workshop on Probabilistic Programming Semantics (PPS 2017), Janary 2017.
Efficient Exact Inference in Discrete Anglican Programs. Robert Cornish, Frank Wood, and Hongseok Yang. Workshop on Probabilistic Programming Semantics (PPS 2017), Janary 2017.
On the Pitfalls of Nested Monte Carlo. Tom Rainforth, Robert Cornish, Hongseok Yang, and Frank Wood. NIPS workshop on Advances in Approximate Bayesian Inference (AABI 2016), December 2016.
Learning a Variable-Clustering Strategy for Octagon from Labeled Data Generated by a Static Analysis. Kihong Heo, Hakjoo Oh, and Hongseok Yang. SAS 2016, September 2016. ©Springer-Verlag
Specification and Complexity of Collaborative Text Editing. Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski. PODC 2016, July 2016. ©ACM. The full version is available here.
Semantics for Probabilistic Programming: Higher-order Functions, Continuous Distributions, and Soft Constraints. Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, and Frank Wood. LICS 2016, July 2016. ©IEEE
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. POPL 2016, January 2016. ©ACM. The full version is available here.
Abstraction Refinement Guided by a Learnt Probabilistic Model. Radu Grigore and Hongseok Yang. POPL 2016, January 2016. ©ACM. The full version is available here.
Selective X-Sensitive Analysis Guided by Impact Pre-Analysis. Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. ACM Transactions on Programming Languages and Systems, December 2015. ©ACM. This is a full version of our PLDI'14 paper.
Learning a Strategy for Adapting a Program Analysis via Bayesian Optimisation. Hakjoo Oh, Hongseok Yang, and Kwangkeun Yi. OOPSLA 2015, October 2015. ©ACM
Transaction Chopping for Parallel Snapshot Isolation. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. DISC 2015, October 2015. ©Springer-Verlag. The full version is available here.
Modularity in Lattices: A Case Study on the Correspondence between Top-Down and Bottom-Up Analysis. Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, and Hongseok Yang. SAS 2015, September 2015. ©Springer-Verlag
Particle Gibbs with Ancestor Sampling for Probabilistic Programs. Jan-Willem van de Meent, Hongseok Yang, Vikash Mansinghka, and Frank Wood. AISTATS 2015, May 2015.
Composite Replicated Data Types. Alexey Gotsman and Hongseok Yang. ESOP 2015, April 2015. ©Springer-Verlag. The full version is available here.
Symbolic Automata for Representing Big Code. Hila Peleg, Sharon Shoham, Eran Yahav, and Hongseok Yang . Acta Informatica, 2015. This is a full version of our SAS'13 paper.
Parameterised Linearizability. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. ICALP 2014, July 2014. ©Springer-Verlag. The full version is available here.
On Abstraction Refinement for Program Analyses in Datalog. Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. PLDI 2014, June 2014. ©ACM. The full version is available here. (Distinguished paper award.)
Hybrid Top-Down and Bottom-Up Interprocedural Analysis. Xin Zhang, Ravi Mangal, Mayur Naik, and Hongseok Yang. PLDI 2014, June 2014. ©ACM. The full version is available here.
Selective Context-Sensitivity Guided by Impact Pre-Analysis. Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. PLDI 2014, June 2014. ©ACM. The full version is available here.
A Correspondence between Two Approaches to Interprocedural Analyses in the Presence of Join. Ravi Mangal, Mayur Naik, and Hongseok Yang. ESOP 2014, April 2014. ©Springer-Verlag. The full version is available here. (Best paper award nominee.)
Replicated Data Types: Specification, Verification, Optimality. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, and Marek Zawirski. POPL 2014, January 2014. ©ACM. The full version is available here. The preliminary version with some additional material can be found here.
Modular Verification of Preemptive OS Kernels. Alexey Gotsman and Hongseok Yang. Journal of Functional Programming, Volume 23, Number 4, 2013. This is a full version of our ICFP'11 paper.
Linearizability with Ownership Transfer. Alexey Gotsman and Hongseok Yang. Logical Methods in Computer Science, 9(3:12), 2013. This is a full version of our CONCUR'12 paper.
Symbolic Automata for Static Specification Mining. Hila Peleg, Sharon Shoham, Eran Yahav, and Hongseok Yang. SAS 2013, June 2013. ©Springer-Verlag. The full version is available here.
Finding Optimum Abstractions in Parametric Dataflow Analysis. Xin Zhang, Mayur Naik, and Hongseok Yang. PLDI 2013, June 2013. ©ACM. The full version is available here.
Verifying Concurrent Memory Reclamation Algorithms with Grace. Alexey Gotsman, Noam Rinetzky, and Hongseok Yang. ESOP 2013, March 2013. ©Springer-Verlag. The full version is available here. (EASST & EATCS best paper runner-up.)
A Step-Indexed Kripke Model of Hidden State. Jan Schwinghammer, Lars Birkedal, Francois Pottier, Bernhard Reus, Kristian Stovring, and Hongseok Yang. Mathematical Structures in Computer Science, Volume 23, Number 1, February 2013.
Views: Compositional Reasoning for Concurrent Programs. Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. POPL 2013, January 2013. ©ACM (Most influential paper award in POPL 2023.)
Two for the Price of One: Lifting Separation Logic Assertions. Jacob Thamsborg, Lars Birkedal, and Hongseok Yang. Logical Methods in Computer Science, 8(3:22), 2012.
Automated Concolic Testing of Smartphone Apps. Saswat Anand, Mayur Naik, Mary Jean Harrold, and Hongseok Yang. FSE 2012, November 2012. ©ACM. The full version is available here. (ESEC/FSE 2022 test of time award.)
Show No Weakness: Sequentially Consistent Specifications of TSO Libraries. Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. DISC 2012, October 2012. ©Springer-Verlag. The full version is available here.
Linearizability with Ownership Transfer. Alexey Gotsman, and Hongseok Yang. CONCUR 2012, September 2012. ©Springer-Verlag. The full version is available here. (Best paper award.)
Concurrent Library Correctness on the TSO Memory Model. Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. ESOP 2012, March 2012. ©Springer-Verlag. The full version with proofs is available here.
Abstractions From Tests. Mayur Naik, Hongseok Yang, Ghila Castelnuovo, and Mooly Sagiv. POPL 2012, January 2012. ©ACM. The full version is available here.
A Divide-and-Concur Approach for Analysing Overlaid Data Structures. Oukseh Lee, Hongseok Yang, and Rasmus Petersen. Formal Methods in System Design, Volume 41, Number 1, 2012. ©Springer-Verlag. This is a journal version of our CAV’11 paper, and contains in-depth discussions on the pre-analysis.
Compositional Shape Analysis by means of Bi-abduction. Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang. Journal of the ACM, Volume 58, Number 6, December 2011. This is a journal version of our POPL’09 paper.
Modular Verification of Preemptive OS Kernels. Alexey Gotsman, and Hongseok Yang. ICFP 2011, September 2011. ©ACM. The full version with proofs is available here.
Nested Hoare Triples and Frame Rule for Higher-order Store. Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang. Logical Methods in Computer Science, 7(3:21), 2011. This is a journal version of our CSL’09 paper. It contains more examples, proofs, and counterexamples.
Liveness-preserving Atomicity Abstraction. Alexey Gotsman, and Hongseok Yang. ICALP 2011, July 2011. ©Springer-Verlag. The full version with proofs is available here.
Program Analysis for Overlaid Data Structures. Oukseh Lee, Hongseok Yang, and Rasmus Petersen. CAV 2011, July 2011. ©Springer-Verlag
Step-Indexed Kripke Models over Recursive Worlds. Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Stovring, Jacob Thamsborg, and Hongseok Yang. POPL 2011, January 2011. ©ACM
Metric Spaces and Termination Analysis. Aziem Chawdhary, and Hongseok Yang. APLAS 2010, November 2010. ©Springer-Verlag. The full version with proofs is available here.
Abstraction for Concurrent Objects. Ivana Filipovic, Peter O’Hearn, Noam Rinetzky and Hongseok Yang. Theoretical Computer Science, vol 411/51-52, pp 51-52, December 2010. ©Elsevier. This is a journal version of our ESOP’09 paper, and it contains proofs, examples and more in-depth discussions on our results.
A Semantic Foundation for Hidden State, Jan Schwinghammer, Hongseok Yang, Lars Birkedal, Francois Pottier, and Bernhard Reus. FOSSACS 2010, April 2010. ©Springer-Verlag. The full version with proofs is available here.
Blamining the Client: On Data Refinement in the Presence of Pointers. Ivana Filipovic, Peter O’Hearn, Noah Torp-Smith and Hongseok Yang. Formal Aspects of Computing 22(5), 2010. ©Springer-Verlag.
Nested Hoare Triples and Frame Rule for Higher-order Store. Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang. CSL 2009, August 2009. ©Springer-Verlag. The full version with proofs is available here.
Abstraction for Concurrent Objects. Ivana Filipovic, Peter O’Hearn, Noam Rinetzky and Hongseok Yang. ESOP 2009, April 2009. ©Springer-Verlag. The full version with proofs is available here.
Separation and Information Hiding. Peter O’Hearn, Hongseok Yang and John Reynolds. ACM Transactions on Programming Languages and Systems 31(3), 2009. ©ACM
Compositional Shape Analysis by means of Bi-abduction. Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang. POPL 2009, January 2009. ©ACM (Most influential paper award in POPL 2019).
Scalable Shape Analysis for Systems Code. Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano and Peter O’Hearn. CAV 2008, July 2008. ©Springer-Verlag
A Simple Model of Separation Logic for Higher-order Store. Lars Birkedal, Bernhard Reus, Jan Schwinghammer and Hongseok Yang. ICALP 2008, July 2008. ©Springer-Verlag
Ranking Abstractions. Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv and Hongseok Yang. ESOP 2008, April 2008. ©Springer-Verlag. The full version with proofs is available here.
Relational Parametricity and Separation Logic. Lars Birkedal and Hongseok Yang. Logical Methods in Computer Science, 4(2:6), 2008. Journal version of my FOSSACS’07 paper. It contains proofs, examples and a description on general framework.
On Scalable Shape Analysis. Hongseok Yang, Oukseh Lee, Cristiano Calcagno, Dino Distefano and Peter O’Hearn. Queen Mary Tech Report RR-07-10, November 2007.
Goal-directed Weakening of Abstract Interpretation Results. Sunae Seo, Hongseok Yang, Kwangkeun Yi and Taisook Han. ACM Transactions on Programming Languages and Systems, 29(6), 2007. ©ACM
Footprint Analysis: A Shape Analysis that Discovers Preconditions. Cristiano Calcagno, Dino Distefano, Peter O’Hearn and Hongseok Yang. SAS 2007, August 2007. ©Springer-Verlag. Queen Mary Tech Report RR-07-02.
Shape Analysis for Composite Data Structures. Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn, Thomas Wies and Hongseok Yang. CAV 2007, July 2007. ©Springer-Verlag. Microsoft Research Tech Report TR-2007-13.
Local Action and Abstract Separation Logic. Cristiano Calcagno, Peter O’Hearn and Hongseok Yang. LICS 2007, July 2007. ©IEEE. The full version with proofs is available here.
Relational Separation Logic. Hongseok Yang. Theoretical Computer Science, vol 375/1-3, pp 308-334, May 2007. ©Elsevier
Relational Parametricity and Separation Logic. Lars Birkedal and Hongseok Yang. FOSSACS 2007, April 2007. ©Springer-Verlag
Semantics of Separation-logic Typing and Higher-order Frame Rules for Algol-like Languages. Lars Birkedal, Noah Torp-Smith and Hongseok Yang. Logical Methods in Computer Science, 2(5:1), 2006. Journal version of my LICS’05 paper. It contains proofs, examples and new results on the conjunction rule.
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. Cristiano Calcagno, Dino Distefano, Peter O'Hearn and Hongseok Yang,. SAS 2006, August 2006. ©Springer-Verlag. The full version with proofs is available here.
A Local Shape Analysis based on Separation Logic. Dino Distefano, Peter O'Hearn and Hongseok Yang. TACAS 2006, April 2006. ©Springer-Verlag. The full version with proofs is available here.
Data Refinement with Low-level Pointer Operations. Ivana Mijajlovic and Hongseok Yang. APLAS 2005, November 2005. ©Springer-Verlag. The full version with proofs is available here.
Static Insertion of Safe and Effective Memory Reuse Commands into ML-like Programs. Oukseh Lee, Hongseok Yang and Kwangkeun Yi. Science of Computer Programming, vol 58/1-2, pp 141-178, October 2005. ©Elsevier
Semantics of Separation-logic Typing and Higher-order Frame Rules. Lars Birkedal, Noah Torp-Smith and Hongseok Yang. LICS 2005, June 2005. ©IEEE
Automatic Verification of Pointer Programs Using Grammar-Based Shape Analysis. Oukseh Lee, Hongseok Yang and Kwangkeun Yi. ESOP 2005, April 2005. ©Springer-Verlag. A technical report has more explanations, and it is available here.
Abstract-value Slicing. Sunae Seo, Hongseok Yang and Kwangkeun Yi. Electronic Manuscript. September 2004. A longer version with proofs is available here.
Possible Worlds and Resources: The Semantics of BI. David J. Pym, Peter W. O'Hearn and Hongseok Yang. Theoretical Computer Science, vol 315/1, pp 257-305, May 2004. ©Elsevier
Correctness of Data Representations involving Heap Data Structures. Uday S. Reddy and Hongseok Yang. Science of Computer Programming, vol. 50/1-3, pp 129-160, March 2004. ©Elsevier. This is a journal version of our ESOP paper. It contains a better semantic model than the one in the conference paper.
Separation and Information Hiding. Peter W. O'Hearn, Hongseok Yang and John C. Reynolds. POPL 2004, January 2004. ©ACM
Automatic Construction of Hoare Proofs from Abstract Interpretation Results. Sunae Seo, Hongseok Yang and Kwangkeun Yi,. APLAS 2003, November 2003. ©Springer-Verlag
Inserting Safe Memory Re-use Commands into ML-like Programs. Oukseh Lee, Hongseok Yang and Kwangkeun Yi. SAS 2003, June 2003. ©Springer-Verlag
Correctness of Data Representations involving Heap Data Structures. Uday S. Reddy and Hongseok Yang. ESOP 2003, April 2003. ©Springer-Verlag
A Semantic Basis for Local Reasoning. Hongseok Yang and Peter W. O'Hearn. FOSSACS 2002, April 2002. ©Springer-Verlag
Local Reasoning about Programs that Alter Data Structures. Peter W. O'Hearn, John Reynolds and Hongseok Yang. CSL 2001, September 2001. ©Springer-Verlag
Local Reasoning for Stateful Programs. Hongseok Yang. Ph.D. thesis, July, 2001
Computability and Complexity Results for a Spatial Assertion Language for Data Structures. Cristiano Calcagno, Hongseok Yang and Peter W. O'Hearn. FSTTCS 2001, December 2001. ©Springer-Verlag
An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm. Hongseok Yang. Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE 2001), January 2001.
Parametric Sheaves for modelling Store Locality. Hongseok Yang and Uday S. Reddy. Electronic Manuscript, December 2000.
On the Semantics of Refinement Calculi. Hongseok Yang and Uday S. Reddy. FOSSACS 2000, April 2000. ©Springer-Verlag
Petri Net Semantics of Bunched Implication. Peter W. O'Hearn and Hongseok Yang. Electric Manuscript, October 1999.
Type Reconstruction for Syntactic Control of Interference, Part 2. Hongseok Yang and Howard Huang. ICCL 1998, May 1998.
Imperative Lambda Calculus Revisited. Hongseok Yang and Uday S. Reddy. Electronic Manuscript, August 1997.