Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 19:20 - 19:30 at POPL-A - Program Analysis

In call-by-value languages, some mutually-recursive definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures.

We present a set of declarative inference rules, prove its soundness with respect to the reference source-level semantics of Nordlander, Carlsson, and Gill [2008], and show that it can be directed into an algorithmic backwards analysis check in a surprisingly simple way.

Our implementation of this new check replaced the existing check used by the OCaml programming language, a fragile syntactic/grammatical criterion which let several subtle bugs slip through as the language kept evolving. We document some issues that arise when advanced features of a real-world functional language (exceptions in first-class modules, GADTs, etc.) interact with safety checking for recursive definitions.

Conference Day
Wed 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
Program AnalysisPOPL at POPL-A
18:30
10m
Talk
Verifying Correct Usage of Context-Free API Protocols
POPL
Kostas FerlesUT Austin, Jon StephensUniversity of Texas at Austin, Isil DilligUniversity of Texas at Austin
Link to publication DOI
18:40
10m
Talk
Data Flow Refinement Type Inference
POPL
Zvonimir PavlinovicGoogle, USA, Yusen SuNew York University, University of Waterloo, Thomas WiesNew York University, USA
Link to publication DOI
18:50
10m
Talk
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
POPL
Jay P. LimRutgers University, USA, Mridul AanjaneyaRutgers University, John GustafsonNational University of Singapore, Santosh NagarakatteRutgers University, USA
Link to publication DOI
19:00
10m
Talk
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow GraphsDistinguished Paper
POPL
Julian RosemannSaarland University, Saarland Informatics Campus, Simon MollNEC Deutschland, Sebastian HackSaarland University, Germany
Link to publication DOI
19:10
10m
Talk
Relatively Complete Verification of Probabilistic Programs
POPL
Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaETH Zurich
Link to publication DOI
19:20
10m
Talk
A Practical Mode System for Recursive Definitions
POPL
Alban ReynaudENS Lyon, Gabriel SchererINRIA Saclay, Jeremy YallopUniversity of Cambridge
Link to publication DOI Pre-print