Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
Fri 25 Jun 2021 13:45 - 13:50 at PLDI-B - Talks 6B: Applied Logics and Semantics
Sat 26 Jun 2021 01:45 - 01:50 at PLDI-B - Talks 6B: Applied Logics and Semantics

We study termination of higher-order probabilistic functional programs with recursion, stochastic conditioning and sampling from continuous distributions.

Reasoning about the termination probability of programs with continuous distributions is hard, because the enumeration of terminating executions cannot provide any non-trivial bounds.
We present a new operational semantics based on traces of intervals, which is sound and complete with respect to the standard sampling-based semantics, in which (countable) enumeration can provide arbitrarily tight lower bounds.
Consequently we obtain the first proof that deciding almost-sure termination (AST) for programs with continuous distributions is $\Pi^0_2$-complete.
We also provide a compositional representation of our semantics in terms of an intersection type system.

In the second part, we present a method of proving AST for non-affine programs, i.e., recursive programs that can, during the evaluation of the recursive body, make multiple recursive calls (of a first-order function) from distinct call sites.
Unlike in a deterministic language, the number of recursion call sites has direct consequences on the termination probability.
Our framework supports a proof system that can verify AST for programs that are well beyond the scope of existing methods.

We have constructed prototype implementations of our method of computing lower bounds of termination probability, and AST verification.

Fri 25 Jun

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

13:30 - 14:00
Talks 6B: Applied Logics and SemanticsPLDI at PLDI-B +12h
13:30
5m
Talk
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
PLDI
Simon Spies MPI-SWS, Lennard Gäher Saarland University, Daniel Gratzer Aarhus University, Joseph Tassarotti Boston College, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Lars Birkedal Aarhus University
DOI
13:35
5m
Talk
Example-Guided Synthesis of Relational Queries
PLDI
Aalok Thakkar University of Pennsylvania, Aaditya Naik University of Pennsylvania, Nathaniel Sands University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California
DOI
13:40
5m
Talk
CompCertO: Compiling Certified Open C Components
PLDI
Jérémie Koenig Yale University, Zhong Shao Yale University
DOI
13:45
5m
Talk
On Probabilistic Termination of Functional Programs with Continuous Distributions
PLDI
Raven Beutner University of Oxford, C.-H. Luke Ong University of Oxford
DOI
13:50
5m
Talk
Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption
PLDI
Meghan Cowan Facebook Reality Labs Research, Deeksha Dangwal Facebook Reality Labs Research, Armin Alaghi Facebook Reality Labs Research, Caroline Trippel Stanford University, Vincent T. Lee Facebook Reality Labs Research, Brandon Reagen New York University
DOI
13:55
5m
Talk
Polynomial Reachability Witnesses via Stellensätze
PLDI
Ali Asadi Sharif University of Technology, Krishnendu Chatterjee IST Austria, Hongfei Fu Shanghai Jiao Tong University, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Mohammad Mahdavi Sharif University of Technology
DOI

Sat 26 Jun

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

01:30 - 02:00
Talks 6B: Applied Logics and SemanticsPLDI at PLDI-B
01:30
5m
Talk
Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
PLDI
Simon Spies MPI-SWS, Lennard Gäher Saarland University, Daniel Gratzer Aarhus University, Joseph Tassarotti Boston College, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Lars Birkedal Aarhus University
DOI
01:35
5m
Talk
Example-Guided Synthesis of Relational Queries
PLDI
Aalok Thakkar University of Pennsylvania, Aaditya Naik University of Pennsylvania, Nathaniel Sands University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California
DOI
01:40
5m
Talk
CompCertO: Compiling Certified Open C Components
PLDI
Jérémie Koenig Yale University, Zhong Shao Yale University
DOI
01:45
5m
Talk
On Probabilistic Termination of Functional Programs with Continuous Distributions
PLDI
Raven Beutner University of Oxford, C.-H. Luke Ong University of Oxford
DOI
01:50
5m
Talk
Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption
PLDI
Meghan Cowan Facebook Reality Labs Research, Deeksha Dangwal Facebook Reality Labs Research, Armin Alaghi Facebook Reality Labs Research, Caroline Trippel Stanford University, Vincent T. Lee Facebook Reality Labs Research, Brandon Reagen New York University
DOI
01:55
5m
Talk
Polynomial Reachability Witnesses via Stellensätze
PLDI
Ali Asadi Sharif University of Technology, Krishnendu Chatterjee IST Austria, Hongfei Fu Shanghai Jiao Tong University, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Mohammad Mahdavi Sharif University of Technology
DOI