Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Tue 25 Sep 2018 13:45 - 14:07 at Stifel Theatre - Proof Techniques and Mechanization Chair(s): Niki Vazou

Abstract interpretation is a technique for developing static analyses. Yet, proving abstract interpreters sound is challenging for interesting analyses, because of the high proof complexity and proof effort. To reduce complexity and effort, we propose a framework for abstract interpreters that makes their soundness proof compositional. Key to our approach is to capture the similarities between concrete and abstract interpreters in a single shared interpreter, parameterized over an arrow-based interface. In our framework, a soundness proof is reduced to proving reusable soundness lemmas over the concrete and abstract instances of this interface; the soundness of the overall interpreters follows from a generic theorem. To further reduce proof effort, we explore the relationship between soundness and parametricity. Parametricity not only provides us with useful guidelines for how to design non-leaky interfaces for shared interpreters, but also provides us soundness of shared pure functions as free theorems. We implemented our framework in Haskell and developed a k-CFA analysis for PCF and a tree-shape analysis for Stratego. We were able to prove both analyses sound compositionally with manageable complexity and effort, compared to a conventional soundness proof.

Tue 25 Sep
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

13:00 - 14:30
Proof Techniques and MechanizationResearch Papers at Stifel Theatre
Chair(s): Niki VazouUniversity of Maryland, USA
13:00
22m
Talk
MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic
Research Papers
Robbert KrebbersDelft University of Technology, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Ralf JungMPI-SWS, Joseph TassarottiCarnegie Mellon University, Jan-Oliver KaiserMPI-SWS, Amin Timanyimec-Distrinet KU-Leuven, Arthur CharguéraudInria, Derek DreyerMPI-SWS
DOI
13:22
22m
Talk
Mtac2: Typed Tactics for Backward Reasoning in Coq
Research Papers
Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET, Robbert KrebbersDelft University of Technology, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek DreyerMPI-SWS
DOI
13:45
22m
Talk
Compositional Soundness Proofs of Abstract Interpreters
Research Papers
Sven KeidelDelft University of Technology, Netherlands, Casper Bach PoulsenDelft University of Technology, Sebastian ErdwegDelft University of Technology, Netherlands
DOI
14:07
22m
Talk
Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper
Research Papers
Nicolas TabareauInria, Éric TanterUniversity of Chile & Inria Paris, Matthieu SozeauInria
DOI