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:

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