-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathpaper.tex
181 lines (153 loc) · 6.91 KB
/
paper.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
\documentclass[english,submission]{programming}
\usepackage[backend=bibtex,autopunct=true]{biblatex}
\usepackage{
, coqdoc
, todonotes
, balance
, lettrine % use a large font for first letter
% , MorrisIn % font for starting letter of chapter
% , EileenBl % font for starting letter of chapter
, Zallman % font for starting letter of chapter
}
\usepackage{fancyvrb}
% \renewcommand{\LettrineFontHook}{\MorrisInfamily}
% \renewcommand{\LettrineFontHook}{\EileenBlfamily}
\renewcommand{\LettrineFontHook}{\Zallmanfamily}
\LettrineTextFont{\itshape}
\setcounter{DefaultLines}{3}
\makeatletter
\renewcommand{\verbatim@font}{\ttfamily\small}
\makeatother
% rename figure to scroll
\captionsetup[figure]{name={Scroll}}
\renewcaptionname{english}{\figureautorefname}{Scroll}
\newcommand{\jump}[1]{\vspace{1ex}\noindent\textit{#1}\vspace{1ex}}
\renewenvironment{coqdoccomment}{\small\texttt(*}{*)\normalsize}
\renewenvironment{coqdoccode}{\small}{\normalsize}
\renewcommand{\cite}[1]{\citeauthor*{#1}~\autocite{#1}}
\bibliography{paper}
%% don't color citations/links green
\hypersetup{
colorlinks=false,
pdfborder={0 0 0},
}
\begin{document}
\title{One Monad to Prove Them All}
% \subtitle{Preparing Articles for Programming}% optional
% \titlerunning{Preparing Articles for Programming} %optional, in case that the title is too long; the running title should fit into the top page column
\author[a]{Sandra Dylus}
\authorinfo{\email{[email protected]}}
\affiliation[a]{University of Kiel, Germany}
\author{Jan Christiansen}
\authorinfo{\email{[email protected]}}
\affiliation{Flensburg University of Applied Sciences, Germany}
\author[a]{Finn Teegen}
\authorinfo{\email{[email protected]}}
%% Keywords
%% comma separated list
\keywords{Haskell, monads, free monad, containers, verification} %% \keywords is optional
%%%%%%%%%%%%%%%%%%
%% These data MUST be filled for your submission. (see 5.3)
\paperdetails{
%% perspective options are: art, sciencetheoretical, scienceempirical, engineering.
%% Choose exactly the one that best describes this work. (see 2.1)
perspective=art,
%% State one or more areas, separated by a comma. (see 2.2)
%% Please see list of areas in http://programming-journal.org/cfp/
%% The list is open-ended, so use other areas if yours is/are not listed.
area={General-purpose programming, Program verification},
%% You may choose the license for your paper (see 3.)
%% License options include: cc-by (default), cc-by-nc
% license=cc-by,
}
%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%
%% These data are provided by the editors. May be left out on submission.
%\paperdetails{
% submitted=2016-08-10,
% published=2016-10-11,
% year=2016,
% volume=1,
% issue=1,
% articlenumber=1,
%}
%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Please go to https://dl.acm.org/ccs/ccs.cfm and generate your Classification
% System [view CCS TeX Code] stanz and copy _all of it_ to this place.
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003752.10010124.10010138.10010142</concept_id>
<concept_desc>Theory of computation~Program verification</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011008.10011009.10011012</concept_id>
<concept_desc>Software and its engineering~Functional languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Theory of computation~Program verification}
\ccsdesc[500]{Software and its engineering~Functional languages}
%% End of generated code
%% \maketitle
%% Note: \maketitle command must come after title commands, author
%% commands, abstract environment, Computing Classification System
%% environment and commands, and keywords command.
\maketitle
\begin{abstract}
One Monad to Prove Them All is a modern fairy tale about curiosity and
perseverance, two important properties of a successful PhD student.
We follow the PhD student Mona on her adventure of proving
properties about Haskell programs in the proof assistant Coq.
On the one hand, as a PhD student in computer science Mona observes an increasing demand for correct software products.
In particular, because of the large amount of existing software, verifying existing software products becomes more important.
Verifying programs in the functional programming language Haskell is no exception.
On the other hand, Mona is delighted to see that communities in the
area of theorem proving are becoming popular.
Thus, Mona sets out to learn more about the interactive theorem prover Coq and verifying Haskell programs in Coq.
To prove properties about a Haskell function in Coq, Mona has to
translate the function into Coq code.
As Coq programs have to be total and Haskell programs are often not,
Mona has to model partiality explicitly in Coq.
In her quest for a solution Mona finds an ancient manuscript that explains
how properties about Haskell functions can be proven in the proof
assistant Agda by translating Haskell programs into monadic Agda
programs.
By instantiating the monadic program with a concrete monad instance
the proof can be performed in either a total or a partial setting.
Mona discovers that the proposed transformation does not work in Coq
due to a restriction in the termination checker.
In fact the transformation does not work in Agda anymore as well, as
the termination checker in Agda has been improved.
We follow Mona on an educational journey through the land of functional
programming where she learns about concepts like free
monads and containers as well as basics and restrictions of proof
assistants like Coq.
These concepts are well-known individually, but their interplay gives
rise to a solution for Mona's problem based on the originally proposed
monadic tranformation that has not been presented before.
When Mona starts to test her approach by proving a statement about
simple Haskell functions, she realizes that her approach has an
additional advantage over the original idea in Agda.
Mona's final solution not only works for a specific monad instance
but even allows her to prove monad-generic properties.
Instead of proving properties over and over again for specific monad
instances she is able to prove properties that hold for all monads
representable by a container-based instance of the free monad.
In order to strengthen her confidence in the practicability of her
approach, Mona evaluates her approach in a case study that compares
two implementations for queues.
In order to share the results with other functional programmers the fairy tale is available as a literate Coq file.
If you are a citizen of the land of functional programming or are at
least familiar with its customs, had a journey that involved reasoning
about functional programs of your own, or are just a curious soul
looking for the next story about monads and proofs, then this tale is
for you.
\end{abstract}
\input{FreeMonadicProving}
% bib is defined in *.v-file
%\bibliography{paper}
\end{document}