BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Formal Reasoning about Mutable Data Structures with Holes in Separ
 ation Logic
DTSTART:20230906T090000
DTEND:20230906T110000
DTSTAMP:20260409T010555Z
UID:84ab643753ad36211b717dd2a7a9e9979e86833141b16fe22a41c5cc
CATEGORIES:Conferences - Seminars
DESCRIPTION:Yawen Guan\nEDIC candidacy exam\nExam president: Prof. Martin 
 Odersky\nThesis advisor: Prof. Clément Pit-Claudel\nCo-examiner: Prof. Vi
 ktor Kuncak\n\nAbstract\nWhen reasoning about shared mutable data\nstructu
 res that owns its elements (often referred to as\ncontainers) in separatio
 n logic\, borrows can be viewed as\ncreating holes in the logical model of
  original data structures.\nReasoning about accesses into containers is a 
 complex task\nwith a particular challenge arising in handling multiple\nbo
 rrows. Initially\, we present the founding paper of separation\nlogic [Rey
 nolds(2002)] to establish the theoretical\nfoundation. We then explore an 
 innovative apporach proposed\nin [Charguéraud(2016)] for supporting multi
 ple borrows.\nSystematically generalizing this technique necessitates\nthe
  development of a calculus for datatypes with holes.\n[McBride(2001)] offe
 rs a novel perspective of such datatypes\,\nproviding valuable insights to
  its development. Building upon\nthe strengths and limitations of these pr
 ior contributions\,\n\nBackground papers\n\n	Reynolds\, J.C. “Separation
  Logic: A Logic for Shared Mutable Data Structures.” In Proceedings 17t
 h Annual IEEE Symposium on Logic in Computer Science\, 55–74\, 2002. do
 i.org/10.1109/LICS.2002.1029817.\n	Charguéraud\, Arthur. “Higher-Order 
 Representation Predicates in Separation Logic.” In Proceedings of the 5
 th ACM SIGPLAN Conference on Certified Programs and Proofs\, 3–14. St. P
 etersburg FL USA: ACM\, 2016. doi.org/10.1145/2854065.2854068.\n	Mcbride\
 , Conor. “The Derivative of a Regular Type Is Its Type of One-Hole Conte
 xts (Extended Abstract)\,” April 16\, 2009. strictlypositive.org/diff.
 pdf\n
LOCATION:BC 333 https://plan.epfl.ch/?room==BC%20333
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR