无所有权或线性类型的模块化借用(IWACO 2024 - IWACO'24) - SPLASH 2024

主要观点

  • 借用是资源可临时共享和使用后归还的过程,在 Rust 语言中流行,用于保证内存安全。
  • 提出基于类型和效果系统以及布尔代数子类型的新借用方式,在类型系统中跟踪资源使用作为副作用,用布尔否定类型表示借用区域,避免某些效果发生。
  • 利用 MLstruct 的布尔代数子类型推断可表达使用借用的程序而无需用户程序中的类型注解,且借用规则基于类型而非语法,可自由模块化代码。

关键信息

  • 借用在 Rust 中通过限制可变性和别名互斥及绑定借用引用的生命周期来保证内存安全,依赖其所有权系统。
  • 新借用方式通过类型系统跟踪资源使用和用布尔否定类型表示借用区域。
  • 可利用特定推断表达使用借用的程序且可自由模块化代码。

重要细节

  • 11:00 - 12:30 在 Session 2[IWACO]于[Pacific B]举行,主席是[James Noble],在新西兰惠灵顿。
  • 11:00 有 30 分钟的演讲“Capabilities, Effects, Ownership, and Behaviors”由[Colin Gordon]演讲。
  • 11:30 有 30 分钟的演讲“Modular Borrowing Without Ownership or Linear Types”由[Lionel Parreaux](香港科技大学)演讲,有媒体和文件附件。
  • 12:00 有 30 分钟的演讲“Substructural Information Flow via Polymorphism”由[Hemant Gouni](卡内基梅隆大学)和[Jonathan Aldrich](卡内基梅隆大学)演讲,有媒体和文件附件。
阅读 22
0 条评论