nominal2: Nominal/Ex/Exec/document/root.tex@66114fa3d2ee (annotated)

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

author	Christian Urban <urbanc@in.tum.de>
	Thu, 19 Apr 2018 13:58:22 +0100
branch	Nominal2-Isabelle2016-1
changeset 3246	66114fa3d2ee
parent 3173	9876d73adb2b
permissions	-rw-r--r--