Wed 23 Oct 2024 14:00 - 14:20 at San Gabriel - Formal Methods 1 Chair(s): Benjamin Delaware

Dynamically typed array languages such as Python, APL, and Matlab lift scalar operations to arrays and replicate scalars to fit applications. We present a mechanism for automatically inferring map and replicate operations in a statically-typed language in a way that resembles the programming experience of a dynamically-typed language while preserving the static typing guarantees. Our type system—which supports parametric polymorphism, higher-order functions, and top-level let-generalization—makes use of integer linear programming in order to find the minimum number of operations needed to elaborate to a well-typed program. We argue that the inference system provides useful and unsurprising guarantees to the programmer. We demonstrate important theoretical properties of the mechanism and report on the implementation of the mechanism in the statically-typed array programming language Futhark.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:40 - 15:20
Formal Methods 1OOPSLA 2024 at San Gabriel
Chair(s): Benjamin Delaware Purdue University
13:40
20m
Talk
Realistic Realizability: Specifying ABIs You Can Count On
OOPSLA 2024
Andrew Wagner Northeastern University, Zachary Eisbach Northeastern University, Amal Ahmed Northeastern University, USA
DOI
14:00
20m
Talk
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
OOPSLA 2024
Robert Schenck DIKU, University of Copenhagen, Nikolaj Hey Hinnerskov DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Magnus Madsen Aarhus University, Martin Elsman University of Copenhagen
DOI
14:20
20m
Talk
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
OOPSLA 2024
Noam Zilberstein Cornell University, Angelina Saliling Cornell University, Alexandra Silva Cornell University
DOI
14:40
20m
Talk
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
OOPSLA 2024
Yichuan Li Nanjing University of Science and Technology, Wei Song Nanjing University of Science and Technology, Jeff Huang Texas A&M University
DOI
15:00
20m
Talk
Weighted Context-Free-Language Ordered Binary Decision Diagrams
OOPSLA 2024
Meghana Aparna Sistla The University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Thomas Reps University of Wisconsin-Madison
DOI