SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Thu 8 Dec 2022 16:30 - 17:00 at Seminar Room LG004 - ICFP Papers Chair(s): Matthieu Lemerre

We present a novel denotational semantics for the untyped call-by-value λ-calculus, where terms are interpreted as stable relations, i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. The definition also admits a presentation as a program logic. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its result—a form of frame condition for functional programs.

Thu 8 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
ICFP PapersCOVID Time Papers In Person at Seminar Room LG004
Chair(s): Matthieu Lemerre CEA LIST, France
15:30
30m
Talk
Certifying the Synthesis of Heap-Manipulating Programs
COVID Time Papers In Person
Yasunari Watanabe Ahrefs Research, Kiran Gopinathan National University of Singapore, George Pîrlea National University of Singapore, Singapore, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore
Link to publication DOI
16:00
30m
Talk
Kindly Bent to Free Us
COVID Time Papers In Person
Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany
Link to publication DOI
16:30
30m
Talk
Stable relations and abstract interpretation of higher-order programs
COVID Time Papers In Person
Benoît Montagu Inria, Thomas P. Jensen INRIA Rennes
Link to publication File Attached