xOur data center is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Tue 24 Aug 2021 16:15 - 16:30 at ICFP Talks - Session 3
Wed 25 Aug 2021 04:15 - 04:30 at ICFP Talks - Session 3

Adversarial computations are a widely studied class of computations
where resource-bounded probabilistic adversaries have access to
oracles, i.e., probabilistic procedures with private state. These
computations arise routinely in several domains, including security,
privacy and machine learning.

In this paper, we develop program logics for reasoning about
adversarial computations in a higher-order setting. Our logics are
built on top of a simply typed $\lambda$-calculus extended with a
graded monad for probabilities and state. The grading is used to
model and restrict the memory footprint and the cost (in terms of
oracle calls) of computations. Under this view, an adversary is a
higher-order expression that expects as arguments the code of its
oracles. We develop unary program logics for reasoning about error
probabilities and expected values, and a relational logic for
reasoning about coupling-based properties. All logics feature rules
for adversarial computations, and yield guarantees that are valid
for all adversaries that satisfy a fixed resource policy. We prove
the soundness of the logics in the category of quasi-Borel spaces,
using a general notion of graded predicate liftings, and we use
logical relations over graded predicate liftings to establish the
soundness of proof rules for adversaries. We illustrate the working
of our logics with simple but illustrative examples.

Tue 24 Aug

Displayed time zone: Seoul change

16:00 - 17:30
16:00
15m
Talk
Modular, Compositional, and Executable Formal Semantics for LLVM IR
Research Papers
Yannick Zakowski Inria, Calvin Beck University of Pennsylvania, Irene Yoon University of Pennsylvania, Ilya Zaichuk Taras Shevchenko National University of Kyiv, Vadim Zaliva University of Cambridge, UK, Steve Zdancewic University of Pennsylvania
DOI Media Attached
16:15
15m
Talk
Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics
Research Papers
Alejandro Aguirre Aarhus University, Gilles Barthe MPI-SP; IMDEA Software Institute, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Shin-ya Katsumata National Institute of Informatics, Tetsuya Sato Tokyo Institute of Technology
DOI Media Attached
16:30
15m
Talk
How to Evaluate Blame for Gradual Types
Research Papers
Lukas Lazarek Northwestern University, Ben Greenman Brown University, Matthias Felleisen Northeastern University, Christos Dimoulas PLT @ Northwestern University
DOI Media Attached
16:45
15m
Talk
ProbNV: Probabilistic Verification of Network Control Planes
Research Papers
Nick Giannarakis University of Wisconsin-Madison, Alexandra Silva University College London, David Walker Princeton University
DOI Media Attached
17:00
15m
Talk
Of JavaScript AOT Compilation Performance
Research Papers
Manuel Serrano Inria, France
DOI Media Attached
17:15
15m
Talk
Symbolic and Automatic Differentiation of Languages
Research Papers
DOI Media Attached

Wed 25 Aug

Displayed time zone: Seoul change

04:00 - 05:30
Session 3Research Papers at ICFP Talks
04:00
15m
Talk
Modular, Compositional, and Executable Formal Semantics for LLVM IR
Research Papers
Yannick Zakowski Inria, Calvin Beck University of Pennsylvania, Irene Yoon University of Pennsylvania, Ilya Zaichuk Taras Shevchenko National University of Kyiv, Vadim Zaliva University of Cambridge, UK, Steve Zdancewic University of Pennsylvania
DOI Media Attached
04:15
15m
Talk
Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics
Research Papers
Alejandro Aguirre Aarhus University, Gilles Barthe MPI-SP; IMDEA Software Institute, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Shin-ya Katsumata National Institute of Informatics, Tetsuya Sato Tokyo Institute of Technology
DOI Media Attached
04:30
15m
Talk
How to Evaluate Blame for Gradual Types
Research Papers
Lukas Lazarek Northwestern University, Ben Greenman Brown University, Matthias Felleisen Northeastern University, Christos Dimoulas PLT @ Northwestern University
DOI Media Attached
04:45
15m
Talk
ProbNV: Probabilistic Verification of Network Control Planes
Research Papers
Nick Giannarakis University of Wisconsin-Madison, Alexandra Silva University College London, David Walker Princeton University
DOI Media Attached
05:00
15m
Talk
Of JavaScript AOT Compilation Performance
Research Papers
Manuel Serrano Inria, France
DOI Media Attached
05:15
15m
Talk
Symbolic and Automatic Differentiation of Languages
Research Papers
DOI Media Attached