19 \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} |
20 \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} |
20 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
21 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
21 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
22 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
22 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
23 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
23 \renewcommand{\isasymequiv}{$\dn$} |
24 \renewcommand{\isasymequiv}{$\dn$} |
24 \renewcommand{\isasymiota}{} |
25 %%\renewcommand{\isasymiota}{} |
25 \renewcommand{\isasymemptyset}{$\varnothing$} |
26 \renewcommand{\isasymemptyset}{$\varnothing$} |
26 \newcommand{\isasymnotapprox}{$\not\approx$} |
27 \newcommand{\isasymnotapprox}{$\not\approx$} |
27 \newcommand{\isasymLET}{$\mathtt{let}$} |
28 \newcommand{\isasymLET}{$\mathtt{let}$} |
28 \newcommand{\isasymAND}{$\mathtt{and}$} |
29 \newcommand{\isasymAND}{$\mathtt{and}$} |
29 \newcommand{\isasymIN}{$\mathtt{in}$} |
30 \newcommand{\isasymIN}{$\mathtt{in}$} |
30 \newcommand{\isasymEND}{$\mathtt{end}$} |
31 \newcommand{\isasymEND}{$\mathtt{end}$} |
31 \newcommand{\isasymBIND}{$\mathtt{bind}$} |
32 \newcommand{\isasymBIND}{$\mathtt{bind}$} |
32 \newcommand{\isasymANIL}{$\mathtt{anil}$} |
33 \newcommand{\isasymANIL}{$\mathtt{anil}$} |
33 \newcommand{\isasymACONS}{$\mathtt{acons}$} |
34 \newcommand{\isasymACONS}{$\mathtt{acons}$} |
|
35 \newcommand{\isasymCASE}{$\mathtt{case}$} |
|
36 \newcommand{\isasymOF}{$\mathtt{of}$} |
34 \newcommand{\LET}{\;\mathtt{let}\;} |
37 \newcommand{\LET}{\;\mathtt{let}\;} |
35 \newcommand{\IN}{\;\mathtt{in}\;} |
38 \newcommand{\IN}{\;\mathtt{in}\;} |
36 \newcommand{\END}{\;\mathtt{end}\;} |
39 \newcommand{\END}{\;\mathtt{end}\;} |
37 \newcommand{\AND}{\;\mathtt{and}\;} |
40 \newcommand{\AND}{\;\mathtt{and}\;} |
38 \newcommand{\fv}{\mathit{fv}} |
41 \newcommand{\fv}{\mathit{fv}} |
67 term-constructors where multiple variables are bound at once. Such general |
70 term-constructors where multiple variables are bound at once. Such general |
68 bindings are ubiquitous in programming language research and only very |
71 bindings are ubiquitous in programming language research and only very |
69 poorly supported with single binders, such as lambda-abstractions. Our |
72 poorly supported with single binders, such as lambda-abstractions. Our |
70 extension includes novel definitions of alpha-equivalence and establishes |
73 extension includes novel definitions of alpha-equivalence and establishes |
71 automatically the reasoning infrastructure for alpha-equated terms. We |
74 automatically the reasoning infrastructure for alpha-equated terms. We |
72 also provide strong induction principles that have the usual variable |
75 also prove strong induction principles that have the usual variable |
73 convention already built in. |
76 convention already built in. |
74 \end{abstract} |
77 \end{abstract} |
75 |
78 |
76 |
79 |
77 \input{session} |
80 \input{session} |