Stable relations and abstract interpretation of higher-order programs
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.
Slides (slides-stable-relations-ICFP-SPLASH.pdf) | 1008KiB |
Thu 8 DecDisplayed 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 30mTalk | 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 30mTalk | 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 30mTalk | Stable relations and abstract interpretation of higher-order programs COVID Time Papers In Person Link to publication File Attached |