Fine-Grained Aliasing Control with Capture Calculus

Thumbnail

Event details

Date 06.07.2023
Hour 11:0013:00
Speaker Yichen Xu
Location
Category Conferences - Seminars
EDIC candidacy exam
Exam president: Prof. Viktor Kuncak
Thesis advisor: Prof. Martin Odersky
Co-examiner: Prof. Clément Pit-Claudel

Abstract
Various problems in programming, such as dangling pointers and data races, stem from aliasing. Aliasing control addresses these problems by tracking and regulating aliases. However, aliasing control is a double-edged sword as it can simultaneously invalidate common programming patterns and affect language usability. We propose to study fine-grained aliasing control mechanisms based on capture calculus, aiming to stike a balance between safety and usability. We put forward two potential extensions to capture calculus: syntactic control of interference and uniqueness. Formal results, including type soundness, will be developed for the proposed calculi. Additionally, we intend to implement the formal methods resulted from this research as an extension to the Scala 3 compiler to validate its usability and effectiveness in real-world programming scenarios.

Background papers
1. Karl Crary, David Walker, J. Gregory Morrisett: Typed Memory Management in a Calculus of Capabilities. POPL 1999: 262-275
2. Aaron Weiss, Olek Gierczak, Daniel Patterson, Amal Ahmed: Oxide: the Essence of Rust. arXiv:1903.00982 [cs.PL]
3. Martin Odersky, Aleksander Boruch-Gruszecki, Edward Lee, Jonathan Brachthäuser, Ondřej Lhoták: Scoped Capabilities for Polymorphic Effects. arXiv:2207.03402 [cs.PL]

Practical information

  • General public
  • Free

Contact

  • edic@epfl.ch

Tags

EDIC candidacy exam

Share