Formal Reasoning about Mutable Data Structures with Holes in Separation Logic
Event details
| Date | 06.09.2023 |
| Hour | 09:00 › 11:00 |
| Speaker | Yawen Guan |
| Location | |
| Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. Martin Odersky
Thesis advisor: Prof. Clément Pit-Claudel
Co-examiner: Prof. Viktor Kuncak
Abstract
When reasoning about shared mutable data
structures that owns its elements (often referred to as
containers) in separation logic, borrows can be viewed as
creating holes in the logical model of original data structures.
Reasoning about accesses into containers is a complex task
with a particular challenge arising in handling multiple
borrows. Initially, we present the founding paper of separation
logic [Reynolds(2002)] to establish the theoretical
foundation. We then explore an innovative apporach proposed
in [Charguéraud(2016)] for supporting multiple borrows.
Systematically generalizing this technique necessitates
the development of a calculus for datatypes with holes.
[McBride(2001)] offers a novel perspective of such datatypes,
providing valuable insights to its development. Building upon
the strengths and limitations of these prior contributions,
Background papers
Exam president: Prof. Martin Odersky
Thesis advisor: Prof. Clément Pit-Claudel
Co-examiner: Prof. Viktor Kuncak
Abstract
When reasoning about shared mutable data
structures that owns its elements (often referred to as
containers) in separation logic, borrows can be viewed as
creating holes in the logical model of original data structures.
Reasoning about accesses into containers is a complex task
with a particular challenge arising in handling multiple
borrows. Initially, we present the founding paper of separation
logic [Reynolds(2002)] to establish the theoretical
foundation. We then explore an innovative apporach proposed
in [Charguéraud(2016)] for supporting multiple borrows.
Systematically generalizing this technique necessitates
the development of a calculus for datatypes with holes.
[McBride(2001)] offers a novel perspective of such datatypes,
providing valuable insights to its development. Building upon
the strengths and limitations of these prior contributions,
Background papers
- Reynolds, J.C. “Separation Logic: A Logic for Shared Mutable Data Structures.” In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 55–74, 2002. doi.org/10.1109/LICS.2002.1029817.
- Charguéraud, Arthur. “Higher-Order Representation Predicates in Separation Logic.” In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 3–14. St. Petersburg FL USA: ACM, 2016. doi.org/10.1145/2854065.2854068.
- Mcbride, Conor. “The Derivative of a Regular Type Is Its Type of One-Hole Contexts (Extended Abstract),” April 16, 2009. strictlypositive.org/diff.pdf
Practical information
- General public
- Free