1 \documentclass{llncs} |
|
2 \usepackage[utf8]{inputenc} |
|
3 \usepackage{lineno} |
|
4 \usepackage{url} |
|
5 \usepackage{amsmath,amssymb} |
|
6 \usepackage{isabelle,isabellesym} |
|
7 \usepackage{pdfsetup} |
|
8 \usepackage{ot1patch} |
|
9 %\usepackage{boxedminipage} |
|
10 |
|
11 \allowdisplaybreaks |
|
12 \urlstyle{rm} |
|
13 \isabellestyle{it} |
|
14 \renewcommand{\isastyleminor}{\it}% |
|
15 \renewcommand{\isastyle}{\normalsize\it}% |
|
16 |
|
17 \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}} |
|
18 \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}} |
|
19 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
|
20 \renewcommand{\isasymbullet}{{\raisebox{0.2mm}{\small$\bullet$}}} |
|
21 \renewcommand{\isasymintegral}{$\lambda$} |
|
22 \renewcommand{\isasymlbrace}{$\ulcorner$} |
|
23 \renewcommand{\isasymrbrace}{$\urcorner$} |
|
24 %\renewcommand{\isasymguillemotleft}{} |
|
25 %\renewcommand{\isasymguillemotright}{} |
|
26 |
|
27 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
|
28 \renewcommand{\isasymequiv}{=} |
|
29 %%\renewcommand{\isasymiota}{} |
|
30 \renewcommand{\isasymxi}{$..$} |
|
31 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
32 \newcommand{\isasymnotapprox}{$\not\approx$} |
|
33 \newcommand{\isasymLET}{$\mathtt{let}$} |
|
34 \newcommand{\isasymAND}{$\mathtt{and}$} |
|
35 \newcommand{\isasymIN}{$\mathtt{in}$} |
|
36 \newcommand{\isasymEND}{$\mathtt{end}$} |
|
37 \newcommand{\isasymBIND}{$\mathtt{bind}$} |
|
38 \newcommand{\isasymANIL}{$\mathtt{anil}$} |
|
39 \newcommand{\isasymACONS}{$\mathtt{acons}$} |
|
40 \newcommand{\isasymCASE}{$\mathtt{case}$} |
|
41 \newcommand{\isasymOF}{$\mathtt{of}$} |
|
42 \newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}} |
|
43 \newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}} |
|
44 \newcommand{\isasymFRESH}{\#} |
|
45 \newcommand{\LET}{\;\mathtt{let}\;} |
|
46 \newcommand{\IN}{\;\mathtt{in}\;} |
|
47 \newcommand{\END}{\;\mathtt{end}\;} |
|
48 \newcommand{\AND}{\;\mathtt{and}\;} |
|
49 \newcommand{\fv}{\mathit{fv}} |
|
50 |
|
51 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
|
52 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
|
53 |
|
54 \begin{document} |
|
55 |
|
56 \title{Execution modulo alpha-equivalence} |
|
57 \author{...\inst{1} \and ...\inst{2}} |
|
58 \institute{... \and ...} |
|
59 |
|
60 \maketitle |
|
61 |
|
62 \begin{abstract} |
|
63 In this paper we show how a formal specification defined modulo |
|
64 alpha-equivalence can be programatically made executable. |
|
65 We show a general algorithm and we present examples of |
|
66 executed calculi, which we implement in Nominal Isabelle. |
|
67 \end{abstract} |
|
68 |
|
69 \input{session} |
|
70 |
|
71 %\begin{spacing}{0.9} |
|
72 \bibliographystyle{abbrv} |
|
73 \bibliography{root} |
|
74 %\end{spacing} |
|
75 |
|
76 \end{document} |
|
77 |
|
78 %%% Local Variables: |
|
79 %%% mode: latex |
|
80 %%% TeX-master: t |
|
81 %%% End: |
|