Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Tue 5 Sep 2017 13:22 - 13:45 at L1 - Foundations of Higher-Order Programming Chair(s): Gabriel Scherer

Relational program verification is a variant of program verification
where one can reason about two programs and as a special case about
two executions of a single program on different inputs. Relational
program verification can be used for reasoning about a broad range of
properties, including equivalence and refinement, and specialized
notions such as continuity, information flow security or relative
cost. In a higher-order setting, relational program verification can
be achieved using relational refinement type systems, a form of
refinement types where assertions have a relational interpretation.
Relational refinement type systems excel at relating structurally
equivalent terms but provide limited support for relating terms with
very different structures.

We present a logic, called Relational Higher Order Logic (RHOL), for
proving relational properties of a simply typed $\lambda$-calculus
with inductive types and recursive definitions. RHOL retains the
type-directed flavour of relational refinement type systems but
achieves greater expressivity through rules which simultaneously
reason about the two terms as well as rules which only contemplate one
of the two terms. We show that RHOL has strong foundations, by proving
an equivalence with higher-order logic (HOL), and leverage this
equivalence to derive key meta-theoretical properties: subject
reduction, admissibility of a transitivity rule and set-theoretical
soundness. Moreover, we define sound embeddings for several existing
relational type systems such as relational refinement types and type
systems for dependency analysis and relative cost, and we verify
examples that were out of reach of prior work.

Tue 5 Sep

Displayed time zone: Belfast change

13:00 - 14:30
Foundations of Higher-Order ProgrammingResearch Papers at L1
Chair(s): Gabriel Scherer Northeastern University
13:00
22m
Talk
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Research Papers
Makoto Hamana Gunma University, Japan
DOI
13:22
22m
Talk
A Relational Logic for Higher-Order Programs
Research Papers
Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Spain, Marco Gaboardi University at Buffalo, SUNY, USA, Deepak Garg MPI-SWS, Germany, Pierre-Yves Strub École Polytechnique, n.n.
DOI
13:45
22m
Talk
Foundations of Strong Call by Need
Research Papers
Thibaut Balabonski LRI, France / University of Paris-Sud, France, Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia Kesner Université de Paris, CNRS, IRIF, France
DOI
14:07
22m
Talk
No-Brainer CPS Conversion
Research Papers
Milo Davis Northeastern University, USA, William Meehan Northeastern University, USA, Olin Shivers Northeastern University, USA
DOI