The decidability of the βη-equivalence using hereditary substitutions

Hereditary substitutions are substitutions over the simply typed λ-calculus that preserve canonical forms and are structurally recursive. This page is devoted to a formal implementation of a normalizer for the simply typed λ-calculus using hereditary substitutions in Agda, which comes with a proof that this normalizer can be use to decide the decidability of the βη-equivalence.

Sources

The source code is available under the GPL. It is an archive containing:
Download:

Software requirements

For Agda:

Top of the page


Suggestions and bug report

Do not hesitate to make any suggestion or to report bugs to Chantal Keller (remove the anti-spam dots and at).

Top of the page


Home Research Studies Teaching Miscellaneous

Last update: 04/16/10