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:
Learn from patterns
: refine the knowledge in the
branches of a pattern matching construct.
Fail when a type mismatch is found
: when a type
mismatch is found while performing operations on the abstract
domain, fail immediatly. This should not happen.
Fixpoint unrolling
: tells how many iterations
must be unfolded before a standard fixpoint computation is
started (only useful for recursive functions).
Delay widening
: tells how many iterations must be
performed during fixpoint computation before widening must be
employed (only useful for recursive functions).
Author: Benoît
Montagu
Copyright © Inria 2020-2021
Powered by OCaml,
Js_of_ocaml
and the ACE code editor.