Analysis of the λ-calculus using stable relations

This web-page embeds a prototype relational, modular static analyser for the typed λ-calculus as described in the paper Stable Relations and Abstract Interpretation of Higher-Order Programs. We extended the analyser to support pairs, records, sums, and recursive functions. Recursive datatypes are not supported at the moment. We also implemented Hindley-Milner type inference thanks to the excellent Inferno library.

The analyser infers relations between the inputs and the outputs of programs. Programs are analysed in a compositional manner. In particular, functions are analysed only once, at their definition site. As we note in the paper, the abstract domain we currently use loses a lot of information when an unknown function (i.e., a parameter of a function) is applied. Precision is satisfying in the other cases.

Warning: the analyser can take a very long time to run in your browser! Do not be surprised if your browser warns you that some script is taking a lot of time.

You can also download the associated Coq development, or browse the associated documentation directly.

The following options are available:

Author: Benoît Montagu
Copyright © Inria 2020-2021
Powered by OCaml, Js_of_ocaml and the ACE code editor.