\documentclass[a4paper]{article}

\usepackage{a4wide}
\usepackage{pifont}
\usepackage{semantic}
\usepackage{stmaryrd}
\usepackage{graphicx}

\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}

\title{Continuationals semantics for \MATITA}
\author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\
\small Department of Computer Science, University of Bologna \\
\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
\small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}

\newcommand{\MATHIT}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\MATHTT}[1]{\ensuremath{\mathtt{#1}}}

\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
\newcommand{\SKIP}{\MATHTT{skip}}
\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}

\newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}

\newcommand{\GOAL}{\MATHIT{goal}}
\newcommand{\SWITCH}{\MATHIT{switch}}
\newcommand{\LIST}{\MATHTT{list}}
\newcommand{\INT}{\MATHTT{int}}
\newcommand{\OPEN}{\MATHTT{Open}}
\newcommand{\CLOSED}{\MATHTT{Closed}}

\newcommand{\SEMOP}[1]{|[#1|]}
\newcommand{\TSEMOP}[1]{{}_t|[#1|]}
\newcommand{\SEM}[3][\xi]{\SEMOP{#2}_{{#1},{#3}}}
\newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle}
\newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}

\newcommand{\GIN}[1][1]{\ensuremath{[l_{#1};\cdots;l_n]}}

\newcommand{\ZEROPOS}{\MATHIT{zero\_pos}}
\newcommand{\INITPOS}{\MATHIT{init\_pos}}
\newcommand{\ISFRESH}{\MATHIT{is\_fresh}}
\newcommand{\FILTER}{\MATHIT{filter}}
\newcommand{\FILTEROPEN}{\MATHIT{filter\_open}}
\newcommand{\ISOPEN}{\MATHIT{is\_open}}
\newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
\newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}}
\newcommand{\GOALS}{\MATHIT{open\_goals}}

\newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}}

\newlength{\sidecondlen}
\setlength{\sidecondlen}{2cm}

\begin{document}
\maketitle

\input{body.tex}

\end{document}

