Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

A Relational Logic for Higher-Order Programs

Series
International Conference on Functional Programming 2017
Video Embed
Alejandro Aguirre, IMDEA Software Institute, Spain, gives the second talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference.
Co-written by Gilles Berthe (IMDEA Software Institute, Spain), Marco Gaboardi (University at Buffalo, SUNY, USA), Deepak Garg (MPI-SWS, Germany), Pierre-Yves Strub (Ecole Polytechnique, France)

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 specialised 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.

More in this series

View Series
International Conference on Functional Programming 2017

Verified Low-Level Programming Embedded in F

Jonathan Protzen, Microsoft Research, United States, gives the second talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference.
Previous
International Conference on Functional Programming 2017

Verifying Efficient Function Calls in CakeML

Scott Owens University of Kent, UK, gives the third talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Alejandro Aguirre
Keywords
technology
computing
programming
Department: Department of Computer Science
Date Added: 18/12/2017
Duration: 00:17:28

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford