IWACO 2023
who it's for
programming language researchers, compiler engineers, formal verification engineers, Rust developers, Scala developers, systems programmers, tool developers
topics
capture tracking in Scala; borrow checking via abstract interpreter; capture separation calculus; alias-tracking for Java; mechanized box calculus in Coq; verifier for Rust iterator chains; ownership step-debugger Oxidize; arena allocation optimizations; non-lexical lifetime inference; ghost instructions for lifetimes; separation-degree inference
| title | author | length |
|---|---|---|
| Welcome to IWACO! | Aleksander Boruch-Gruszecki | 07m |
Organizers pull IWACO together after a chance conversation at Splash and four people end up running the workshop; the program ties capability as a file handle… | ||
| Capture Tracking in Scala | Martin Odersky | 01h 23m |
Claim: compile-time capture tracking makes effect- and resource-typing work without exploding higher‑order APIs by treating effects as capabilities as implicit… | ||
| Borrow checking Hylo | Dimi Racordon, Dave Abrahams | 28m |
Hylo aims for C++-level speed with guaranteed freedom from undefined behavior by running borrow checking on Hylo IR using an abstract interpreter that models… | ||
| Degrees of Separation: A Flexible Type System for Data Race Prevention | Yichen Xu, Aleksander Boruch-Gruszecki, Martin Odersky | 26m |
Proposes Capture Separation Calculus (CSC) that lets aliasing remain common but tracks and restricts aliases only where races matter, proving type safety and… | ||
| Latte: Lightweight Aliasing Tracking for Java | Conrad Zimmerman, Catarina Gamboa, Alcides Fonseca, Jonathan Aldrich | 33m |
A formal alias-tracking type system for Java that requires annotations only on parameters and fields, infers all local aliases, and enforces unique parameters… | ||
| A Mechanized Theory of the Box Calculus | Joseph Fourment, Yichen Xu | 22m |
Mechanization of the Box Calculus appears as a complete Coq development that formalizes System CC_<:□ with Coq mechanization and produces a verified soundness… | ||
| Compositional Reasoning about Advanced Iterator Patterns in Rust | Aurel Bílý, Jonas Hansen, Alexander J. Summers, Peter Müller | 25m |
Methodology specifies and verifies Rust iterator chains that include closures with side effects, claiming precise modular reasoning about composition and… | ||
| Oxidize: A Step-Debugger for Static Semantics | Peter Chon, Dimi Racordon, Nada Amin | 23m |
A static step-debugger for Rust-like ownership semantics that actually simulates the borrow checker by stepping three explicit contexts: a type context, a… | ||
| nothing matches | ||