equal
deleted
inserted
replaced
53 where multiple variables are bound at once. Such |
53 where multiple variables are bound at once. Such |
54 binding structures are ubiquitous in programming language research and only |
54 binding structures are ubiquitous in programming language research and only |
55 very poorly supported with single binders, such as the lambdas in the |
55 very poorly supported with single binders, such as the lambdas in the |
56 lambda-calculus. Our extension includes novel definitions of |
56 lambda-calculus. Our extension includes novel definitions of |
57 alpha-equivalence and establishes automatically the reasoning infrastructure for |
57 alpha-equivalence and establishes automatically the reasoning infrastructure for |
58 alpha-equated terms. This includes strong induction principles that have the |
58 alpha-equated terms. We can also provide strong induction principles that have |
59 usual variable convention already built in. |
59 the usual variable convention already built in. |
60 \end{abstract} |
60 \end{abstract} |
61 |
61 |
62 |
62 |
63 \input{session} |
63 \input{session} |
64 |
64 |