Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Fri 28 Sep 2018 10:45 - 11:10 at New York Central - Session 1

Rust represents a major advancement in production programming languages because of its success in bridging the gap between high-level application programming and low-level systems programming. At the heart of its design lies a novel approach to ownership that remains highly programmable.

In this talk, we will describe our ongoing work on providing a formal semantics for Rust that captures how programmers can understand ownership and borrowing without trying to grasp the details of lifetime analysis. Our model is close to source-level Rust (but with full type annotations) which differs from the recent RustBelt effort that essentially models MIR, a CPS-style IR used in the Rust compiler. Moreover, while RustBelt’s goal is to verify the unsafe code in Rust’s standard library, ours is much less ambitious. We model Rust’s standard library APIs using primitives, which is entirely sufficient for capturing their expressive power, but yields a simpler model of Rust and its type system that we think PL researchers (you!) will find easier to use as a starting point for investigating extensions to Rust. Unlike RustBelt, we prove type soundness using progress and preservation instead of Kripke logical relation. Finally, our semantics is a family of languages of increasing expressive power—where, following Felleisen, “expressive power of languages” is defined in terms of observational equivalence. Separating the language into different levels of expressive power provides useful information for future work on Rust verification and compiler optimization.

Fri 28 Sep
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:20 - 12:00: Session 1ML at New York Central
10:20 - 10:45
Safely Mixing OCaml and Rust
Stephen DolanUniversity of Cambridge
10:45 - 11:10
Rust Distilled: An Expressive Tower of Languages
Aaron WeissNortheastern University, Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
Link to publication Pre-print
11:10 - 11:35
Generating Mutually Recursive Definitions
Jeremy YallopUniversity of Cambridge, UK, Oleg Kiselyov
11:35 - 12:00
Experience Report: Type-Safe Multi-Tier Programming with Standard ML Modules
Martin ElsmanUniversity of Copenhagen, Denmark, Philip MunksgaardIntelligent Alpha AG, Switzerland, Ken Friis LarsenDIKU, University of Copenhagen
Link to publication