Paper/document/root.tex
changeset 1687 51bc795b81fd
parent 1657 d7dc35222afc
child 1703 ac2d0d4ea497
equal deleted inserted replaced
1686:7b3dd407f6b3 1687:51bc795b81fd
     7 \usepackage{tikz}
     7 \usepackage{tikz}
     8 \usepackage{pgf}
     8 \usepackage{pgf}
     9 \usepackage{pdfsetup}
     9 \usepackage{pdfsetup}
    10 \usepackage{ot1patch}
    10 \usepackage{ot1patch}
    11 \usepackage{times}
    11 \usepackage{times}
       
    12 \usepackage{boxedminipage}
    12 
    13 
    13 \urlstyle{rm}
    14 \urlstyle{rm}
    14 \isabellestyle{it}
    15 \isabellestyle{it}
    15 \renewcommand{\isastyleminor}{\it}%
    16 \renewcommand{\isastyleminor}{\it}%
    16 \renewcommand{\isastyle}{\normalsize\it}%
    17 \renewcommand{\isastyle}{\normalsize\it}%
    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}