Hereditary substitutions for simple types (revised)
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
BetaEta.agda
COPYING
Completeness.agda
Everything.agda
Lemmas.agda
Normalization.agda
README.md
Soundness.agda
Stlc.agda

README.md

Hereditary substitutions for simple types (revised)

Based on

  1. Chantal Keller and Thorsten Altenkirch. 2010. Hereditary substitutions for simple types, formalized.
    In Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming (MSFP '10). ACM, New York, NY, USA, 3-10.
    DOI=10.1145/1863597.1863601
    http://doi.acm.org/10.1145/1863597.1863601

  2. Chantal Keller. 2010. The decidability of the βη-equivalence using hereditary substitutions.
    http://www.lix.polytechnique.fr/~keller/Recherche/hsubst.html

I tried to refactor the code in [1] and [2], to make it more "good-looking". Whether the result is really better than the original, is disputable. "There's no accounting for taste." :-)

Note. [2] is under GNU General Public License. Thus, the part of the code that is based on [2] is under GPL. On the other hand, the text of the paper [1] is not under GPL. Hence, the code that is directly based on [1] needn't be under GPL (and it is not).