Relational reasoning for advanced type systems in advanced program logics

Many interesting properties of programs and programming languages arerelational, e.g., contextual refinement and equivalence,non-interference (a security property) and compilercorrectness. Logical relations are a versatile proof technique forestablishing relational properties developed primarily for reasoningabout contextual refinement and equivalence. This technique wasoriginally developed for purely functional higher-order programminglanguages and has recently been extended to support reasoning forprogramming languages with such advanced features as dynamicallyallocated higher-order mutable references and concurrency which areubiquitous in most modern programming languages.Recently we have demonstrated how one can define such astate-of-the-art logical relations in a state-of-the-art program logiccalled Iris. This development has been carried out in the Coq proofassistant and has made it possible for the first time to reasonformally about contextual refinements in a proof assistant. Forinstance, we showed refinement for modules implementing trickyfine-grained concurrent data-structures. This work was done incollaboration with Prof. Birkedal (Aarhus university, Denmark). Ourresults have been published in POPL'17, the premier conference in thefield of programming languages.In this project we will research and formally develop logicalrelations for programming languages with richer and more expressivetype systems, e.g., Scala and Rust, which use more intricate types toguarantee stronger properties about programs. We will use theselogical relations to also study properties such as non-interferenceand compiler correctness.

Keywords:Programming Languages, Secure Compilation, Logical Relations, Program Logics (Separation Logic), Formal Verification

Disciplines:Applied mathematics in specific fields, Computer architecture and networks, Distributed computing, Information sciences, Information systems, Programming languages, Scientific computing, Theoretical computer science, Visual computing, Other information and computing sciences