main.tex

%%
%% This is file `sample-sigplan.tex',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% samples.dtx  (with options: `sigplan')
%% 
%% IMPORTANT NOTICE:
%% 
%% For the copyright see the source file.
%% 
%% Any modified versions of this file must be renamed
%% with new filenames distinct from sample-sigplan.tex.
%% 
%% For distribution of the original source see the terms
%% for copying and modification in the file samples.dtx.
%% 
%% This generated file may be distributed as long as the
%% original source files, as listed above, are part of the
%% same distribution. (The sources need not necessarily be
%% in the same archive or directory.)
%%
%% Commands for TeXCount
%TC:macro \cite [option:text,text]
%TC:macro \citep [option:text,text]
%TC:macro \citet [option:text,text]
%TC:envir table 0 1
%TC:envir table* 0 1
%TC:envir tabular [ignore] word
%TC:envir displaymath 0 word
%TC:envir math 0 word
%TC:envir comment 0 0
%%
%%
%% The first command in your LaTeX source must be the \documentclass command.
%\documentclass[sigplan,screen]{acmart}
\documentclass[sigplan,screen,nonacm]{acmart}
%% NOTE that a single column version is required for 
%% submission and peer review. This can be done by changing
%% the \doucmentclass[...]{acmart} in this template to 
%% \documentclass[manuscript,screen,review]{acmart}
%% 
%% To ensure 100% compatibility, please check the white list of
%% approved LaTeX packages to be used with the Master Article Template at
%% https://www.acm.org/publications/taps/whitelist-of-latex-packages 
%% before creating your document. The white list page provides 
%% information on how to submit additional LaTeX packages for 

\usepackage{mylhs2tex}
\usepackage[backend=pgf, extension=pgf, outputdir=diagrams, input]{diagrams-latex}
\usepackage{tikz}
\usepackage{tikz-cd} % for commutative diagrams
\usepackage{textgreek} % for \textlambda
\usepackage{multirow} % for multirow in tables
\usepackage[inline]{enumitem} % for inline lists
\usepackage{minted} % for code snippets
\usepackage{wrapfig} % for wrapping text around figures
\usepackage{mathpartir} % for inference rules


\newcommand{\REM}[2]{\textcolor{blue}{[\textbf{#1:} #2]}}
\newcommand{\Johan}[1]{\REM{Johan}{#1}}
\newcommand{\Matthias}[1]{\REM{Matthias}{#1}}
\newcommand{\Igor}[1]{\REM{Igor}{#1}}
\newcommand{\nm}{notional machine}
\newcommand{\nms}{notional machines}
\newcommand{\Nm}{Notional machine}
\newcommand{\Nms}{Notional machines}
\newcommand{\NM}{Notional Machine}
\newcommand{\NMs}{Notional Machines}
\newcommand{\nmName}[1]{\textsc{#1}}
\newcommand{\plName}[1]{\textsc{#1}}
\newcommand{\done}{\textcolor[rgb]{0,1,0}{(done)}}
\newcommand{\todo}{\textcolor[rgb]{1,0,0}{TODO }}
\newcommand{\inv}[1]{{#1}^{\scriptscriptstyle -1}}
\newcommand{\numOfNMs}{37\ }

\newcommand{\app}[2]{#1\ #2}
\newcommand{\abs}[2]{\text{\textlambda}#1.#2}
\newcommand{\tyabs}[3]{\text{\textlambda}#1:#2.#3}
\newcommand{\subst}[3]{[#2 \mapsto #1]#3}

\newcommand{\ift}[3]{\texttt{if\;}#1\texttt{\;then\;}#2\texttt{\;else\;}#3}
\newcommand{\succt}[1]{\texttt{succ\;}#1}
\newcommand{\predt}[1]{\texttt{pred\;}#1}
\newcommand{\iszerot}[1]{\texttt{iszero\;}#1}
\newcommand{\true}{\texttt{true}}
\newcommand{\false}{\texttt{false}}
\newcommand{\zero}{0}

\newcommand{\unit}{\texttt{unit}}
\newcommand{\refr}[1]{\texttt{ref\;}#1}
\newcommand{\deref}[1]{\texttt{!}#1}
\newcommand{\assign}[2]{#1\;:= #2}
\newcommand{\seq}[2]{#1;\;#2}
\newcommand{\proj}[2]{#1.#2}

\newcommand{\Bool}{\texttt{Bool}}
\newcommand{\Nat}{\texttt{Nat}}
\newcommand{\Ref}[1]{\texttt{Ref\;}#1}
\newcommand{\Unit}{\texttt{Unit}}
\newcommand{\Fun}[2]{#1 \rightarrow #2}
\newcommand{\Tuple}[1]{\{#1\}}

%% review and adoption.
%% Fonts used in the template cannot be substituted; margin 
%% adjustments are not allowed.
%%
%% \BibTeX command to typeset BibTeX logo in the docs
\AtBeginDocument{%
  \providecommand\BibTeX{{%
    \normalfont B\kern-0.5em{\scshape i\kern-0.25em b}\kern-0.8em\TeX}}}

%% Rights management information.  This information is sent to you
%% when you complete the rights form.  These commands have SAMPLE
%% values in them; it is your responsibility as an author to replace
%% the commands and values with those provided to you when you
%% complete the rights form.
\setcopyright{acmcopyright}
\copyrightyear{2018}
\acmYear{2018}
\acmDOI{XXXXXXX.XXXXXXX}

%% These commands are for a PROCEEDINGS abstract or paper.
\acmConference[Conference acronym 'XX]{Make sure to enter the correct
  conference title from your rights confirmation emai}{June 03--05,
  2018}{Woodstock, NY}
%
%  Uncomment \acmBooktitle if th title of the proceedings is different
%  from ``Proceedings of ...''!
%
%\acmBooktitle{Woodstock '18: ACM Symposium on Neural Gaze Detection,
%  June 03--05, 2018, Woodstock, NY} 
\acmPrice{15.00}
\acmISBN{978-1-4503-XXXX-X/18/06}

\settopmatter{printacmref=false, printccs=true, printfolios=true}

%%
%% Submission ID.
%% Use this when submitting an article to a sponsored event. You'll
%% receive a unique submission ID from the organizers
%% of the event, and this ID should be used as the parameter to this command.
%%\acmSubmissionID{123-A56-BU3}

%%
%% For managing citations, it is recommended to use bibliography
%% files in BibTeX format.
%%
%% You can then either use BibTeX with the ACM-Reference-Format style,
%% or BibLaTeX with the acmnumeric or acmauthoryear sytles, that include
%% support for advanced citation of software artefact from the
%% biblatex-software package, also separately available on CTAN.
%%
%% Look at the sample-*-biblatex.tex files for templates showcasing
%% the biblatex styles.
%%

%%
%% The majority of ACM publications use numbered citations and
%% references.  The command \citestyle{authoryear} switches to the
%% "author year" style.
%%
%% If you are preparing content for an event
%% sponsored by ACM SIGGRAPH, you must use the "author year" style of
%% citations and references.
%% Uncommenting
%% the next command will enable that style.
\citestyle{acmauthoryear}

%%
%% end of the preamble, start of the body of the document source.
\begin{document}

%%
%% The "title" command has an optional parameter,
%% allowing the author to define a "short title" to be used in page headers.
\title{Sound Notional Machines}

%%
%% The "author" command and its associated commands are used to define
%% the authors and their affiliations.
%% Of note is the shared affiliation of the first two authors, and the
%% "authornote" and "authornotemark" commands
%% used to denote shared contribution to the research.
\author{Igor Moreno Santos}
\orcid{0000-0002-7844-2058}
\affiliation{%
  \institution{Universit\`a della Svizzera italiana}
  \city{Lugano}
  \country{Switzerland}
}
\email{igor.moreno.santos@usi.ch}

\author{Matthias Hauswirth}
\orcid{0000-0001-5527-5931}
\affiliation{%
  \institution{Universit\`a della Svizzera italiana}
  \city{Lugano}
  \country{Switzerland}
}
\email{matthias.hauswirth@usi.ch}

\author{Johan Jeuring}
\orcid{0000-0001-5645-7681}
\affiliation{%
  \institution{Utrecht University}
  \city{Utrecht}
  \country{The Netherlands}
}
\email{j.t.jeuring@uu.nl}



%%
%% By default, the full list of authors will be used in the page
%% headers. Often, this list is too long, and will overlap
%% other information printed in the page headers. This command allows
%% the author to define a more concise list
%% of authors' names for this purpose.
%\renewcommand{\shortauthors}{Trovato and Tobin, et al.}

%%
%% The abstract is a short summary of the work to be presented in the
%% article.
\begin{abstract}
%What is a notional machine?
A notional machine is
a pedagogical device
that abstracts away details of the semantics of a programming language 
to focus on some aspects of interest.
%What properties should an NM satisfy?
A \nm{} should be \emph{sound}:
it should be consistent with the corresponding programming language,
and it should be a proper abstraction.
This reduces the risk of it introducing misconceptions in education.
% - Problem
Despite being widely used in computer science education,
\nms{}
are usually not evaluated with respect to their soundness.
% - Solution
To address this problem,
we first introduce a formal definition of soundness for \nms{}.
% -- Explain a bit the formalism
The definition is based on the construction of a commutative diagram that relates
the \nm{} with the aspect of the programming language under its focus.
%
Derived from this formalism,
we present a methodology for
%designing
constructing
sound \nms{},
which we demonstrate by
applying it to
a series of small case studies.
%
We also show how the same formalism can be used to
%Finally, we present a similar methodology to
analyze existing \nms{} and
find
inconsistencies
in them
as well as
propose solutions to these inconsistencies.
%
% - Takeaways
%Our work provides a formal foundation for \nms{} and
The work establishes a firmer ground for research in notional machines
by
serving as a framework to reason about them.
%
% The result is more generally a framework to reason about notional machines
% and as such
% can be used
% in the design, analysis, and evaluation of notional machines,
% as well as
% the construction of automated tools
% based on
% %for
% notional machines.


% Raw abstract
% A notional machine is a pedagogical device that abstracts away details of the semantics of a programming language to focus on some aspects of interest. A notional machine should be sound: it should be consistent with the corresponding programming language, and it should be a proper abstraction. This reduces the risk of it introducing misconceptions in education. Despite being widely used in computer science education, notional machines are usually not evaluated with respect to their soundness. To address this problem, we first introduce a formal definition of soundness for notional machines. The definition is based on the construction of a commutative diagram that relates the notional machine with the aspect of the programming language under its focus. Derived from this formalism, we present a methodology for constructing sound notional machines, which we demonstrate by applying it to a series of small case studies. We also show how the same formalism can be used to analyze existing notional machines and find inconsistencies in them as well as propose solutions to these inconsistencies. The work establishes a firmer ground for research in notional machines by serving as a framework to reason about them.


\end{abstract}

%%
%% The code below is generated by the tool at http://dl.acm.org/ccs.cfm.
%% Please copy and paste the code instead of the example below.
%%
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003456.10003457.10003527</concept_id>
<concept_desc>Social and professional topics~Computing education</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011039</concept_id>
<concept_desc>Software and its engineering~Formal language definitions</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011050</concept_id>
<concept_desc>Software and its engineering~Context specific languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}

\ccsdesc[500]{Social and professional topics~Computing education}
\ccsdesc[500]{Software and its engineering~Formal language definitions}
\ccsdesc[500]{Software and its engineering~Context specific languages}


%%
%% Keywords. The author(s) should pick words that accurately describe
%% the work being presented. Separate the keywords with commas.
\keywords{notional machines, programming education, language semantics, equational reasoning, bisimulation}

%% A "teaser" image appears between the author and affiliation
%% information and the body of the document, and typically spans the
%% page.
%\begin{teaserfigure}
%  \includegraphics[width=\textwidth]{sampleteaser}
%  \caption{Seattle Mariners at Spring Training, 2010.}
%  \Description{Enjoying the baseball game from the third-base
%  seats. Ichiro Suzuki preparing to bat.}
%  \label{fig:teaser}
%\end{teaserfigure}

%\received{20 February 2007}
%\received[revised]{12 March 2009}
%\received[accepted]{5 June 2009}

%%
%% This command processes the author and affiliation and title
%% information and builds the first part of the formatted document.
\maketitle

\input{sections/introduction.tex}
\input{sections/designing-nms.tex}
\input{sections/fixing-nms.tex}
\input{sections/ConcreteSyntax}
\input{sections/evaluation.tex}
\input{sections/related-work.tex}
\input{sections/conclusions.tex}
\input{sections/data-availability-statement.tex}

%%
%% The acknowledgments section is defined using the "acks" environment
%% (and NOT an unnumbered section). This ensures the proper
%% identification of the section in the article metadata, and the
%% consistent spelling of the heading.
\begin{acks}
We would like to thank Luca Chiodini for being a thoughtful critic.
This work was partially funded by the Swiss National Science Foundation project 200021\_184689.
\end{acks}

%%
%% The next two lines define the bibliography style to be used, and
%% the bibliography file.
\bibliographystyle{ACM-Reference-Format}
\bibliography{biblio}

\newpage

%%
%% If your work has an appendix, this is the place to put it.
\appendix

\input{sections/appendix.tex}

\end{document}
\endinput
%%
%% End of file `sample-sigplan.tex'.