git.iko.soy/Idris-dev
on master help sign in
Started a new tutorial. Don't hold your breath.
8fbef42Edwin Brady
tutorial/Makefilenew file+41
compare with master
unifiedsplit
@@ -0,0 +1,41 @@
1+PAPER = idris-tutorial
2+
3+all: ${PAPER}.pdf
4+
5+TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex
6+
7+DIAGS =
8+
9+SOURCES = ${TEXFILES} ${DIAGS} macros.ltx library.ltx literature.bib
10+
11+DITAA = java -jar ~/Downloads/ditaa.jar
12+
13+${PAPER}.pdf: ${SOURCES}
14+# dvipdf ${PAPER}.dvi
15+ pdflatex ${PAPER}
16+ -bibtex ${PAPER}
17+ -pdflatex ${PAPER}
18+ -pdflatex ${PAPER}
19+
20+${PAPER}.ps: ${PAPER}.dvi
21+ dvips -o ${PAPER}.ps ${PAPER}
22+
23+${PAPER}.dvi: $(SOURCES)
24+ -latex ${PAPER}
25+ -bibtex ${PAPER}
26+ -latex ${PAPER}
27+ -latex ${PAPER}
28+
29+progress: .PHONY
30+ wc -w ${TEXFILES}
31+
32+%.png : %.diag
33+ $(DITAA) -o -E $<
34+
35+todropbox: .PHONY
36+ cp ${SOURCES} ~/Dropbox/TeX/ImplDTP/
37+
38+fromdropbox: .PHONY
39+ cp ~/Dropbox/TeX/ImplDTP/* .
40+
41+.PHONY:
tutorial/examples/hello.idrnew file+5
@@ -0,0 +1,5 @@
1+module main;
2+
3+main : IO ();
4+main = putStrLn "Hello world";
5+
tutorial/idris-tutorial.texnew file+40
@@ -0,0 +1,40 @@
1+\documentclass{article}
2+
3+\usepackage{fullpage}
4+\usepackage{palatino}
5+\usepackage{url}
6+\usepackage{fancyvrb}
7+
8+\input{macros.ltx}
9+\input{library.ltx}
10+
11+\newcommand{\Idris}{\textsc{Idris}}
12+
13+\title{Dependently Typed Programming in \Idris{}}
14+\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
15+
16+\begin{document}
17+
18+\maketitle
19+
20+%\tableofcontents
21+
22+\input{intro}
23+\input{starting}
24+
25+%Planned sections
26+
27+\section{Types and Functions}
28+\section{Type Classes}
29+\section{The Well-Typed Interpreter}
30+\section{Views}
31+\section{Theorem Proving}
32+\section{Provisional Definitions}
33+\section{A verified binary adder}
34+
35+\input{miscellany}
36+
37+\bibliographystyle{abbrv}
38+\bibliography{literature.bib}
39+
40+\end{document}
tutorial/intro.texnew file+56
@@ -0,0 +1,56 @@
1+\section{Introduction}
2+
3+In conventional programming languages, there is a clear distinction between
4+\remph{types} and \remph{values}. For example, in Haskell~\cite{haskell-report},
5+the following are types, representing integers, characters, lists of characters,
6+and lists of any value respectively:
7+
8+\begin{itemize}
9+\item \texttt{Int}, \texttt{Char}, \texttt{[Char]}, \texttt{[a]}
10+\end{itemize}
11+
12+\noindent
13+Correspondingly, the following values are examples of inhabitants of those types:
14+
15+\begin{itemize}
16+\item \texttt{42}, \texttt{'a'}, \texttt{"Hello world!"}, \texttt{[2,3,4,5,6]}
17+\end{itemize}
18+
19+In a language with \emph{dependent types}, however, the distinction is less
20+clear. Dependent types allow types to ``depend'' on values. The standard
21+example is the type of lists of a given length\footnote{Typically, and perhaps
22+confusingly, referred to in the dependently typed programming literaute as
23+``vectors''}, \texttt{Vect a n}, where \texttt{a} is the element type and
24+\texttt{n} is the length of the list and can be an arbitrary
25+term.
26+
27+When types can contain values, and where those values describe properties (e.g.
28+the length of a list)
29+functions over those types begin to describe their own properties. For example,
30+concatenating two lists has the property that the resulting list's length is
31+the sum of the lengths of the two input lists. We can therefore give the following type
32+to the \texttt{app} function, which concatenates vectors:
33+
34+\begin{SaveVerbatim}{appendv}
35+
36+app : Vect a n -> Vect a m -> Vect a (n + m);
37+
38+\end{SaveVerbatim}
39+\useverb{appendv}
40+
41+
42+This tutorial introduces \Idris{}, a general purpose dependently typed functional
43+programming language.
44+The goal of the \Idris{} project is to build a dependently typed language suitable
45+for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language
46+which aims to generate efficient executable code. It also has a lightweight foreign
47+function interface which allows easy interaction with external C libraries.
48+
49+\subsection{Intended Audience}
50+
51+This tutorial is intended as a brief introduction to the language, and is aimed
52+at readers already familiar with a functional language such as Haskell or
53+OCaml. In particular, a certain amount of familiarity with Haskell syntax is
54+assumed, although most concepts will at least be explained briefly. The reader
55+is also assumed to have some interest in using dependent types for writing and
56+verifying systems software.
tutorial/library.ltxnew file+325
@@ -0,0 +1,325 @@
1+%%%%%%%%%%%%%%% library file for datatypes etc.
2+
3+%%% Identifiers
4+
5+\newcommand{\va}{\VV{a}}
6+\newcommand{\vb}{\VV{b}}
7+\newcommand{\vc}{\VV{c}}
8+\newcommand{\vd}{\VV{d}}
9+\newcommand{\ve}{\VV{e}}
10+\newcommand{\vf}{\VV{f}}
11+\newcommand{\vg}{\VV{g}}
12+\newcommand{\vh}{\VV{h}}
13+\newcommand{\vi}{\VV{i}}
14+\newcommand{\vj}{\VV{j}}
15+\newcommand{\vk}{\VV{k}}
16+\newcommand{\vl}{\VV{l}}
17+\newcommand{\vm}{\VV{m}}
18+\newcommand{\vn}{\VV{n}}
19+\newcommand{\vo}{\VV{o}}
20+\newcommand{\vp}{\VV{p}}
21+\newcommand{\vq}{\VV{q}}
22+\newcommand{\vr}{\VV{r}}
23+\newcommand{\vs}{\VV{s}}
24+\newcommand{\vt}{\VV{t}}
25+\newcommand{\vu}{\VV{u}}
26+\newcommand{\vv}{\VV{v}}
27+\newcommand{\vw}{\VV{w}}
28+\newcommand{\vx}{\VV{x}}
29+\newcommand{\vy}{\VV{y}}
30+\newcommand{\vz}{\VV{z}}
31+\newcommand{\vA}{\VV{A}}
32+\newcommand{\vB}{\VV{B}}
33+\newcommand{\vC}{\VV{C}}
34+\newcommand{\vD}{\VV{D}}
35+\newcommand{\vE}{\VV{E}}
36+\newcommand{\vF}{\VV{F}}
37+\newcommand{\vG}{\VV{G}}
38+\newcommand{\vH}{\VV{H}}
39+\newcommand{\vI}{\VV{I}}
40+\newcommand{\vJ}{\VV{J}}
41+\newcommand{\vK}{\VV{K}}
42+\newcommand{\vL}{\VV{L}}
43+\newcommand{\vM}{\VV{M}}
44+\newcommand{\vN}{\VV{N}}
45+\newcommand{\vO}{\VV{O}}
46+\newcommand{\vP}{\VV{P}}
47+\newcommand{\vQ}{\VV{Q}}
48+\newcommand{\vR}{\VV{R}}
49+\newcommand{\vS}{\VV{S}}
50+\newcommand{\vT}{\VV{T}}
51+\newcommand{\vU}{\VV{U}}
52+\newcommand{\vV}{\VV{V}}
53+\newcommand{\vW}{\VV{W}}
54+\newcommand{\vX}{\VV{X}}
55+\newcommand{\vY}{\VV{Y}}
56+\newcommand{\vZ}{\VV{Z}}
57+\newcommand{\vas}{\VV{as}}
58+\newcommand{\vbs}{\VV{bs}}
59+\newcommand{\vcs}{\VV{cs}}
60+\newcommand{\vds}{\VV{ds}}
61+\newcommand{\ves}{\VV{es}}
62+\newcommand{\vfs}{\VV{fs}}
63+\newcommand{\vgs}{\VV{gs}}
64+\newcommand{\vhs}{\VV{hs}}
65+\newcommand{\vis}{\VV{is}}
66+\newcommand{\vjs}{\VV{js}}
67+\newcommand{\vks}{\VV{ks}}
68+\newcommand{\vls}{\VV{ls}}
69+\newcommand{\vms}{\VV{ms}}
70+\newcommand{\vns}{\VV{ns}}
71+\newcommand{\vos}{\VV{os}}
72+\newcommand{\vps}{\VV{ps}}
73+\newcommand{\vqs}{\VV{qs}}
74+\newcommand{\vrs}{\VV{rs}}
75+%\newcommand{\vss}{\VV{ss}}
76+\newcommand{\vts}{\VV{ts}}
77+\newcommand{\vus}{\VV{us}}
78+\newcommand{\vvs}{\VV{vs}}
79+\newcommand{\vws}{\VV{ws}}
80+\newcommand{\vxs}{\VV{xs}}
81+\newcommand{\vys}{\VV{ys}}
82+\newcommand{\vzs}{\VV{zs}}
83+
84+%%% Telescope Identifiers
85+
86+\newcommand{\ta}{\vec{\VV{a}}}
87+\newcommand{\tb}{\vec{\VV{b}}}
88+\newcommand{\tc}{\vec{\VV{c}}}
89+\newcommand{\td}{\vec{\VV{d}}}
90+\newcommand{\te}{\vec{\VV{e}}}
91+\newcommand{\tf}{\vec{\VV{f}}}
92+\newcommand{\tg}{\vec{\VV{g}}}
93+%\newcommand{\th}{\vec{\VV{h}}}
94+\newcommand{\ti}{\vec{\VV{i}}}
95+\newcommand{\tj}{\vec{\VV{j}}}
96+\newcommand{\tk}{\vec{\VV{k}}}
97+\newcommand{\tl}{\vec{\VV{l}}}
98+\newcommand{\tm}{\vec{\VV{m}}}
99+\newcommand{\tn}{\vec{\VV{n}}}
100+%\newcommand{\to}{\vec{\VV{o}}}
101+\newcommand{\tp}{\vec{\VV{p}}}
102+\newcommand{\tq}{\vec{\VV{q}}}
103+\newcommand{\tr}{\vec{\VV{r}}}
104+\newcommand{\tts}{\vec{\VV{s}}}
105+\newcommand{\ttt}{\vec{\VV{t}}}
106+\newcommand{\tu}{\vec{\VV{u}}}
107+%\newcommand{\tv}{\vec{\VV{v}}}
108+\newcommand{\tw}{\vec{\VV{w}}}
109+\newcommand{\tx}{\vec{\VV{x}}}
110+\newcommand{\ty}{\vec{\VV{y}}}
111+\newcommand{\tz}{\vec{\VV{z}}}
112+\newcommand{\tA}{\vec{\VV{A}}}
113+\newcommand{\tB}{\vec{\VV{B}}}
114+\newcommand{\tC}{\vec{\VV{C}}}
115+\newcommand{\tD}{\vec{\VV{D}}}
116+\newcommand{\tE}{\vec{\VV{E}}}
117+\newcommand{\tF}{\vec{\VV{F}}}
118+\newcommand{\tG}{\vec{\VV{G}}}
119+\newcommand{\tH}{\vec{\VV{H}}}
120+\newcommand{\tI}{\vec{\VV{I}}}
121+\newcommand{\tJ}{\vec{\VV{J}}}
122+\newcommand{\tK}{\vec{\VV{K}}}
123+\newcommand{\tL}{\vec{\VV{L}}}
124+\newcommand{\tM}{\vec{\VV{M}}}
125+\newcommand{\tN}{\vec{\VV{N}}}
126+\newcommand{\tO}{\vec{\VV{O}}}
127+\newcommand{\tP}{\vec{\VV{P}}}
128+\newcommand{\tQ}{\vec{\VV{Q}}}
129+\newcommand{\tR}{\vec{\VV{R}}}
130+\newcommand{\tS}{\vec{\VV{S}}}
131+\newcommand{\tT}{\vec{\VV{T}}}
132+\newcommand{\tU}{\vec{\VV{U}}}
133+\newcommand{\tV}{\vec{\VV{V}}}
134+\newcommand{\tW}{\vec{\VV{W}}}
135+\newcommand{\tX}{\vec{\VV{X}}}
136+\newcommand{\tY}{\vec{\VV{Y}}}
137+\newcommand{\tZ}{\vec{\VV{Z}}}
138+
139+
140+
141+%%% Nat
142+
143+\newcommand{\NatPackage}{
144+ \newcommand{\Nat}{\TC{\mathbb{N}}}
145+ \newcommand{\Z}{\DC{0}}
146+ \newcommand{\suc}{\DC{s}}
147+ \newcommand{\NatDecl}{
148+ \Data \hg
149+ \Axiom{\Nat\Hab\Type} \hg
150+ \Where \hg
151+ \Axiom{\Z\Hab\Nat} \hg
152+ \Rule{\vn\Hab\Nat}
153+ {\suc\:\vn\Hab\Nat}
154+}}
155+
156+%%% Bool
157+
158+\newcommand{\BoolPackage}{
159+ \newcommand{\Bool}{\TC{Bool}}
160+ \newcommand{\true}{\DC{true}}
161+ \newcommand{\false}{\DC{false}}
162+ \newcommand{\BoolDecl}{
163+ \Data \hg
164+ \Axiom{\Bool\Hab\Type} \hg
165+ \Where \hg
166+ \Axiom{\true\Hab\Bool} \hg
167+ \Axiom{\false\Hab\Bool}
168+}}
169+
170+%%% So
171+
172+\newcommand{\SoPackage}{
173+ \newcommand{\So}{\TC{So}}
174+ \newcommand{\oh}{\DC{oh}}
175+ \newcommand{\SoDecl}{
176+ \Data \hg
177+ \Rule{\vb\Hab\Bool}
178+ {\So\:\vb\Hab\Type} \hg
179+ \Where \hg
180+ \Axiom{\oh\Hab\So\:\true}
181+}}
182+
183+%%% Unit
184+
185+\newcommand{\UnitPackage}{
186+ \newcommand{\Unit}{\TC{Unit}}
187+ \newcommand{\void}{\DC{void}}
188+ \newcommand{\UnitDecl}{
189+ \Data \hg
190+ \Axiom{\Unit\Hab\Type} \hg
191+ \Where \hg
192+ \Axiom{\void\Hab\Unit}
193+}}
194+
195+%%% Maybe
196+
197+\newcommand{\MaybePackage}{
198+ \newcommand{\Maybe}{\TC{Maybe}}
199+ \newcommand{\yes}{\DC{yes}}
200+ \newcommand{\no}{\DC{no}}
201+ \newcommand{\MaybeDecl}{
202+ \Data \hg
203+ \Rule{\vA\Hab\Type}
204+ {\Maybe\:\vA\Hab\Type} \hg
205+ \Where \hg
206+ \Rule{\va \Hab \vA}
207+ {\yes\:\va\Hab\Maybe\:\vA} \hg
208+ \Axiom{\no\Hab\Maybe\:\vA}
209+}}
210+
211+%%% Cross
212+
213+\newcommand{\pr}[2]{(#1\DC{,}#2)} %grrrr
214+\newcommand{\CrossPackage}{
215+ \newcommand{\Cross}{\times}
216+ \newcommand{\CrossDecl}{
217+ \Data \hg
218+ \Rule{\vA,\vB\Hab\Type}
219+ {\vA\Cross\vB\Hab\Type} \hg
220+ \Where \hg
221+ \Rule{\va \Hab \vA \hg \vb\Hab\vB}
222+ {\pr{\va}{\vb}\Hab\vA\Cross\vB}
223+}}
224+
225+%%% Fin
226+
227+\newcommand{\FinPackage}{
228+ \newcommand{\Fin}{\TC{Fin}}
229+ \newcommand{\fz}{\DC{f0}}
230+ \newcommand{\fs}{\DC{fs}}
231+ \newcommand{\FinDecl}{
232+ \AR{
233+ \Data \hg
234+ \Rule{\vn\Hab\Nat}
235+ {\Fin\:\vn\Hab\Type} \hg \\
236+ \Where \hg
237+ \begin{array}[t]{c}
238+ \Axiom{\fz\Hab\Fin\:(\suc\:\vn)} \hg
239+ \Rule{\vi\Hab\Fin\:\vn}
240+ {\fs\:\vi\Hab\Fin\:(\suc\:\vn)}
241+ \end{array}
242+ }
243+}}
244+
245+%%% Vect
246+
247+\newcommand{\VectPackage}{
248+ \newcommand{\Vect}{\TC{Vect}}
249+ \newcommand{\vnil}{\varepsilon}
250+ \newcommand{\vcons}{\,\dcolon\,}
251+ \newcommand{\vsnoc}{\,\dcolon\,}
252+ \newcommand{\VectConsDecl}{
253+ \Data \hg
254+ \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
255+ {\Vect\:\vA\:\vn\Hab\Type} \hg
256+ \Where \hg \begin{array}[t]{c}
257+ \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
258+ \Rule{\vx\Hab\vA \hg \vxs\Hab \Vect\:\vA\:\vn }
259+ {\vx\vcons\vxs\Hab\Vect\:\vA\:(\suc\vn)}
260+ \end{array}
261+}
262+ \newcommand{\VectSnocDecl}{
263+ \Data \hg
264+ \Rule{\vA \Hab \Type \hg \vn\Hab\Nat}
265+ {\Vect\:\vA\:\vn\Hab\Type} \hg
266+ \Where \hg \begin{array}[t]{c}
267+ \Axiom{\vnil \Hab \Vect\:\vA\:\Z} \\
268+ \Rule{\vxs\Hab \Vect\:\vA\:\vn \hg \vx\Hab\vA}
269+ {\vxs\vsnoc\vx\Hab\Vect\:\vA\:(\suc\vn)}
270+ \end{array}
271+}
272+}
273+
274+%%% Compare
275+
276+%Data Compare : (x:nat)(y:nat)Type
277+% = lt : (x:nat)(y:nat)(Compare x (plus (S y) x))
278+% | eq : (x:nat)(Compare x x)
279+% | gt : (x:nat)(y:nat)(Compare (plus (S x) y) y);
280+
281+
282+\newcommand{\ComparePackage}{
283+ \newcommand{\Compare}{\TC{Compare}}
284+ \newcommand{\ltComp}{\DC{lt}}
285+ \newcommand{\eqComp}{\DC{eq}}
286+ \newcommand{\gtComp}{\DC{gt}}
287+ \newcommand{\CompareDecl}{
288+ \Data \hg
289+ \Rule{\vm\Hab\Nat\hg\vn\Hab\Nat}
290+ {\Compare\:\vm\:\vn\Hab\Type} \\
291+ \Where \hg\begin{array}[t]{c}
292+ \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
293+ {\ltComp_{\vx}\:\vy\Hab\Compare\:\vx\:(\FN{plus}\:\vx\:(\suc\:\vy))} \\
294+ \Rule{\vx\Hab\Nat}
295+ {\eqComp_{\vx}\Hab\Compare\:\vx\:\vx}\\
296+ \Rule{\vx\Hab\Nat\hg\vy\Hab\Nat}
297+ {\gtComp_{\vy}\:\vx\Hab\Compare\:(\FN{plus}\:\vy\:(\suc\:\vx))\:\vy} \\
298+ \end{array}
299+ }
300+
301+%Data CompareM : Type
302+% = ltM : (ydiff:nat)CompareM
303+% | eqM : CompareM
304+% | gtM : (xdiff:nat)CompareM;
305+
306+ \newcommand{\CompareM}{\TC{Compare^-}}
307+ \newcommand{\ltCompM}{\DC{lt^-}}
308+ \newcommand{\eqCompM}{\DC{eq^-}}
309+ \newcommand{\gtCompM}{\DC{gt^-}}
310+ \newcommand{\CompareMDecl}{
311+
312+ \Data \hg
313+ \Axiom{\CompareM\Hab\Type} \\
314+ \Where \hg\begin{array}[t]{c}
315+ \Rule{\vy\Hab\Nat}
316+ {\ltCompM\:\vy\Hab\CompareM} \\
317+ \Axiom{\eqCompM\Hab\CompareM}\\
318+ \Rule{\vx\Hab\Nat}
319+ {\gtCompM\:\vx\Hab\CompareM} \\
320+ \end{array}
321+ }
322+ \newcommand{\CompareRec}{\FN{CompareRec}}
323+ \newcommand{\CompareRecM}{\FN{CompareRec^-}}
324+
325+}
tutorial/literature.bibnew file+3846
@@ -0,0 +1,3846 @@
1+@article{lambdapi,
2+ author = {Andres L\"{o}h and Conor McBride and Wouter Swierstra},
3+ title = {A tutorial implementation of a dependently typed lambda calculus},
4+ year = 2010,
5+ journal = {Fundamenta Informaticae},
6+ volume = 102,
7+ number = 2
8+}
9+
10+@article{idioms,
11+ author = {McBride, Conor and Paterson, Ross},
12+ title = {Applicative programming with effects},
13+ journal = {J. Funct. Program.},
14+ volume = {18},
15+ issue = {1},
16+ month = {January},
17+ year = {2008},
18+ issn = {0956-7968},
19+ pages = {1--13},
20+ numpages = {13},
21+ url = {http://portal.acm.org/citation.cfm?id=1348940.1348941},
22+ doi = {10.1017/S0956796807006326},
23+ acmid = {1348941},
24+ publisher = {Cambridge University Press},
25+ address = {New York, NY, USA},
26+}
27+
28+@inproceedings{lava,
29+ author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam},
30+ title = {Lava: hardware design in {Haskell}},
31+ booktitle = {Proceedings of the third ACM SIGPLAN international conference on Functional programming},
32+ series = {ICFP '98},
33+ year = {1998},
34+ isbn = {1-58113-024-4},
35+ location = {Baltimore, Maryland, United States},
36+ pages = {174--184},
37+ numpages = {11},
38+ url = {http://doi.acm.org/10.1145/289423.289440},
39+ doi = {http://doi.acm.org/10.1145/289423.289440},
40+ acmid = {289440},
41+ publisher = {ACM},
42+ address = {New York, NY, USA},
43+}
44+
45+@inproceedings{plpv11,
46+ author = {Edwin Brady},
47+ title = {Idris --- Systems programming meets full dependent types},
48+ booktitle = {Programming Languages meets Program Verification {(PLPV 2011)}},
49+ year = {2011},
50+ pages = {43--54},
51+ ee = {http://doi.acm.org/10.1145/1929529.1929536},
52+ bibsource = {DBLP, http://dblp.uni-trier.de}
53+}
54+
55+@inproceedings{epic-tfp,
56+ author = {Edwin Brady},
57+ title = {Epic --- a library for generating compilers},
58+ year = 2011,
59+ booktitle = {{Trends in Functional Programming} ({TFP} '11)},
60+ note = {To appear}
61+}
62+
63+@inproceedings{ynot08,
64+ author = {Nanevski,, Aleksandar and Morrisett,, Greg and
65+ Shinnar,, Avraham and Govereau,, Paul and Birkedal,,
66+ Lars},
67+ title = {Ynot: reasoning with the awkward squad},
68+ booktitle = {{ICFP} '08: Proceeding of the 13th {ACM SIGPLAN}
69+ international conference on Functional programming},
70+ year = {2008},
71+ isbn = {978-1-59593-919-7},
72+ pages = {229--240},
73+ location = {Victoria, BC, Canada},
74+ doi = {http://doi.acm.org/10.1145/1411204.1411237},
75+ publisher = {ACM},
76+ address = {New York, NY, USA},
77+}
78+
79+@article{cbconc-fi,
80+ author = {Edwin Brady and Kevin Hammond},
81+ title = {Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols},
82+ year = 2010,
83+ journal = {Fundamenta Informaticae},
84+ volume = 102,
85+ number = 2,
86+ pages = {145--176}
87+}
88+
89+@inproceedings{devil-osdi00,
90+ author = {Fabrice M{\'e}rillon and
91+ Laurent R{\'e}veill{\`e}re and
92+ Charles Consel and
93+ Renaud Marlet and
94+ Gilles Muller},
95+ title = {Devil: An IDL for Hardware Programming},
96+ booktitle = {4th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2000)},
97+ year = {2000}
98+}
99+
100+
101+@INPROCEEDINGS{device-osdi08,
102+ author = {Dan Williams and Patrick Reynolds and Kevin Walsh and Emin Gün Sirer and Fred B. Schneider},
103+ title = {Device driver safety through a reference validation mechanism},
104+ booktitle = {8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008)},
105+ year = {2008}
106+}
107+
108+@inproceedings{sozeau-equations,
109+ author = {Matthieu Sozeau},
110+ title = {Equations: A Dependent Pattern-Matching Compiler},
111+ booktitle = {First International Conference on Interactive Theorem Proving (ITP 2010)},
112+ year = {2010},
113+ pages = {419--434},
114+ ee = {http://dx.doi.org/10.1007/978-3-642-14052-5_29},
115+ crossref = {DBLP:conf/itp/2010},
116+ bibsource = {DBLP, http://dblp.uni-trier.de}
117+}
118+
119+
120+@inproceedings{packet-type,
121+ author = "Peter J. McCann and Satish Chandra",
122+ title = "Packet Types: Abstract Specification of Network Protocol Messages",
123+ year = 2000,
124+ booktitle = "SIGCOMM '00",
125+ publisher = {{ACM}}
126+}
127+
128+@inproceedings{qs-types,
129+ author = {Eelis {van der Weegen} and James McKinna},
130+
131+ title={A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq},
132+ year={2009},
133+ pages={256--271},
134+ series = {Lecture Notes in Computer Science},
135+ publisher = {Springer}
136+
137+}
138+
139+@inproceedings{totalparser,
140+ author = {Nils Anders Danielsson},
141+ title = {Total Parser Combinators},
142+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
143+ year = {2010},
144+ isbn = {978-1-60558-794-3},
145+ pages = {285--296},
146+ location = {Baltimore, Maryland, USA},
147+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},
148+ publisher = {{ACM}},
149+ address = {New York, NY, USA},
150+ }
151+
152+@misc{rfc791,
153+ author="J. Postel",
154+ title="{Internet Protocol}",
155+ series="Request for Comments",
156+ number="791",
157+ howpublished="RFC 791 (Standard)",
158+ publisher="IETF",
159+ organization="Internet Engineering Task Force",
160+ year=1981,
161+ month=sep,
162+ note="Updated by RFC 1349",
163+ url="http://www.ietf.org/rfc/rfc791.txt",
164+}
165+
166+
167+@misc{rfc792,
168+ author="J. Postel",
169+ title="{Internet Control Message Protocol}",
170+ series="Request for Comments",
171+ number="792",
172+ howpublished="RFC 792 (Standard)",
173+ publisher="IETF",
174+ organization="Internet Engineering Task Force",
175+ year=1981,
176+ month=sep,
177+ note="Updated by RFCs 950, 4884",
178+ url="http://www.ietf.org/rfc/rfc792.txt",
179+}
180+
181+@INPROCEEDINGS{Dybjer-indrec,
182+ author = {Peter Dybjer and Anton Setzer},
183+ title = {A Finite Axiomatization of Inductive-Recursive Definitions},
184+ booktitle = {Tyed Lambda Calculi and Applications},
185+ volume = {1581},
186+ series = {Lecture Notes in Computer Science},
187+ year = {1998},
188+ pages = {129--146},
189+ publisher = {Springer}
190+}
191+
192+@book{stevenstcpip,
193+ author = {W. Richard Stevens},
194+ title = {{TCP/IP} Illustrated Volume 1: The Protocols},
195+ year = 1994,
196+ publisher = {Addison Wesley},
197+ isbn = {0-201-63346-9}
198+}
199+
200+@inproceedings{coqtypeclasses,
201+ author = {Sozeau, Matthieu and Oury, Nicolas},
202+ title = {First-Class Type Classes},
203+ booktitle = {TPHOLs '08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics},
204+ year = {2008},
205+ isbn = {978-3-540-71065-3},
206+ pages = {278--293},
207+ location = {Montreal, P.Q., Canada},
208+ doi = {http://dx.doi.org/10.1007/978-3-540-71067-7_23},
209+ publisher = {Springer-Verlag},
210+ address = {Berlin, Heidelberg},
211+ }
212+
213+
214+@inproceedings{kipling,
215+ author = {McBride, Conor},
216+ title = {Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation},
217+ booktitle = {WGP '10: Proceedings of the 6th {ACM} {SIGPLAN} workshop on Generic programming},
218+ year = {2010},
219+ isbn = {978-1-4503-0251-7},
220+ pages = {1--12},
221+ location = {Baltimore, Maryland, USA},
222+ doi = {http://doi.{ACM}.org/10.1145/1863495.1863497},
223+ publisher = {{ACM}},
224+ address = {New York, NY, USA},
225+ }
226+
227+@inproceedings{padsml,
228+ author = {Yitzhak Mandelbaum and
229+ Kathleen Fisher and
230+ David Walker and
231+ Mary F. Fern{\'a}ndez and
232+ Artem Gleyzer},
233+ title = {{PADS/ML}: a functional data description language},
234+ booktitle = {POPL '07: Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on
235+ Principles of Programming Languages, POPL 2007, Nice, France,
236+ January 17-19, 2007},
237+ year = {2007},
238+ pages = {77-83},
239+ ee = {http://doi.{ACM}.org/10.1145/1190216.1190231},
240+ crossref = {DBLP:conf/popl/2007},
241+ bibsource = {DBLP, http://dblp.uni-trier.de}
242+}
243+
244+@proceedings{DBLP:conf/popl/2007,
245+ editor = {Martin Hofmann and
246+ Matthias Felleisen},
247+ title = {Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on
248+ Principles of Programming Languages, POPL 2007, Nice, France,
249+ January 17-19, 2007},
250+ booktitle = {POPL},
251+ publisher = {{ACM}},
252+ year = {2007},
253+ isbn = {1-59593-575-4},
254+ bibsource = {DBLP, http://dblp.uni-trier.de}
255+}
256+
257+@inproceedings{melange,
258+ author = {Madhavapeddy, Anil and Ho, Alex and Deegan, Tim and Scott, David and Sohan, Ripduman},
259+ title = {Melange: creating a "functional" internet},
260+ booktitle = {EuroSys '07: Proceedings of the 2nd {ACM} SIGOPS/EuroSys European Conference on Computer Systems 2007},
261+ year = {2007},
262+ isbn = {978-1-59593-636-3},
263+ location = {Lisbon, Portugal},
264+ doi = {http://doi.{ACM}.org/10.1145/1272996.1273009},
265+ publisher = {{ACM}},
266+ address = {New York, NY, USA},
267+ }
268+
269+
270+
271+@article{next700data,
272+ author = {Fisher, Kathleen and Mandelbaum, Yitzhak and Walker, David},
273+ title = {The next 700 data description languages},
274+ journal = {{SIGPLAN} Not.},
275+ volume = {41},
276+ number = {1},
277+ year = {2006},
278+ issn = {0362-1340},
279+ pages = {2--15},
280+ doi = {http://doi.{ACM}.org/10.1145/1111320.1111039},
281+ publisher = {{ACM}},
282+ address = {New York, NY, USA},
283+ }
284+
285+
286+@INPROCEEDINGS{xi-ats,
287+ author = {Hongwei Xi},
288+ title = {{Applied Type System} (extended abstract)},
289+ booktitle = {Types for Proofs and Programs 2003},
290+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
291+ publisher = {Springer},
292+ series = {Lecture Notes in Computer Science},
293+ volume = {3085},
294+ year = {2004},
295+ pages = {394--408}
296+}
297+
298+@inproceedings{powerpi,
299+ author = {Nicolas Oury and
300+ Wouter Swierstra},
301+ title = {The power of {Pi}},
302+ booktitle = {{ICFP} '08: Proceedings of the 13th {ACM} {SIGPLAN} International Conference
303+ on Functional Programming, {ICFP} 2008, Victoria, BC, Canada,
304+ September 20-28, 2008},
305+ year = {2008},
306+ pages = {39--50},
307+ ee = {http://doi.{ACM}.org/10.1145/1411204.1411213},
308+ crossref = {DBLP:conf/{ICFP}/2008},
309+ bibsource = {DBLP, http://dblp.uni-trier.de}
310+}
311+
312+@proceedings{DBLP:conf/{ICFP}/2008,
313+ editor = {James Hook and
314+ Peter Thiemann},
315+ title = {Proceeding of the 13th {ACM} {SIGPLAN} international conference
316+ on Functional programming, {ICFP} 2008, Victoria, BC, Canada,
317+ September 20-28, 2008},
318+ booktitle = {{ICFP}},
319+ publisher = {{ACM}},
320+ year = {2008},
321+ isbn = {978-1-59593-919-7},
322+ bibsource = {DBLP, http://dblp.uni-trier.de}
323+}
324+
325+
326+@inproceedings{security-types,
327+ author = {Morgenstern, Jamie and Licata, Daniel R.},
328+ title = {Security-typed programming within dependently typed programming},
329+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
330+ year = {2010},
331+ isbn = {978-1-60558-794-3},
332+ pages = {169--180},
333+ location = {Baltimore, Maryland, USA},
334+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863569},
335+ publisher = {{ACM}},
336+ address = {New York, NY, USA},
337+ }
338+
339+@inproceedings{levitation,
340+ author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
341+ title = {The gentle art of levitation},
342+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
343+ year = {2010},
344+ isbn = {978-1-60558-794-3},
345+ pages = {3--14},
346+ location = {Baltimore, Maryland, USA},
347+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863547},
348+ publisher = {{ACM}},
349+ address = {New York, NY, USA},
350+ }
351+
352+
353+
354+@INPROCEEDINGS{awkward,
355+ author = {Simon {Peyton Jones}},
356+ title = {Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in {Haskell}},
357+ booktitle = {Engineering theories of software construction},
358+ year = {2001},
359+ pages = {47--96}
360+}
361+
362+@inproceedings{scrap-engine,
363+ author = {Brady, Edwin and Hammond, Kevin},
364+ title = {Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation},
365+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
366+ year = {2010},
367+ isbn = {978-1-60558-794-3},
368+ pages = {297--308},
369+ location = {Baltimore, Maryland, USA},
370+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},
371+ publisher = {{ACM}},
372+ address = {New York, NY, USA},
373+ }
374+
375+@article{urweb,
376+ author = {Chlipala, Adam},
377+ title = {Ur: statically-typed metaprogramming with type-level record computation},
378+ journal = {{SIGPLAN} Not.},
379+ volume = {45},
380+ number = {6},
381+ year = {2010},
382+ issn = {0362-1340},
383+ pages = {122--133},
384+ doi = {http://doi.{ACM}.org/10.1145/1809028.1806612},
385+ publisher = {{ACM}},
386+ address = {New York, NY, USA},
387+ }
388+
389+
390+
391+@phdthesis{norell-thesis,
392+ author = {Ulf Norell},
393+ title = {Towards a practical programming language based on dependent type
394+ theory},
395+ school = {Chalmers University of Technology},
396+ year = 2007,
397+ month = {September},
398+}
399+
400+@inproceedings{open-type,
401+ author = {Schrijvers, Tom and Peyton Jones, Simon and Chakravarty, Manuel and Sulzmann, Martin},
402+ title = {Type checking with open type functions},
403+ booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},
404+ year = {2008},
405+ pages = {51--62},
406+ doi = {http://doi.{ACM}.org/10.1145/1411203.1411215},
407+ publisher = {{ACM}},
408+ address = {New York, NY, USA},
409+ }
410+
411+@inproceedings{ngna-dsl,
412+ title = {Domain Specific Languages ({DSL}s) for Network Protocols},
413+ author = {Saleem Bhatti and Edwin Brady and Kevin Hammond and James McKinna},
414+ year = {2009},
415+ booktitle = {International Workshop on Next Generation Network Architecture ({NGNA} 2009)}
416+}
417+
418+@phdthesis{gill-thesis,
419+ title = {Cheap deforestation for non-strict functional languages},
420+ author = {A Gill},
421+ institution = {University of Glasgow},
422+ month = {January},
423+ year = 1996
424+}
425+
426+@misc{llvm-haskell,
427+ title = {Low Level Virtual Machine for {Glasgow Haskell Compiler}},
428+ author = {David Terei},
429+ year = 2009,
430+ howpublished = {Bachelor's Thesis, Computer Science and Engineering Dept., The University of New South Wales, Sydney, Australia}
431+}
432+
433+@mastersthesis{llvm,
434+ title = {{LLVM}: An Infrastructure for Multi-Stage Optimization},
435+ author = {Chris Lattner},
436+ year = 2002,
437+ month = {December},
438+ institution = {Computer Science Dept., University of Illinois at Urbana-Champaign}
439+}
440+
441+@inproceedings{gpu-arrays,
442+ title = {GPU Kernels as Data-Parallel Array Computations in Haskell},
443+ author = {Sean Lee and Manuel M. T. Chakravarty and Vinod Grover and Gabriele Keller.},
444+ year = 2009,
445+ booktitle = {Workshop on Exploiting Parallelism using GPUs and other Hardware-Assisted Methods (EPAHM 2009)}
446+}
447+
448+@misc{cryptol,
449+ author = {Galois, Inc.},
450+ title = {Cryptol},
451+ year = {2009},
452+ howpublished = {\url{http://cryptol.net/}}
453+}
454+
455+@inproceedings{paradise-dsl,
456+ author = {Lennart Augustsson and Howard Mansell and Ganesh Sittampalam},
457+ title = {{Paradise: a two-stage DSL embedded in Haskell}},
458+ booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},
459+ year = {2008},
460+ publisher = {{ACM}},
461+ pages = {225--228}
462+ }
463+
464+@misc{dsl-bib,
465+ author = {Arie {van Deursen} and Paul Klint and Joost Visser},
466+ title = {Domain-Specific Languages --- an annotated bibliography},
467+ year = 2000,
468+ howpublished = {\url{http://homepages.cwi.nl/~arie/papers/dslbib/}}
469+}
470+
471+@inproceedings{imperative-pe,
472+ author = {Debois, S{\o}ren},
473+ title = {Imperative program optimization by partial evaluation},
474+ booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
475+ year = {2004},
476+ isbn = {1-58113-835-0},
477+ pages = {113--122},
478+ location = {Verona, Italy},
479+ doi = {http://doi.{ACM}.org/10.1145/1014007.1014019},
480+ publisher = {{ACM}},
481+ address = {New York, NY, USA},
482+ }
483+
484+
485+@inproceedings{offline-pe-termination,
486+ author = {Andersen, Peter Holst and Holst, Carsten Kehler},
487+ title = {Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language},
488+ booktitle = {Proc. SAS '96: Intl. Symp. on Static Analysis},
489+ year = {1996},
490+ isbn = {3-540-61739-6},
491+ pages = {67--82},
492+ publisher = {Springer},
493+ notaddress = {London, UK},
494+ }
495+
496+
497+@inproceedings{stage-duplication,
498+ author = {Swadi, Kedar and Taha, Walid and Kiselyov, Oleg and Pasalic, Emir},
499+ title = {A monadic approach for avoiding code duplication when staging memoized functions},
500+ notbooktitle = {PEPM '06: Proceedings of the 2006 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
501+ booktitle = {Proc. PEPM '06:{ACM} Symp. on Partial Evaluation and Semantics-based Program Manipulation},
502+ year = {2006},
503+ isbn = {1-59593-196-1},
504+ pages = {160--169},
505+ location = {Charleston, South Carolina},
506+ doi = {http://doi.{ACM}.org/10.1145/1111542.1111570},
507+ notpublisher = {{ACM}},
508+ notaddress = {New York, NY, USA},
509+ }
510+
511+
512+@inproceedings{concoqtion,
513+ author = {Fogarty, Seth and Pasalic, Emir and Siek, Jeremy and Taha, Walid},
514+ title = {Concoqtion: indexed types now!},
515+ booktitle = {PEPM '07: Proceedings of the 2007 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
516+ year = {2007},
517+ isbn = {978-1-59593-620-2},
518+ pages = {112--121},
519+ location = {Nice, France},
520+ doi = {http://doi.{ACM}.org/10.1145/1244381.1244400},
521+ publisher = {{ACM}},
522+ address = {New York, NY, USA},
523+ }
524+
525+@inproceedings{metahaskell,
526+ author = "Tim Sheard and Simon {Peyton Jones}",
527+ title = "Template metaprogramming for {Haskell}",
528+ booktitle = "{ACM} Haskell Workshop",
529+ year = 2002,
530+ month = oct,
531+ pages = "1-16",
532+ noteditor = "Manuel M. T. Chakravarty",
533+ notpublisher = "{ACM} Press"
534+}
535+
536+@misc{shark-profiler,
537+ title = {Optimizing your application with {Shark 4}},
538+ year = 2009,
539+ howpublished = {\url{http://developer.apple.com/tools/sharkoptimize.html}}
540+}
541+
542+@misc{shootout,
543+ title = {The Computer Language Benchmark Game},
544+ year = {2009},
545+ howpublished = {\url{http://shootout.alioth.debian.org/}}
546+}
547+
548+@article{futamura,
549+ author = {Yoshihiko Futamura},
550+ year = 1971,
551+ title = "Partial Evaluation of Computation Process --– An Approach to a Compiler-Compiler",
552+ journal = {Systems, Comps., Controls},
553+ volume = 2,
554+ number = 5,
555+ pages = {45-–50}
556+}
557+
558+@book{pebook,
559+ title = {Partial Evaluation and Automatic Program Generation},
560+ author = {N.D. Jones and C.K. Gomard and P. Sestoft},
561+ year = 1993,
562+ publisher = {Prentice Hall International}
563+}
564+
565+@inproceedings{pantheon,
566+ author = {Sean Seefried and Manuel Chakravarty and Gabriele Keller},
567+ title = {Optimising Embedded {DSLs} using {Template Haskell}},
568+ year = {2004},
569+ booktitle = {{Proc. GPCE~'04: Conf. Generative Prog. and Component Eng.}},
570+ publisher = {Springer},
571+ series = {LNCS}
572+}
573+
574+@article{pan,
575+ author = {Elliott, Conal and Finne, Sigbj\orn and De Moor, Oege},
576+ title = {Compiling embedded languages},
577+ journal = {J. Funct. Program.},
578+ volume = {13},
579+ number = {3},
580+ year = {2003},
581+ issn = {0956-7968},
582+ pages = {455--481},
583+ doi = {http://dx.doi.org/10.1017/S0956796802004574},
584+ publisher = {Cambridge University Press},
585+ address = {New York, NY, USA},
586+ }
587+
588+
589+@inproceedings{russell,
590+ author = {Sozeau, Matthieu},
591+ title = {Program-ing finger trees in Coq},
592+ booktitle = {{ICFP} '07: Proceedings of the 12th {ACM} {SIGPLAN} international conference on Functional programming},
593+ year = {2007},
594+ isbn = {978-1-59593-815-2},
595+ pages = {13--24},
596+ location = {Freiburg, Germany},
597+ doi = {http://doi.{ACM}.org/10.1145/1291151.1291156},
598+ publisher = {{ACM}},
599+ address = {New York, NY, USA},
600+ }
601+
602+@inproceedings{turner-total,
603+ author = {D. A. Turner},
604+ title = {Elementary Strong Functional Programming},
605+ year = 1995,
606+ booktitle = "First International Symposium on Functional Programming Languages in Education",
607+ publisher = {Springer},
608+ series = {LNCS},
609+ volume = {1022},
610+ pages = {1--13}
611+}
612+
613+@incollection{free-theorems,
614+ author = "P. Wadler",
615+ title = "Theorems for Free!",
616+ booktitle = "{Proc. 4th Int.\ Conf.\ on Funct.\ Prog.\ Languages and Computer Arch., {FPCA}'89, London, {UK}, 11--13 Sept 1989}",
617+ publisher = "{ACM} Press",
618+ address = "New York",
619+ pages = "347--359",
620+ year = "1989",
621+ url = "citeseer.ist.psu.edu/wadler89theorems.html"
622+}
623+
624+@inproceedings{TrulyConcurrent,
625+ author = {Naiyong Jin and Jifeng He},
626+ title = {Towards A Truly Concurrent Model for Processes Sharing Resources},
627+ booktitle = {Proc. 3rd {IEEE} International Conf. on Soft. Eng. and Formal Methods},
628+ year = {2005},
629+ isbn = {0-7695-2435-4},
630+ pages = {231--239},
631+ doi = {http://dx.doi.org/10.1109/SEFM.2005.50},
632+ publisher = {{IEEE} Computer Society},
633+ address = {Washington, DC, USA},
634+ }
635+
636+@misc{GPCE2006,
637+ note = {Omitted to preserve anonymity, contact PC chair for details}
638+}
639+
640+@misc{IFL2006,
641+ note = {Omitted to preserve anonymity, contact PC chair for details}
642+}
643+
644+@misc{ivor-anon,
645+ note = {Omitted to preserve anonymity, contact PC chair for details}
646+}
647+
648+@inproceedings{HaskellIO,
649+ author = {Simon L. {Peyton Jones} and Philip Wadler},
650+ title = {Imperative functional programming},
651+ booktitle = {Proc. 20th {ACM} Symposium on Principles of programming languages},
652+ year = {1993},
653+ isbn = {0-89791-560-7},
654+ pages = {71--84},
655+ location = {Charleston, South Carolina, United States},
656+ doi = {http://doi.{ACM}.org/10.1145/158511.158524},
657+ publisher = {{ACM}},
658+ address = {New York, NY, USA},
659+ }
660+
661+@article{CorrectnessConstruction,
662+author = "P. Amey",
663+title = "{Correctness by Construction: Better can also be Cheaper}",
664+journal = "{CrossTalk: the Journal of Defense Software Engineering}",
665+month = mar,
666+year = 2002,
667+pages = "24--28"
668+}
669+
670+
671+
672+@INPROCEEDINGS{hj:popl03,
673+ AUTHOR = {M. Hofmann and S. Jost},
674+ TITLE = {Static Prediction of Heap Space Usage for First-Order Function
675+al Programs},
676+booktitle = "Proc. {POPL 2003 --- 2003 {ACM} Symp. on Principles of Programming La
677+nguages}",
678+ KEY = {HJ_POPL03},
679+ PAGES = {185--197},
680+ YEAR = {2003},
681+ ORGANIZATION = {{ACM}}
682+}
683+
684+
685+@article{kobayashi-lock,
686+ author = {Naoki Kobayashi},
687+ title = {A type system for lock-free processes},
688+ journal = {Inf. Comput.},
689+ volume = {177},
690+ number = {2},
691+ year = {2002},
692+ issn = {0890-5401},
693+ pages = {122--159},
694+ doi = {http://dx.doi.org/10.1016/S0890-5401(02)93171-8},
695+ publisher = {Academic Press, Inc.},
696+ address = {Duluth, MN, USA},
697+ }
698+
699+@techreport{linear-alias,
700+ title = {Linear types for aliased resources},
701+ author = {Chris Hawblitzel},
702+ year = {2005},
703+ institution = {Microsoft Research},
704+ number = {MSR-TR-2005-141}
705+}
706+
707+@article{kobayashi-esop,
708+ title = {Type-Based Analysis of Deadlock fora Concurrent Calculus with Interrupts},
709+ author = {Kohei Suenaga and Naoki Kobayashi},
710+ year = {2007},
711+ booktitle = {ESOP}
712+}
713+
714+@inproceedings{res-c,
715+ title = {A Path Sensitive Type System for Resource Usage Verification of C Like Languages},
716+ author = {Hyun-Goo Kang and Youil Kim and Taisook Han and Hwansoo Han},
717+ year = 2005,
718+ publisher = {Springer-Verlag},
719+ booktitle = {Programming Languages and Systems},
720+ pages = {264--280},
721+ series = {LNCS},
722+ volume = {3780}
723+}
724+
725+@miscs{lsr,
726+ title = {Lightweight static resources: Sexy types for embedded and systems programming},
727+ author = {Oleg Kiselyov and Chung-Chieh Shan},
728+ year = 2007,
729+ note = {Draft}
730+}
731+
732+@inproceedings{scoped-res,
733+ title = {Resource Usage Analysis Via Scoped Methods},
734+ author = {Gang Tan and Xinming Ou and David Walker},
735+ booktitle = {Foundations of Object-Oriented Languages},
736+ year = {2003}
737+}
738+
739+@article{igarashi-res,
740+ author = {Igarashi, Atsushi and Kobayashi, Naoki},
741+ title = {Resource usage analysis},
742+ journal = {ACM Trans. Program. Lang. Syst.},
743+ volume = {27},
744+ issue = {2},
745+ month = {March},
746+ year = {2005},
747+ issn = {0164-0925},
748+ pages = {264--313},
749+ numpages = {50},
750+ url = {http://doi.acm.org/10.1145/1057387.1057390},
751+ doi = {http://doi.acm.org/10.1145/1057387.1057390},
752+ acmid = {1057390},
753+ publisher = {ACM},
754+ address = {New York, NY, USA},
755+ keywords = {Resource usage, type inference},
756+}
757+
758+@phdthesis{monitoring,
759+ title = {Policy Enforcement via Program Monitoring},
760+ author = {Jarred Adam Ligatti},
761+ year = 2006,
762+ month = {May}
763+}
764+
765+@inproceedings{sec-policy,
766+ title = {A Type System for Expressive Security Policies},
767+ author = {David Walker},
768+ booktitle = {Twenty-Seventh {ACM} {SIGPLAN} Symposium on Principles of Programming Languages},
769+ pages = {254--267},
770+ year = 2000}
771+
772+@inproceedings{res-dfa,
773+ author = {K. Marriott and P.J. Stuckey and M. Sulzmann},
774+ title = {Resource Usage Verification},
775+ year = 2003,
776+ booktitle = {In Proc. of First Asian Symposium, APLAS 2003},
777+ pages = {212--229},
778+ publisher = {Springer-Verlag}
779+}
780+
781+@incollection{ hancock-interactive,
782+ author = "Peter Hancock and Anton Setzer",
783+ title = "Interactive Programs in Dependent Type Theory",
784+ booktitle = "Proc.\ of 14th Ann.\ Conf.\ of {EACSL}, {CSL}'00, Fischbau, Germany, 21--26 Aug 2000",
785+ volume = "1862",
786+ publisher = "Springer-Verlag",
787+ address = "Berlin",
788+ editor = "P. Clote and H. Schwichtenberg",
789+ pages = "317--331",
790+ year = "2000",
791+ url = "citeseer.ist.psu.edu/hancock00interactive.html" }
792+
793+@inproceedings{popeea-resources,
794+ author = {Corneliu Popeea and Wei-Ngan Chin},
795+ title = {A type system for resource protocol verification and its correctness proof},
796+ booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
797+ year = {2004},
798+ isbn = {1-58113-835-0},
799+ pages = {135--146},
800+ location = {Verona, Italy},
801+ doi = {http://doi.{ACM}.org/10.1145/1014007.1014021},
802+ publisher = {{ACM} Press},
803+ address = {New York, NY, USA},
804+ }
805+
806+@inproceedings{sheard-langfuture,
807+ author = {Tim Sheard},
808+ title = "Languages of the future",
809+ booktitle = "{ACM} Conference on Object Orientated Programming Systems, Languages and Applicatioons (OOPSLA'04)",
810+ year = "2004"
811+}
812+
813+@inproceedings{ivor,
814+ author = {Edwin Brady},
815+ title = {{Ivor}, a proof engine},
816+ year = {2007},
817+ publisher = {Springer-Verlag},
818+ series = {LNCS},
819+ booktitle = {Implementation and Application of Functional Languages 2006}
820+}
821+
822+@misc{coq-in-coq,
823+ author = {Bruno Barras and Benjamin Werner},
824+ year = 1997,
825+ title = {{Coq} in {Coq}}
826+}
827+
828+@article{hudak-edsl,
829+ author = {Paul Hudak},
830+ title = {Building Domain-Specific Embedded Languages},
831+ year = {1996},
832+ month = {December},
833+ journal = {{ACM} Computing Surveys},
834+ volume = {28A},
835+ number = {4}
836+}
837+
838+@inproceedings{concon,
839+ author = {Conor McBride and Healfdene Goguen and James McKinna},
840+ title = {Some Constructions On Constructors},
841+ year = 2005,
842+ booktitle = {TYPES 2004},
843+ publisher = {Springer},
844+ series = {LNCS},
845+ volume = {3839}
846+}
847+
848+@InProceedings{Hume-GPCE,
849+author = {K. Hammond and G.J. Michaelson},
850+title = {{Hume: a Domain-Specific Language for Real-Time Embedded Systems}},
851+booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'03)}},
852+publisher = {Springer-Verlag},
853+series = {Lecture Notes in Computer Science},
854+year = {2003},
855+}
856+
857+@inproceedings{lcf-milner,
858+ author = {Robin Milner},
859+ title = {{LCF}: A Way of Doing Proofs with a Machine},
860+ booktitle = {Mathematical Foundations of Computer Science 1978},
861+ pages = {146-159},
862+ year = 1979,
863+ series = {LNCS},
864+ volume = {64}
865+}
866+
867+
868+@inproceedings{epireloaded,
869+ title = {Epigram Reloaded: A Standalone Typechecker for {ETT}},
870+ author = {James Chapman and Thorsten Altenkirch and Conor McBride},
871+ year = 2006,
872+ booktitle = {Trends in Functional Programming 2005},
873+ note = {To appear}
874+}
875+
876+@TECHREPORT{why-tool,
877+ AUTHOR = {J.-C. Filli\^atre},
878+ TITLE = {{Why: a multi-language multi-prover verification tool}},
879+ INSTITUTION = {{LRI, Universit\'e Paris Sud}},
880+ TYPE = {{Research Report}},
881+ NUMBER = {1366},
882+ MONTH = {March},
883+ YEAR = 2003,
884+ URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
885+}
886+
887+@misc{ large-extraction,
888+ author = "Lu\'iz Cruz-Filipe and Bas Spitters",
889+ title = "Program Extraction from Large Proof Developments",
890+ year = 2003,
891+ url = "citeseer.ist.psu.edu/cruz-filipe03program.html" }
892+
893+@inproceedings{ fta,
894+ author = "Herman Geuvers and Freek Wiedijk and Jan Zwanenburg",
895+ title = "A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals",
896+ booktitle = "{TYPES 2000}",
897+ pages = "96--111",
898+ year = "2000",
899+ url = "citeseer.ist.psu.edu/geuvers01constructive.html" }
900+
901+@article{mckinna-expr,
902+ title = {A type-correct, stack-safe, provably correct, expression compiler in {Epigram}},
903+ author = {James McKinna and Joel Wright},
904+ year = 2007,
905+ journal = {Journal of Functional Programming},
906+ note = {To appear}
907+}
908+
909+@article{pugh-omega,
910+ title = "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis",
911+ author = "William Pugh",
912+ journal = "Communication of the {ACM}",
913+ year = 1992,
914+ pages = {102--114}
915+}
916+
917+@misc{four-colour,
918+ author = "Georges Gonthier",
919+ title = "A computer-checked proof of the {Four Colour Theorem}",
920+ year = 2005,
921+ howpublished = {\url{http://research.microsoft.com/~gonthier/4colproof.pdf}}}
922+
923+@inproceedings{sparkle,
924+ author = "Maarten {de Mol} and Marko {van Eekelen} and Rinus Plasmeijer",
925+ title = "Theorem Proving for Functional Programmers",
926+ url = "citeseer.ist.psu.edu/654423.html",
927+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2002)},
928+ publisher = {Springer},
929+ series = {LNCS},
930+ volume = {2312},
931+ year = 2002
932+ }
933+
934+@misc{agda,
935+ title = {Agda},
936+ author = {Catarina Coquand},
937+ howpublished= {\url{http://agda.sourceforge.net/}},
938+ year = 2005
939+}
940+
941+@misc{cover,
942+ title = {Cover Translator},
943+ howpublished = {\url{http://coverproject.org/CoverTranslator/}}
944+}
945+
946+@misc{parsec,
947+ title = {Parsec, a fast combinator parser},
948+ author = {Daan Leijen},
949+ year = {2001},
950+ howpublished = {\url{http://www.cs.uu.nl/~daan/parsec.html}}
951+}
952+
953+@inproceedings{dtpmsp-gpce,
954+ author = {Edwin Brady and Kevin Hammond},
955+ title = {A Verified Staged Interpreter is a Verified Compiler},
956+ booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'06)}},
957+ year = 2006
958+}
959+
960+@misc{haddock,
961+ title = {Haddock: A {Haskell} Documentation Tool},
962+ howpublished = {\url{http://www.haskell.org/haddock/}}
963+}
964+
965+@inproceedings{offshoring,
966+ title = {Implicitly Heterogeneous Multi-Stage Programming},
967+ author = {Jason Eckhardt and Roumen Kaibachev and Emir Pa\v{s}al\'{i}c and Kedar Swadi and Walid Taha},
968+ booktitle = {Proc. 2005 Conf. on Generative Programming and Component Engineering (GPCE 2005)},
969+ publisher = {Springer},
970+ series = {LNCS},
971+ volume = {3676},
972+ year = 2005
973+}
974+
975+@misc{alti-partial,
976+ title = {Stop thinking about bottoms when writing programs},
977+ author = {Thorsten Altenkirch},
978+ year = 2006,
979+ note = {Talk at BCTCS 2006}
980+}
981+
982+@misc{tarmo-partial,
983+ title = {Partiality is an Effect},
984+ author = {Tarmo Uustalu},
985+ year = 2004,
986+ note = {Talk at Dagstuhl workshop on Dependently Typed Progamming}
987+}
988+
989+@inproceedings{McKinnaPOPL06,
990+ author = {James McKinna},
991+ title = {Why dependent types matter},
992+ booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2006)},
993+ year = {2006},
994+ issn = {0362-1340},
995+ pages = {1--1},
996+ doi = {http://doi.{ACM}.org/10.1145/1111320.1111038},
997+}
998+
999+
1000+@inproceedings{leroy-compiler,
1001+ title = {Formal Certification of a Compiler Back-end},
1002+ author = {Xavier Leroy},
1003+ year = 2006,
1004+ booktitle = {Principles of Programming Languages 2006},
1005+ pages = {42--54},
1006+ publisher = {{ACM} Press}
1007+}
1008+
1009+@inproceedings{hutton-exceptions,
1010+ title = {Compiling Exceptions Correctly},
1011+ year = 2004,
1012+ author = {Graham Hutton and Joel Wright},
1013+ booktitle = {Mathematics of Program Construction},
1014+ publisher = {Springer},
1015+ series = {LNCS},
1016+ volume = {3125}
1017+}
1018+
1019+@inproceedings{tagless-staged,
1020+ title = {Tagless Staged Interpreters for Typed Languages},
1021+ year = {2002},
1022+ booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},
1023+ author = {Emir Pa\v{s}al\'{i}c and Walid Taha and Tim Sheard},
1024+ publisher = {{ACM}}
1025+}
1026+
1027+@inproceedings{env-classifiers,
1028+ title = {Environment Classifiers},
1029+ year = 2003,
1030+ author = {Walid Taha},
1031+ booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2003)},
1032+ pages = {26--37},
1033+}
1034+
1035+@inproceedings{dsl-msp,
1036+ title = {{DSL} Implementation in {MetaOCaml}, {Template Haskell}, {and C++}},
1037+ booktitle = {Domain Specific Program Genearation 2004},
1038+ author = {Krzysztof Czarnecki and John O'Donnell and J\"{o}rg Striegnitz and Walid Taha},
1039+ publisher = {Springer},
1040+ series = {LNCS},
1041+ volume = {3016},
1042+ year = 2004
1043+}
1044+
1045+@misc{ gadt-extk,
1046+ author = {Tim Sheard and James Hook and Nathan Linger},
1047+ title = {{GADTs} + Extensible Kinds = Dependent Programming},
1048+ year = 2005,
1049+ misc = {Submitted to {ICFP} '05}
1050+}
1051+
1052+@INPROCEEDINGS{dt-framework,
1053+ TITLE = {A Dependently Typed Framework for Static Analysis of Program Execution Costs},
1054+ YEAR = {2006},
1055+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
1056+ AUTHOR = {Edwin Brady and Kevin Hammond},
1057+ VOLUME = {4015},
1058+ SERIES = {LNCS},
1059+ PAGES = {74--90},
1060+ PUBLISHER = {Springer}
1061+}
1062+
1063+@INPROCEEDINGS{step-counting,
1064+ TITLE = {Accurate Step Counting},
1065+ YEAR = {2006},
1066+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
1067+ AUTHOR = {Catherine Hope and Graham Hutton},
1068+ PUBLISHER = {Springer}
1069+}
1070+
1071+@misc{multi-taha,
1072+ author = {Walid Taha},
1073+ title = {{A Gentle Introduction to Multi-stage Programming}},
1074+ year = {2003},
1075+ note = {Available from \url{http://www.cs.rice.edu/~taha}},
1076+ notnote = {Available from \url{http://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf}}
1077+}
1078+
1079+@misc{mckinnabrady-phase,
1080+ title = {Phase Distinctions in the Compilation of {Epigram}},
1081+ year = 2005,
1082+ author = {James McKinna and Edwin Brady},
1083+ note = {Draft}
1084+}
1085+
1086+@phdthesis{ brady-thesis,
1087+ author = {Edwin Brady},
1088+ title = {Practical Implementation of a Dependently Typed Functional Programming Language},
1089+ year = 2005,
1090+ school = {University of Durham}
1091+}
1092+
1093+@phdthesis{ taha-thesis,
1094+ author = {Walid Taha},
1095+ title = {Multi-stage Programming: Its Theory and Applications},
1096+ year = 1999,
1097+ school = {Oregon Graduate Inst. of Science and Technology}
1098+}
1099+
1100+@phdthesis{ pasalic-thesis,
1101+ author = {Emir Pa\v{s}al\'{i}c},
1102+ title = {The Role of Type-Equality in Meta-programming},
1103+ year = 2004,
1104+ school = {OGI School of Science and Engineering}
1105+}
1106+
1107+@misc{ydtm,
1108+ author = {Thorsten Altenkirch and Conor McBride and James McKinna},
1109+ title = {Why Dependent Types Matter},
1110+ note = {Draft},
1111+ year = 2005}
1112+
1113+
1114+@inproceedings { wadler-listless,
1115+ author = {Philip Wadler},
1116+ title = {Listlessness is better than laziness: {Lazy} evaluation and garbage collection at compile-time},
1117+ booktitle = {Proceedings of the 1984 {ACM} Symposium on LISP and functional programming},
1118+ year = 1984,
1119+ pages = {45--52}
1120+}
1121+
1122+@techreport { gofer-impl,
1123+ author = {Mark P. Jones},
1124+ title = {The implementation of the Gofer functional programming system},
1125+ month = {May},
1126+ year = {1994},
1127+ number = {YALEU/DCS/RR-1030},
1128+ institution = {Yale University}
1129+}
1130+
1131+@techreport { pm-opt1,
1132+ author = {Kevin Scott and Norman Ramsey},
1133+ title = {When do match-compilation heuristics matter?},
1134+ month = {May},
1135+ year = {2000},
1136+ number = {CS-2000-13},
1137+ institution = {Department of Computer Science, University of Virginia}
1138+}
1139+
1140+@inproceedings{ pm-opt2,
1141+ author = "Fabrice Le Fessant and Luc Maranget",
1142+ title = "Optimizing Pattern Matching",
1143+ booktitle = "International Conference on Functional Programming",
1144+ pages = "26-37",
1145+ year = "2001",
1146+ url = "citeseer.ist.psu.edu/lefessant01optimizing.html" }
1147+
1148+@incollection{con-engine,
1149+ author = {G\'{e}rard Huet},
1150+ title = {The constructive engine},
1151+ booktitle = {A Perspective in Theoreticak Computer Science},
1152+ publisher = {World Scientific Publishing},
1153+ year = {1989},
1154+ editor = {R. Narasimhan},
1155+ note = {Commemorative Volume for Gift Siromoney},
1156+ pages = {38--69}
1157+}
1158+
1159+@inproceedings{gadts,
1160+ title = {Simple unification-based type inference for {GADTs}},
1161+ author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
1162+ year = {2006},
1163+ booktitle = {Proc. 2006 International Conf. on Functional Programming ({ICFP} 2006)}
1164+}
1165+
1166+@misc{wobbly,
1167+ author = {Simon {Peyton Jones} and Geoffrey Washburn and Stephanie Weirich},
1168+ title = {Wobbly types: type inference for generalised algebraic data types},
1169+ year = {2004},
1170+ note = {Submitted to POPL 2005}
1171+}
1172+
1173+@misc{epigram-afp,
1174+ author = {Conor McBride},
1175+ title = {Epigram: Practical Programming with Dependent Types},
1176+ year = {2004},
1177+ howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}
1178+}
1179+
1180+@book{ml85,
1181+ author = {Per Martin-L\"{o}f},
1182+ title = "Intuitionistic Type Theory",
1183+ year = "1985",
1184+ publisher = "Bibliopolis"
1185+}
1186+
1187+@article{modular-fulllazy,
1188+ title = {A Modular Fully Lazy Lambda Lifter in {Haskell}},
1189+ author = {Simon {Peyton Jones} and David Lester},
1190+ year = {1991},
1191+ month = {May},
1192+ journal = {Software Practice and Experience},
1193+ volume = {21},
1194+ number = {5},
1195+ pages = {479--506}
1196+}
1197+
1198+@article{ghani-jay95,
1199+ author = {Barry Jay and Neil Ghani},
1200+ title = {The Virtues of Eta-Expansion},
1201+ journal = {Journal of Functional Programming},
1202+ year = {1995},
1203+ volume = {5},
1204+ number = {2},
1205+ pages = {135-154},
1206+}
1207+
1208+@misc{nkpat,
1209+ author = {Lennart Augustsson},
1210+ title = {n+k patterns},
1211+ year = {1993},
1212+ howpublished = {Message to the haskell mailing list, Mon, 17 May 93}
1213+}
1214+
1215+@article{ danvy98functional,
1216+ author = "Olivier Danvy",
1217+ title = "Functional Unparsing",
1218+ journal = "Journal of Functional Programming",
1219+ volume = "8",
1220+ number = "6",
1221+ pages = "621-625",
1222+ year = "1998",
1223+ url = "citeseer.ist.psu.edu/danvy98functional.html" }
1224+
1225+@inproceedings{SeveriPoll94,
1226+ author = {Paula Severi and Erik Poll},
1227+ booktitle = {Logical Foundations of Computing Science, LFCS'94},
1228+ editor = {A. Nerode and Yu. V. Matiyasevich},
1229+ number = {813},
1230+ pages = {316--328},
1231+ publisher = {Springer},
1232+ series = {LNCS},
1233+ title = {{P}ure {T}ype {S}ystems with {D}efinitions},
1234+ year = {1994}
1235+}
1236+
1237+@inproceedings{coinductive,
1238+ title = {An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol},
1239+ booktitle = {Proceedings of the 1995 Workshop on Types for Proofs and Programs},
1240+ series = {LNCS},
1241+ year = {1995},
1242+ volume = {1158},
1243+ pages = {135-152},
1244+ publisher = {Springer-Verlag},
1245+ author = {Eduardo Gim\'{e}nez}
1246+}
1247+
1248+@book{erlang,
1249+ author = "Joe Armstrong and Robert Virding and Claes Wikstr{\"o}m and Mike Williams",
1250+ title = "Concurrent Programming in Erlang",
1251+ edition = "Second",
1252+ publisher = "Prentice-Hall",
1253+ year = "1996",
1254+ url = "citeseer.ist.psu.edu/armstrong93concurrent.html"
1255+}
1256+
1257+@PhdThesis{alti:phd93,
1258+ author = "Thorsten Altenkirch",
1259+ title = "Constructions, Inductive Types and Strong Normalization",
1260+ school = "University of Edinburgh",
1261+ year = "1993",
1262+ month = "November",
1263+}
1264+
1265+@inproceedings{coq-modules,
1266+ author = "Jacek Chrzaszcz",
1267+ title = "Modules in {Coq} Are and Will Be Correct",
1268+ year = {2004},
1269+ booktitle = {Types for Proofs and Programs 2003},
1270+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
1271+ publisher = {Springer},
1272+ volume = {3085}
1273+}
1274+
1275+@inproceedings{comp-polymorphism,
1276+ author = "Robert Harper and Greg Morrisett",
1277+ title = "Compiling Polymorphism Using Intensional Type Analysis",
1278+ year = "1995",
1279+ booktitle = "Proceedings of the 22nd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programming languages",
1280+ pages = "130 -- 141"
1281+}
1282+
1283+@misc{runtime-loader,
1284+ author = "Andre Pang",
1285+ title = "{GHC} Runtime Loading",
1286+ year = "2004",
1287+ howpublished = {Available from \verb+http://www.algorithm.com.au/wiki/hacking/haskell.ghc_runtime_loading+}
1288+}
1289+
1290+@article{mccarthy-lisp,
1291+ author = "John McCarthy",
1292+ title = "Recursive Functions of Symbolic Expressions and Their Computation By Machine",
1293+ year = "1960",
1294+ journal = "Communications of the {ACM}",
1295+ volume = "3",
1296+ number = "4",
1297+ pages = "184--195"
1298+}
1299+
1300+@book{stl,
1301+ author = " David R. Musser and Atul Saini and Gillmer J. Derge",
1302+ title= "The {STL} Tutorial and Reference Guide: {C++} Programming with the Standard Template Library",
1303+ year = "2001",
1304+ publisher = "Addison Wesley"
1305+}
1306+
1307+@misc{ phase-distinction,
1308+ author = "Luca Cardelli",
1309+ title = "Phase Distinctions in Type Theory",
1310+ howpublished = "Manuscript",
1311+ year = "1988",
1312+ url = "citeseer.ist.psu.edu/cardelli88phase.html" }
1313+
1314+@book {pierce-types,
1315+ author = "Benjamin C. Pierce",
1316+ title = "Type and Programming Languages",
1317+ year = "2002",
1318+ publisher = "MIT Press"
1319+}
1320+
1321+@article{ coqcc,
1322+ Author = "Thierry Coquand and G\'{e}rard Huet",
1323+ title = "The calculus of constructions",
1324+ year = "1988",
1325+ journal = "Information and Computation",
1326+ volume = "76",
1327+ pages = "95--120"
1328+}
1329+
1330+@article{ miller91jlc,
1331+ Author = "Dale Miller",
1332+ Title = "A Logic Programming Language with Lambda-Abstraction,
1333+ Function Variables, and Simple Unification",
1334+ Journal = "Journal of Logic and Computation",
1335+ Volume = "1",
1336+ Number = "4",
1337+ Pages = "497-536",
1338+ Year = "1991",
1339+ URL = "citeseer.ist.psu.edu/miller91logic.html",
1340+ URL = "file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z" }
1341+
1342+@article{miller-unity,
1343+ author = "Dale Miller",
1344+ title = "Unification Under a Mixed Prefix",
1345+ journal = "Journal of Symbolic Computation",
1346+ volume = "14",
1347+ pages = "321--358",
1348+ year = 1992
1349+}
1350+
1351+@inproceedings{ cynthia,
1352+ author = "Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe",
1353+ title = "An {ML} Editor Based on Proofs-As-Programs",
1354+ booktitle = "Automated Software Engineering",
1355+ pages = "166-173",
1356+ year = "1999",
1357+ url = "citeseer.ist.psu.edu/whittle99ml.html" }
1358+
1359+
1360+@misc{ewd340,
1361+ title={The Humble Programmer},
1362+ author={Edsger Dijkstra},
1363+ year={1972},
1364+ note={Turing Award Lecture, EWD 340}
1365+}
1366+
1367+@misc{fortran,
1368+ title={Specifications for the {IBM} Mathematical FORmula TRANslating System, {FORTRAN}},
1369+ author={{IBM Applied Science Division}},
1370+ key={IBM},
1371+ year={1954},
1372+ month={November}
1373+}
1374+
1375+@inproceedings{quickcheck,
1376+ title = {{QuickCheck}: A Lightweight Tool For Random Testing Of {Haskell} Programs},
1377+ author = {Koen Claessen and John Hughes},
1378+ year = {2000},
1379+ booktitle = {International Conference on Functional Programming}
1380+}
1381+
1382+@inproceedings{currylam,
1383+ title = {Functionality in Combinatory Logic},
1384+ author = {Haskell Curry},
1385+ year = {1934},
1386+ booktitle = {Proc. Nat. Acad. Sci, USA},
1387+ volume = {20},
1388+ pages = {584--590}
1389+}
1390+
1391+@article{churchsimplelam1,
1392+ title = {A set of postulates for the foundation of logic},
1393+ author = {Alonzo Church},
1394+ year = {1932},
1395+ journal = {Annals of Mathematics},
1396+ volume = {2},
1397+ number = {33},
1398+ pages = {346--366}
1399+}
1400+
1401+@article{churchsimplelam2,
1402+ title = {A set of postulates for the foundation of logic},
1403+ author = {Alonzo Church},
1404+ year = {1933},
1405+ journal = {Annals of Mathematics},
1406+ volume = {2},
1407+ number = {34},
1408+ pages = {839--864}
1409+}
1410+
1411+@article{churchlam,
1412+ title = {A Formulation of the Simple Theory of Types},
1413+ author = {Alonzo Church},
1414+ year = {1940},
1415+ journal = {Journal of Symbolic Logic},
1416+ volume = {5},
1417+ pages = {56--58}
1418+}
1419+
1420+@book{mitchell,
1421+ title = {Concepts in Programming Languages},
1422+ author = {John C. Mitchell},
1423+ year = {2003},
1424+ publisher = {Cambridge University Press}
1425+}
1426+
1427+@inproceedings{harrison-hol99,
1428+ title = {A Machine-Checked Theory of Floating Point Arithmetic},
1429+ year = {1999},
1430+ booktitle = {Theorem Proving in Higher Order Logics: 12th International Conference, TP},
1431+ pages = {113--130},
1432+ author = {John Harrison},
1433+ crossref = {hol99}
1434+}
1435+
1436+@inproceedings{c--,
1437+ title = {C--: A portable assembly language},
1438+ year = {1997},
1439+ booktitle = {Workshop on Implementing Functional Languages, St Andrews},
1440+ author = {Simon {Peyton Jones} and Thomas Nordin and Dino Oliva},
1441+ crossref = {func-imp97}
1442+}
1443+
1444+@proceedings{func-imp97,
1445+ title = {Workshop on Implementing Functional Languages, St Andrews},
1446+ year = {1997},
1447+ editor = {C Clack},
1448+ publisher = {Springer-Verlag}
1449+}
1450+
1451+@proceedings{hol99,
1452+ volume = {1690},
1453+ title = {Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99},
1454+ year = {1999},
1455+ editor = {Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and Christine Paul},
1456+ publisher = {Springer-Verlag},
1457+ address = {Nice, France},
1458+ series = {LNCS}
1459+}
1460+
1461+@book{mathlogic,
1462+ title = {Mathematical Logic and Programming Languages},
1463+ year = {1985},
1464+ editor = {C.A.R. Hoare and J.C. Shepherdson},
1465+ publisher = {Prentice-Hall}
1466+}
1467+
1468+@book{automath,
1469+ title = {Selected Papers on Automath},
1470+ year = {1994},
1471+ editor = {S. Abramsky and J. Barwise and K. Fine and H.J. Keisler and A.S. Troelstr},
1472+ publisher = {North-Holland}
1473+}
1474+
1475+@misc{gimps,
1476+ howpublished = {http://www.mersenne.org/prime.htm},
1477+ title = {Great Internet Mersenne Prime Search}
1478+}
1479+
1480+@misc{haskell-report,
1481+ title = {Haskell 98 Language and Libraries --- The Revised Report},
1482+ year = {2002},
1483+ month = {December},
1484+ author = {Simon {Peyton Jones} and others},
1485+ howpublished = {Available from \verb+http://www.haskell.org/+}
1486+}
1487+
1488+@inproceedings{cayenne-{ICFP},
1489+ author = "Lennart Augustsson",
1490+ title = "Cayenne - a Language with Dependent Types",
1491+ booktitle = "Proc. 1998 International Conf. on Functional Programming ({ICFP} '98)",
1492+ pages = "239--250",
1493+ year = "1998",
1494+ url = "citeseer.nj.nec.com/augustsson98cayenne.html"
1495+}
1496+
1497+
1498+@misc{equality-cayenne,
1499+ howpublished = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
1500+ title = {Equality Proofs in Cayenne},
1501+ year = {1999},
1502+ author = {Lennart Augustsson}
1503+}
1504+
1505+@misc{interp-cayenne,
1506+ title = {An exercise in dependent types: A well-typed interpreter},
1507+ year = {1999},
1508+ author = {Lennart Augustsson and Magnus Carlsson}
1509+}
1510+
1511+@inproceedings{balaa00fixpoint,
1512+ title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},
1513+ year = {2000},
1514+ booktitle = {Theorem Proving in Higher Order Logics},
1515+ pages = {1-16},
1516+ author = {Antonia Balaa and Yves Bertot}
1517+}
1518+
1519+@inproceedings{isabelle-maple,
1520+ title = {Theorems and algorithms: An interface between Isabelle and Maple},
1521+ year = {1995},
1522+ booktitle = {International Symposium on Symbolic and Algebraic Computation},
1523+ author = {Ballarin, C. and Homann, K., and Calmet, J.}
1524+}
1525+
1526+@book{barendregt-num,
1527+ title = {The Lambda Calculus, Its Syntax and Semantics},
1528+ year = {1984},
1529+ publisher = {North-Holland},
1530+ author = {Henk Barendregt}
1531+}
1532+
1533+@book{beiler,
1534+ title = {Recreations in the Theory of Numbers},
1535+ year = {1964},
1536+ publisher = {Dover},
1537+ author = {Albert H. Beiler}
1538+}
1539+
1540+@article{multidigit,
1541+ journal = {Advances in Applied Mathematics},
1542+ title = {Multidigit Multiplication for Mathematicians},
1543+ year = {1998},
1544+ author = {Daniel J. Bernstein}
1545+}
1546+
1547+@article{buhler-fox,
1548+ journal = {{ACM} Crossroads 2.1.},
1549+ month = {September},
1550+ title = {The Fox project: A language-structured approach to networking software.},
1551+ year = {1995},
1552+ author = {Buhler, J.},
1553+ note = {Available at http://www.{ACM}.org/crossroads/xrds2-1/foxnet.html}
1554+}
1555+
1556+@techreport{burstall91,
1557+ title = {Computer Assisted Proof for Mathematics: an Introduction Using the \textsc{Lego} Proof System},
1558+ year = {1991},
1559+ institution = {University of Edinburgh},
1560+ author = {Rod Burstall}
1561+}
1562+
1563+@article{plastic,
1564+ title = {An Implementation of {LF} with Coercive Subtyping and Universes},
1565+ author = {Paul Callaghan and Zhaohui Luo},
1566+ journal = {Journal of Automated Reasoning},
1567+ volume = {27},
1568+ number = {1},
1569+ pages = {3--27},
1570+ year = {2001}
1571+}
1572+
1573+@article{coercive,
1574+ title = {Coercive subtyping},
1575+ author = {Zhaohui Luo},
1576+ journal = {J. Logic Comput.},
1577+ volume = {9},
1578+ number = {1},
1579+ year = {1991},
1580+ pages = {105--130}
1581+}
1582+
1583+@inproceedings{calmet-homann,
1584+ title = {Classification of communication and cooperation mechanisms for logical and symbolic computation systems},
1585+ year = {1996},
1586+ booktitle = {Proceedings of the First International Workshop 'Frontiers of Combining S},
1587+ pages = {133-146},
1588+ publisher = {Kluwer},
1589+ author = {J. Calmet and K. Homann}
1590+}
1591+
1592+@techreport{comm-proofs,
1593+ title = {On Communicating Proofs in Interactive Mathematical Documents},
1594+ year = {2000},
1595+ institution = {Eindhoven University of Technology},
1596+ author = {Olga Caprotti and Martijn Oostdijk}
1597+}
1598+
1599+@article{prime2999,
1600+ title = {How to formally and efficiently prove Prime(2999)},
1601+ year = {2001},
1602+ author = {Olga Caprotti and Martijn Oostdijk},
1603+ journal = {Symbolic Computation and Automated Reasoning},
1604+ pages = {114--125}
1605+}
1606+
1607+@book{church-num,
1608+ title = {The Calculi of Lambda-Conversion},
1609+ year = {1941},
1610+ publisher = {Princeton University Press},
1611+ author = {Alonzo Church}
1612+}
1613+
1614+@book{nuprl86,
1615+ title = {Implementing Mathematics with the NuPrl Proof Development System},
1616+ year = {1986},
1617+ publisher = {Prentice-Hall},
1618+ address = {NJ},
1619+ author = {Constable, Robert L. and others}
1620+}
1621+
1622+@book{conway,
1623+ title = {On Numbers and Games},
1624+ year = {1976},
1625+ publisher = {Academic Press},
1626+ author = {J.H. Conway}
1627+}
1628+
1629+@misc{coq-manual,
1630+ howpublished = {\verb+http://coq.inria.fr/+},
1631+ title = {The {Coq} Proof Assistant --- Reference Manual},
1632+ year = {2009},
1633+ author = {{Coq Development Team}}
1634+}
1635+
1636+@misc{tt-prog,
1637+ month = {June},
1638+ title = {Type Theory and Programming},
1639+ year = {1994},
1640+ author = {Thierry Coquand and Bengt Nordstr\"{o}m and Jan M. Smith and Bj\"{o}rn von Sydow}
1641+}
1642+
1643+@book{func-appr,
1644+ title = {The Functional Approach to Programming},
1645+ year = {1998},
1646+ publisher = {Cambridge University Press},
1647+ author = {Guy Cousineau and Michel Mauny}
1648+}
1649+
1650+@misc{ibmspec,
1651+ howpublished = {http://www2.hursley.ibm.com/decimal/},
1652+ month = {January},
1653+ title = {Standard Decimal Arithmetic Specification},
1654+ year = {2001},
1655+ author = {Mike Cowlishaw},
1656+ note = {\copyright IBM Corporation 2001}
1657+}
1658+
1659+@book{dummett,
1660+ title = {Elements of Intuitionism},
1661+ year = {2000},
1662+ edition = {2nd},
1663+ publisher = {Oxford: Clarendon},
1664+ author = {Michael A.E. Dummet}
1665+}
1666+
1667+@article{dybjer94,
1668+ title = {Inductive Families},
1669+ year = {1994},
1670+ author = {Peter Dybjer},
1671+ journal = {Formal Aspects Of Computing},
1672+ volume = {6},
1673+ pages = {440--465}
1674+}
1675+
1676+@misc{octave,
1677+ howpublished = {http://www.octave.org/},
1678+ month = {February},
1679+ title = {GNU Octave -- A high-level interactive language for numerical computations},
1680+ year = {1997},
1681+ author = {John W. Eaton}
1682+}
1683+
1684+@book{comp-methods,
1685+ title = {Computing methods for scientists and engineers},
1686+ year = {1968},
1687+ publisher = {Oxford : Clarendon Press},
1688+ author = {L. Fox and D.F. Mayers}
1689+}
1690+
1691+@misc{guile,
1692+ howpublished = {http://www.gnu.org/software/guile/guile.html},
1693+ title = {Guile -- Project GNU's extension language},
1694+ year = {2001},
1695+ author = {{Free Software Foundation}}
1696+}
1697+
1698+@article{need-dep,
1699+ journal = {Journal of Functional Programming},
1700+ number = {4},
1701+ volume = {10},
1702+ title = {Do we need dependent types?},
1703+ year = {2000},
1704+ pages = {409-415},
1705+ author = {Daniel Fridlender and Mia Indrika}
1706+}
1707+
1708+@book{primes-programming,
1709+ title = {Primes and Programming -- An Introduction to Number Theory with Computing},
1710+ year = {1993},
1711+ publisher = {Cambridge University Press},
1712+ author = {Peter Giblin}
1713+}
1714+
1715+@misc{rec-coq,
1716+ month = {May},
1717+ title = {A Tutorial on Recursive Types in \textsc{Coq}},
1718+ year = {1998},
1719+ author = {Eduardo Gim\'{e}nez}
1720+}
1721+
1722+@article{goldberg91,
1723+ journal = {{ACM} Computing Surveys},
1724+ number = {1},
1725+ volume = {23},
1726+ title = {What every computer scientist should know about floating point arithmetic},
1727+ year = {1991},
1728+ pages = {5-48},
1729+ author = {D. Goldberg}
1730+}
1731+
1732+@article{binary-lambda,
1733+ journal = {Journal of Functional Programming},
1734+ number = {6},
1735+ volume = {10},
1736+ title = {An adequate and efficient left associated binary numeral system in the $\lambda$-calculus},
1737+ year = {2000},
1738+ author = {Mayer Goldberg}
1739+}
1740+
1741+@book{hol,
1742+ title = {Introduction to HOL},
1743+ year = {1993},
1744+ publisher = {Cambridge University Press},
1745+ author = {M. Gordon and T. Melham}
1746+}
1747+
1748+@misc{gmp,
1749+ howpublished = {Available from \verb+http://www.swox.com/gmp/manual/+},
1750+ title = {The {GNU Multiple Precision} Arithmetic Library 4.1.3 --- Manual},
1751+ year = {2004},
1752+ author = {Torbj\"{o}rn Granlund and others}
1753+}
1754+
1755+@article{harrison-fmsd94,
1756+ journal = {Formal Methods in System Design},
1757+ volume = {5},
1758+ title = {Constructing the Real Numbers in {HOL}},
1759+ year = {1994},
1760+ pages = {35--59},
1761+ author = {John Harrison}
1762+}
1763+
1764+@book{harrison-thesis,
1765+ title = {Theorem Proving with the Real Numbers},
1766+ year = {1998},
1767+ publisher = {Springer-Verlag},
1768+ author = {John Harrison}
1769+}
1770+
1771+@techreport{hol-maple,
1772+ title = {Reasing about the Reals: the marriage of HOL and Maple},
1773+ year = {1993},
1774+ institution = {University of Cambridge Computer Laboratory},
1775+ author = {John Harrison and Laurent Th\'{e}ry}
1776+}
1777+
1778+@misc{coq-tutorial,
1779+ howpublished = {http://pauillac.inria.fr/coq},
1780+ title = {The \textsc{Coq} Proof Assistant - A Tutorial},
1781+ author = {G\'{e}rard Huet and Gilles Kahn and Christine Paulin-Mohring}
1782+}
1783+
1784+@misc{restr-haskell,
1785+ howpublished = {http://citeseer.nj.nec.com/253599.html},
1786+ month = {September},
1787+ title = {Restricted Data Types in Haskell},
1788+ year = {1999},
1789+ author = {John Hughes}
1790+}
1791+
1792+@misc{javadec,
1793+ howpublished = {http://www2.hursley.ibm.com/decimalj/decimald.html},
1794+ month = {September},
1795+ title = {Decimal Arithmetic for Java -- a Proposal},
1796+ year = {2000},
1797+ author = {{IBM Corporation}}
1798+}
1799+
1800+@misc{ieee754,
1801+ title = {{IEEE} Standard for Binary Floating Point Arithmetic},
1802+ year = {1985},
1803+ author = {{IEEE Standard 754}}
1804+}
1805+
1806+@misc{ieee854,
1807+ title = {IEEE Standard for Radix-Independent Floating-Point Arithmetic},
1808+ year = {1987},
1809+ author = {{IEEE Standard 854}}
1810+}
1811+
1812+@inproceedings{jon91,
1813+ title = {Completing the Rational and Metric Spaces in \textsc{Lego}},
1814+ year = {1991},
1815+ booktitle = {Proceedings of the Second Workshop on Logical Frameworks},
1816+ author = {Claire Jones}
1817+}
1818+
1819+@misc{ typinghaskell,
1820+ author = "Mark Jones",
1821+ title = "Typing {Haskell} in {Haskell}",
1822+ howpublished = "In Haskell Workshop, September 1999.",
1823+ year = "1999",
1824+ url = "citeseer.ist.psu.edu/article/jones99typing.html" }
1825+
1826+@article{karatsuba,
1827+ journal = {Soviet Physics-Doklady},
1828+ volume = {7},
1829+ title = {Multiplication of multidigit numbers by automata},
1830+ year = {1963},
1831+ pages = {595--596},
1832+ author = {A. Karatsuba and Y. Ofman}
1833+}
1834+
1835+@book{knuth2,
1836+ volume = {2},
1837+ title = {The Art of Computer Programming - Seminumerical Algorithms},
1838+ year = {1969},
1839+ publisher = {Addison Wesley},
1840+ author = {Donald E. Knuth}
1841+}
1842+
1843+@article{next700,
1844+ journal = {Communications of the {ACM}},
1845+ number = {3},
1846+ month = {March},
1847+ volume = {9},
1848+ title = {The next 700 programming languages},
1849+ year = {1966},
1850+ author = {P.J. Landin}
1851+}
1852+
1853+@techreport{luo-spec,
1854+ month = {January},
1855+ title = {Program Specification and Data Refinement in Type Theory},
1856+ year = {1993},
1857+ institution = {Department of Computer Science, University of Edinburgh},
1858+ author = {Zhaohui Luo}
1859+}
1860+
1861+@phdthesis{luo90,
1862+ school = {University of Edinburgh},
1863+ title = {An Extended Calculus Of Constructions},
1864+ year = {1990},
1865+ author = {Zhaohui Luo}
1866+}
1867+
1868+@techreport{lego-manual,
1869+ title = {\textsc{Lego} Proof Development System: User's Manual},
1870+ year = {1992},
1871+ institution = {Department of Computer Science, University of Edinburgh},
1872+ author = {Zhaohui Luo and Robert Pollack}
1873+}
1874+
1875+@inproceedings{alf,
1876+ title = {The {ALF} proof editor and its proof engine},
1877+ year = {1994},
1878+ booktitle = {Formal Proceeding of the 1993 Workshop on Types for Proofs and Programs},
1879+ author = {Lena Magnusson and Bengt N\"{o}rdstrom}
1880+}
1881+
1882+@misc{happy,
1883+ howpublished = {http://www.haskell.org/happy/},
1884+ title = {Happy User Guide},
1885+ year = {2001},
1886+ author = {Simon Marlow and Andy Gill}
1887+}
1888+
1889+@inproceedings{generic-haskell,
1890+ title = {Generic Haskell, Specifically},
1891+ author = {Dave Clarke and Andres L\"{o}h},
1892+ editor = {Jeremy Gibbons and Johan Jeuring},
1893+ booktitle = {Proceedings of the IFIP TC2 Working Conference on Generic Programming},
1894+ year = {2002},
1895+ publisher = {Kluwer Academic Publishers},
1896+ pages = {21--48}
1897+}
1898+
1899+@article{faking-it,
1900+ title = {Faking It -- Simulating Dependent Types in {Haskell}},
1901+ year = {2002},
1902+ author = {Conor McBride},
1903+ journal = {Journal of Functional Programming},
1904+ volume = {12},
1905+ number = {4+5},
1906+ pages = {375--392}
1907+}
1908+
1909+@misc{mcbride-inverting,
1910+ title = {Inverting Inductively Defined Relations in \textsc{Lego}},
1911+ year = {1996},
1912+ author = {Conor McBride}
1913+}
1914+
1915+@phdthesis{mcbride-thesis,
1916+ month = {May},
1917+ school = {University of Edinburgh},
1918+ title = {Dependently Typed Functional Programs and their proofs},
1919+ year = {2000},
1920+ author = {Conor McBride}
1921+}
1922+
1923+@article{mcbride-unification,
1924+ title = {First-Order Unification by Structural Recursion},
1925+ year = {2003},
1926+ author = {Conor McBride},
1927+ journal = {Journal of Functional Programming},
1928+ volume = {13},
1929+ number = {6},
1930+ pages = {1061--1075}
1931+}
1932+
1933+@misc{mckinna-pollack,
1934+ howpublished = {Kluwer Academic Publishers},
1935+ title = {Some Lambda Calculus and Type Theory formalized},
1936+ year = {1998},
1937+ author = {James McKinna and Robert Pollack}
1938+}
1939+
1940+@book{num-theory,
1941+ title = {An Introduction to the Theory of Numbers},
1942+ year = {1980},
1943+ publisher = {John Wiley and Sons},
1944+ author = {Ivan Niven and Herbert S. Zuckerman}
1945+}
1946+
1947+@book{prog-mltt,
1948+ title = {Programming in Martin-L\"{o}f's Type Theory -- An Introduction},
1949+ year = {1990},
1950+ publisher = {Oxford University Press},
1951+ author = {Bengt Nordstr\"{o}m and Kent Petersson and Jan M. Smith},
1952+ note = {Out of print. Available from http://www.cs.chalmers.se/Cs/Research/Logic}
1953+}
1954+
1955+@book{okasaki,
1956+ title = {Purely Functional Data Structures},
1957+ year = {1998},
1958+ publisher = {Cambridge University Press},
1959+ author = {Chris Okasaki}
1960+}
1961+
1962+@book{arith-systems,
1963+ title = {Computer Arithmetic Systems},
1964+ year = {1994},
1965+ publisher = {Prentice-Hall},
1966+ author = {Amos R. Omondi}
1967+}
1968+
1969+@book{pj-imp,
1970+ title = {The Implementation of Functional Programming Languages},
1971+ year = {1987},
1972+ publisher = {Prentice-Hall},
1973+ author = {Simon {Peyton Jones}}
1974+}
1975+
1976+@book{cp-bjc,
1977+ title = {Computational Numerical Methods},
1978+ year = {1986},
1979+ publisher = {John Wiley and Sons},
1980+ author = {C. Phillips and B. Cornelius}
1981+}
1982+
1983+@book{nag,
1984+ title = {The NAG Library: a beginner's guide},
1985+ year = {1986},
1986+ publisher = {Oxford : Clarendon Press},
1987+ author = {Jen Phillips}
1988+}
1989+
1990+@misc{believe,
1991+ month = {September},
1992+ title = {How to Believe a Machine-Checked Proof},
1993+ year = {1996},
1994+ author = {Robert Pollack}
1995+}
1996+
1997+@phdthesis{pollack94,
1998+ school = {University of Edinburgh},
1999+ title = {The Theory of LEGO -- A Proof Checker for the Extended Calculus of Constructions},
2000+ year = {1994},
2001+ author = {Robert Pollack}
2002+}
2003+
2004+@inproceedings{intel-bug,
2005+ series = {LNCS},
2006+ volume = {915},
2007+ title = {Anatomy of the Pentium Bug},
2008+ publisher = {Springer-Verlag},
2009+ year = {1995},
2010+ pages = {97--107},
2011+ author = {V.R. Pratt}
2012+}
2013+
2014+@book{maple,
2015+ title = {The Maple Handbook: Maple V Release 4},
2016+ year = {1996},
2017+ publisher = {Springer},
2018+ author = {Darren Redfern}
2019+}
2020+
2021+@book{crypto,
2022+ title = {Applied Cryptography: protocols, algorithms and source code in C.},
2023+ year = {1996},
2024+ publisher = {Wiley},
2025+ author = {Bruce Schneier}
2026+}
2027+
2028+@article{adts,
2029+ journal = {Mathematical Structures in Computer Science},
2030+ number = {2},
2031+ volume = {10},
2032+ title = {On lists and other abstract data types in the calculus of construction},
2033+ year = {2000},
2034+ pages = {261-276},
2035+ author = {Jonathan P. Seldin}
2036+}
2037+
2038+@article{seldin97,
2039+ journal = {Annals of Pure and Applied Logic},
2040+ number = {1},
2041+ month = {January},
2042+ volume = {83},
2043+ title = {On the proof theory of Coquand's calculus of constructions},
2044+ year = {1997},
2045+ pages = {23--101},
2046+ author = {Jonathan P. Seldin}
2047+}
2048+
2049+@article{wichmann,
2050+ journal = {The Computer Journal},
2051+ volume = {32},
2052+ title = {Towards a Formal Specification of Floating Point},
2053+ year = {1989},
2054+ pages = {432-436},
2055+ author = {B.A. Wichmann}
2056+}
2057+
2058+@book{mathematica,
2059+ title = {Mathematica : a system for doing mathematics by computer},
2060+ year = {1991},
2061+ publisher = {Addison Wesley},
2062+ author = {Stephen Wolfram}
2063+}
2064+
2065+@inproceedings{xi-imp,
2066+author = "Hongwei Xi",
2067+title = {{Imperative Programming with Dependent Types}},
2068+booktitle = "Proceedings of 15th {IEEE} Symposium on Logic in Computer Science",
2069+year = 2000,
2070+month = "June",
2071+address = "Santa Barbara",
2072+pages = "375--387"
2073+}
2074+
2075+@phdthesis{xi-thesis,
2076+ month = {December},
2077+ school = {Department of Mathematical Sciences, Carnegie Mellon University},
2078+ title = {Dependent Types in Practical Programming},
2079+ year = {1998},
2080+ author = {Hongwei Xi}
2081+}
2082+
2083+
2084+@techreport{dtal,
2085+author = {Hongwei Xi and Robert Harper},
2086+title = {A Dependently Typed Assembly Language},
2087+institution = {Computer Science and Engineering Department, Oregon Graduate Institute},
2088+year = 1999,
2089+number = {OGI-CSE-99-008},
2090+month = {July},
2091+}
2092+
2093+@misc{bignum-cmp,
2094+ month = {February},
2095+ title = {Comparison of three public-domain multiprecision libraries: BigNum, Gmp and Pari},
2096+ year = {1998},
2097+ author = {Paul Zimmerman}
2098+}
2099+
2100+@book{perl,
2101+ title = {Programming Perl},
2102+ author = {Larry Wall and Tom Christiansen and Jon Orwant},
2103+ year = {2000},
2104+ edition = {3rd},
2105+ publisher = {O'Reilly}
2106+}
2107+
2108+@misc{python,
2109+ howpublished = {http://www.python.org/doc/current/tut/tut.html},
2110+ month = {April},
2111+ title = {Python Tutorial},
2112+ year = {2001},
2113+ author = {Guido van {Rossum} and Fred L. {Drake, Jr}}
2114+}
2115+
2116+@book{logic,
2117+ title = {The Language of First Order Logic},
2118+ year = {1992},
2119+ publisher = {CSLI Lecture Notes},
2120+ author = {Jon Barwise and John Etchemendy}
2121+}
2122+
2123+@book{haskell,
2124+ title = {Haskell -- The Craft of Functional Programming},
2125+ year = {1999},
2126+ publisher = {Addison Wesley},
2127+ author = {Simon Thompson}
2128+}
2129+
2130+@inproceedings{coq-hol,
2131+ title = {A Comparative Study of Coq and HOL},
2132+ year = {1997},
2133+ booktitle = {Theorem Proving in Higher Order Logics},
2134+ pages = {323-337},
2135+ author = {Vincent Zammit}
2136+}
2137+
2138+@misc{gay90,
2139+ month = {November},
2140+ title = {Correctly Rounded Binary-Decimal and Decimal-Binary Conversions},
2141+ year = {1990},
2142+ author = {David M. Gay},
2143+ note = {AT&T Bell Laboratories, Numerical Analysis Manuscript 90-10}
2144+}
2145+
2146+@article{hughes-matters,
2147+ journal = {Computer Journal},
2148+ number = {2},
2149+ volume = {32},
2150+ title = {Why Functional Programming Matters},
2151+ year = {1989},
2152+ pages = {98--107},
2153+ author = {J. Hughes}
2154+}
2155+
2156+@inproceedings{proofpointing,
2157+ title = {Proof by Pointing},
2158+ year = {1994},
2159+ booktitle = {Proceedings of the International Symposium on Theoretical Aspects of Computer So},
2160+ pages = {141--160},
2161+ editor = {M. Hagiya and J. C. Mitchell},
2162+ publisher = {Springer-Verlag},
2163+ series = {LNCS},
2164+ volume = {789},
2165+ address = {Sendai, Japan},
2166+ author = {Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry}
2167+}
2168+
2169+@misc{inductive-coq,
2170+ month = {December},
2171+ title = {Inductive Definitions in the System Coq -- Rules and Properties},
2172+ year = {1992},
2173+ author = {Christine Paulin-Mohring}
2174+}
2175+
2176+@misc{leiserson98,
2177+ month = {July},
2178+ title = {Using de Bruijn Sequences to Index a 1 in a Computer Word},
2179+ year = {1998},
2180+ author = {{Charles E. Leiserson} and {Harald Prokop} and {Keith H. Randall}}
2181+}
2182+
2183+@inproceedings{proofchecking,
2184+ title = {A two-level approach towards lean proof-checking},
2185+ year = {1996},
2186+ booktitle = {TYPES},
2187+ pages = {16--35},
2188+ author = {G. Barthe and M.P.J. Ruys and H.P. Barendregt}
2189+}
2190+
2191+@inproceedings{congruence,
2192+ title = {Congruence Types},
2193+ year = {1995},
2194+ booktitle = {CSL},
2195+ pages = {36--51},
2196+ author = {Gilles Barthe and Herman Geuvers}
2197+}
2198+
2199+@phdthesis{geuvers-thesis,
2200+ title = {Logic and Type Systems},
2201+ author = {Herman Geuvers},
2202+ year = 1993,
2203+ school = {Katholieke Universiteit Nijmegen}
2204+}
2205+
2206+@techreport{multiple-values,
2207+ title = {Multiple Values in {Standard ML}},
2208+ year = {1994},
2209+ number = {94-312},
2210+ institution = {LFCS, Dept of Computer Science, University of Edinburgh},
2211+ author = {Kevin Mitchell}
2212+}
2213+
2214+@inproceedings{oracle-checking,
2215+ month = {January},
2216+ title = {Oracle-Based Checking of Untrusted Software},
2217+ year = {2001},
2218+ booktitle = {Proceedings of the 28th {ACM} Symposium on Principles of Programming Languages},
2219+ pages = {142--154},
2220+ author = {{George C. Necula} and {S.P. Rahul}}
2221+}
2222+
2223+@article{adams93jfp,
2224+ journal = {Journal of Functional Programming},
2225+ number = {4},
2226+ volume = {3},
2227+ title = {Efficient Sets -- A Balancing Act},
2228+ year = {1993},
2229+ pages = {553--561},
2230+ author = {Stephen Adams}
2231+}
2232+
2233+@inproceedings{hughes-sized,
2234+ title = {Proving the Correctness of Reactive Systems Using Sized Types},
2235+ year = {1996},
2236+ booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programmin},
2237+ pages = {410--423},
2238+ author = {John Hughes and Lars Pareto and Amr Sabry}
2239+}
2240+
2241+@inproceedings{whittle99ml,
2242+ title = {An {ML} Editor Based on Proofs-As-Programs},
2243+ year = {1999},
2244+ booktitle = {Automated Software Engineering},
2245+ pages = {166--173},
2246+ author = {Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe}
2247+}
2248+
2249+@book{efp-typeinf,
2250+ title = {Elements of Functional Programming},
2251+ year = {1989},
2252+ publisher = {Addison-Wesley},
2253+ author = {Chris Reade},
2254+ series = {International Computer Science Series}
2255+}
2256+
2257+@incollection{ wadler-views,
2258+ author = "Philip Wadler",
2259+ title = "Views: {A} Way for Pattern Matching to Cohabit with Data Abstraction",
2260+ booktitle = "Proceedings, 14th Symposium on Principles of Programming Languages",
2261+ publisher = "Association for Computing Machinery",
2262+ editor = "Steve Munchnik",
2263+ pages = "307--312",
2264+ year = "1987",
2265+ url = "citeseer.nj.nec.com/wadler87views.html" }
2266+
2267+@article{ coquand-checking,
2268+ author = "Thierry Coquand",
2269+ title = "An Algorithm for Type-Checking Dependent Types",
2270+ journal = "Science of Computer Programming",
2271+ volume = "26",
2272+ number = "1-3",
2273+ pages = "167-177",
2274+ year = "1996",
2275+ url = "citeseer.nj.nec.com/coquand96algorithm.html" }
2276+
2277+@misc{coquand-pm,
2278+ author = "Thierry Coquand",
2279+ title = "Pattern Matching with Dependent Types",
2280+ year = "1992",
2281+ howpublished = "Available from \verb+http://www.cs.chalmers.se/~coquand/type.html+"
2282+}
2283+
2284+@misc{pollack-records,
2285+ month = {August},
2286+ title = {Dependently Typed Records for Representing Mathematical Structure},
2287+ year = {2000},
2288+ author = {Robert Pollack}
2289+}
2290+
2291+@article{checking-betarte,
2292+ journal = {Journal of Functional Programming},
2293+ number = {2},
2294+ month = {March},
2295+ volume = {10},
2296+ title = {Type checking dependent (record) types and subtyping},
2297+ year = {2000},
2298+ pages = {137--166},
2299+ author = {Gustavo Betarte}
2300+}
2301+
2302+
2303+@article{ gcode,
2304+ author = "Thomas Johnsson",
2305+ title = "Efficient Compilation of Lazy Evaluation",
2306+ booktitle = "Proceedings of the {{ACM}} {{SIGPLAN}}'84 Symposium on Compiler Con struction",
2307+ journal = "{SIGPLAN} Notices",
2308+ volume = "19",
2309+ number = "6",
2310+ month = "June",
2311+ publisher = "{ACM} Press",
2312+ pages = "58--69",
2313+ year = "1984",
2314+ url = "citeseer.nj.nec.com/johnsson84efficient.html" }
2315+
2316+@misc{kamareddine01,
2317+ month = {February},
2318+ title = {Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems},
2319+ year = {2001},
2320+ author = {Fairouz Kamareddine}
2321+}
2322+
2323+@book{prooftheory,
2324+ title = {Basic Proof Theory},
2325+ year = {1996},
2326+ publisher = {Cambridge University Press},
2327+ author = {A.S. Troelstra and H. Schwichtenberg},
2328+ series = {Cambridge Tracts in Theoretical Computer Science}
2329+}
2330+
2331+@misc{nbe_staged,
2332+ title = {Integrating Normalization-by-Evaluation into a Staged Programming Language},
2333+ year = {1998},
2334+ author = {Tim Sheard}
2335+}
2336+
2337+@inproceedings{nbe2,
2338+ title = {Normalization by evaluation},
2339+ year = {1998},
2340+ author = {Ulrich Berger and Matthias Eberl and Helmut Schwichtenberg},
2341+ booktitle = {Prospects for Hardware Foundations 1998},
2342+ pages = {117--137},
2343+ series = {LNCS}
2344+}
2345+
2346+
2347+
2348+@misc{rtcg_jfp,
2349+ title = {Compiling for Run-time Code Generation},
2350+ year = {2000},
2351+ author = {Frederick Smith and Dan Grossman and Greg Morrisett and Luke Hornof and Trevor J},
2352+ note = {Under consideration for J. Functional Programming}
2353+}
2354+
2355+@phdthesis{fredsmith_thesis,
2356+ month = {January},
2357+ school = {Cornell University},
2358+ title = {Certified Run-time Code Generation},
2359+ year = {2002},
2360+ author = {Frederick Smith}
2361+}
2362+
2363+@inproceedings{xi_arraybounds,
2364+author = "Hongwei Xi and Frank Pfenning",
2365+title = {Eliminating Array Bound Checking through Dependent Types},
2366+booktitle = "Proceedings of {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation",
2367+year = 1998,
2368+month = "June",
2369+address = "Montreal",
2370+pages = "249--257",
2371+}
2372+
2373+@inproceedings{xi_deadcode,
2374+author = "Hongwei Xi",
2375+title = {Dead Code Elimination through Dependent Types},
2376+booktitle = "The First International Workshop on Practical Aspects of Declarative Languages",
2377+year = 1999,
2378+month = "January",
2379+address = "San Antonio",
2380+pages = "228--242"
2381+}
2382+
2383+@book{compilers,
2384+ title = {Compilers --- Principles, Techniques and Tools},
2385+ year = {1986},
2386+ publisher = {Addison-Wesley},
2387+ author = {Alfred Aho and Ravi Sethi and Jeffrey Ullman}
2388+}
2389+
2390+@inproceedings{nhc,
2391+ title = {Highlights from nhc: A space efficient {Haskell} Compiler},
2392+ year = {1995},
2393+ author = "Niklas R{\"o}jemo",
2394+ booktitle = "Functional Programming Languages and Computer Architecture",
2395+ pages = "282--292"
2396+}
2397+
2398+
2399+@misc{mlmatch,
2400+ title = {SML/NJ Match Compiler Notes},
2401+ year = {1992},
2402+ author = {William Aitken}
2403+}
2404+
2405+@misc{mlmatch_sestoft,
2406+ title = {ML pattern match compilation and partial evaluation},
2407+ year = {1992},
2408+ author = {Peter Sestoft}
2409+}
2410+
2411+@inproceedings{compiledstrongreduction,
2412+ title = {A Compiled Implementation of Strong Reduction},
2413+ year = {2002},
2414+ author = {Benjamin Gr\'{e}goire and Xavier Leroy},
2415+ booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},
2416+ pages = {235--246}
2417+}
2418+
2419+@misc{tclhaskell,
2420+ howpublished = {http://www.dcs.gla.ac.uk/~meurig/TclHaskell/usermanual.html},
2421+ month = {August},
2422+ title = {TclHaskell - User Manual},
2423+ year = {1999},
2424+ author = {Meurig Sage}
2425+}
2426+
2427+
2428+@InProceedings{nbe-cat,
2429+ author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
2430+ title = "Categorical reconstruction of a reduction free
2431+ normalization proof",
2432+ year = "1995",
2433+ booktitle = "Category Theory and Computer Science",
2434+ editor = {David Pitt and David E. Rydeheard and Peter Johnstone},
2435+ series = {LNCS},
2436+ volume = {953},
2437+ pages = {182-199}
2438+}
2439+
2440+@inproceedings{presburgerEFSM,
2441+ title = {A Comparison of Presburger Engines for EFSM Reachability},
2442+ year = {1998},
2443+ booktitle = {Computer Aided Verification '98},
2444+ pages = {280--292},
2445+ author = {Thomas R. Shiple and James H. Kukula and Rajeev K. Ranjan}
2446+}
2447+
2448+@misc{typesafecast,
2449+ title = {Type-Safe Cast},
2450+ year = {2000},
2451+ author = {Stephanie Weirich}
2452+}
2453+
2454+@phdthesis{grobauer-thesis,
2455+ school = {University of Aarhus},
2456+ title = {Topics in Semantics Based Program Manipulation},
2457+ year = {2001},
2458+ author = {Bernd Grobauer}
2459+}
2460+
2461+@misc{monads-moggi,
2462+ title = {Computational Lambda Calculus and Monads},
2463+ year = {1989},
2464+ author = {Eugenio Moggi}
2465+}
2466+
2467+@article{gmp-proof,
2468+ title = {A proof of {GMP} square root},
2469+ year = {2002},
2470+ journal = {Journal of Automated Reasoning},
2471+ volume = {29},
2472+ pages = {225--252},
2473+ author = {Yves Bertot and Nicolas Magaud and Paul Zimmerman}
2474+}
2475+
2476+@article{F-tal,
2477+ journal = {{ACM} Transactions on Programming Languages and Systems},
2478+ number = {3},
2479+ month = {May},
2480+ volume = {21},
2481+ title = {From {System F} to Typed Assembly Language},
2482+ year = {1999},
2483+ pages = {528--569},
2484+ author = {Greg Morrisett and David Walker and Karl Crary and Neal Glew}
2485+}
2486+
2487+@techreport{nbe-rtcg,
2488+ month = {December},
2489+ title = {Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation},
2490+ year = {1997},
2491+ institution = {BRICS},
2492+ author = {Vincent Balat and Oliver Danvy}
2493+}
2494+
2495+@misc{yong-schemata,
2496+ howpublished = {http://www.dur.ac.uk/yong.luo/},
2497+ title = {A Methodology for Implementing Inductive Schemata},
2498+ year = {2002},
2499+ author = {Yong Luo and Zhaohui Luo}
2500+}
2501+
2502+@inproceedings{harper93,
2503+ title = {Explicit Polymorphism and CPS Conversion},
2504+ year = {1993},
2505+ booktitle = {20th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
2506+ pages = {206--219},
2507+ publisher = {{ACM} Press, New York, NY, USA},
2508+ author = {Robert Harper and Mark Lillibridge}
2509+}
2510+
2511+@techreport{backends,
2512+ month = {November},
2513+ title = {Functional Back-Ends within the Lambda-Sigma Calculus},
2514+ year = {1996},
2515+ institution = {INRIA},
2516+ author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
2517+}
2518+
2519+@article{stg,
2520+ title = {Implementing lazy functional languages on stock hardware -- the {Spineless Tagless G-machine}},
2521+ year = {1992},
2522+ journal = {Journal of Functional Programming},
2523+ volume = {2},
2524+ number = {2},
2525+ pages = {127--202},
2526+ month = {April},
2527+ author = {Simon {Peyton Jones}}
2528+}
2529+
2530+@article{debruijn,
2531+ journal = {Indagationes Mathematicae},
2532+ volume = {34},
2533+ title = {Lambda calculus notation with nameless dummies},
2534+ year = {1972},
2535+ pages = {381--392},
2536+ author = {N.G. de Bruijn}
2537+}
2538+
2539+@book{assembly,
2540+ month = {January},
2541+ title = {PC Assembly Language},
2542+ year = {2002},
2543+ publisher = {http://www.drpaulcarter.com/},
2544+ author = {Paul A. Carter}
2545+}
2546+
2547+@inproceedings{poly99,
2548+ title = {Once Upon A Polymorphic Type},
2549+ year = {1999},
2550+ booktitle = {26th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
2551+ publisher = {{ACM}},
2552+ author = {Keith Wansbrough and Simon {Peyton Jones}}
2553+}
2554+
2555+@misc{lazy_intro,
2556+ title = {Compiling Lazy Functional Languages: An introduction},
2557+ year = {1986},
2558+ author = {Thomas Johnsson}
2559+}
2560+
2561+@inproceedings{unboxed-fp,
2562+ month = {Sept},
2563+ title = {Unboxed Values as First Class Citizens in a Non-Strict Functional Language},
2564+ year = {1991},
2565+ author = {Simon {Peyton Jones} and John Launchbury},
2566+ booktitle = {Functional Programming Languages and Computer Architecture (FPCA'91)},
2567+ crossref = {fplca91},
2568+ pages = {636--666}
2569+}
2570+
2571+@inproceedings{abc-machine,
2572+ author = {Sjaak Smetsers and Eric N{\"{o}}cker and John {van Groningen} and Rinus Plasmeijer},
2573+ title = {Generating efficient code for lazy functional languages},
2574+ booktitle = {Functional programming Languages and Computer Architecture},
2575+ year = {1991},
2576+ pages = {592--617},
2577+ crossref = {fplca91}
2578+}
2579+
2580+@proceedings{fplca91,
2581+ title = {Functional programming Languages and Computer Architecture},
2582+ year = {1991},
2583+ volume = {523},
2584+ series = {LNCS},
2585+ publisher = {Springer-Verlag},
2586+ editor = {John Hughes}
2587+}
2588+
2589+
2590+
2591+@inproceedings{nbe,
2592+ title = {An inverse of the evaluation functional for typed $\lambda$-calculus},
2593+ year = {1991},
2594+ booktitle = {Proc. 1991 {IEEE} Symp. on Logic in Comp. Sci.},
2595+ pages = {203--211},
2596+ editor = {R. Vemuri},
2597+ author = {Ulrich Berger and Helmut Schwichtenberg}
2598+}
2599+
2600+@inproceedings{typed-closure,
2601+ title = {Typed Closure Conversion},
2602+ year = {1996},
2603+ booktitle = {Symposium on Principles of Programming Languages},
2604+ pages = {271--283},
2605+ author = {Yasuhiko Minamide and J. Gregory Morrisett and Robert Harper}
2606+}
2607+
2608+@misc{ghc-commentary,
2609+ howpublished = {http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/},
2610+ title = {The Glasgow Haskell Compiler (GHC) Commentary},
2611+ year = {2002},
2612+ author = {Manuel M. T. Chakravarty and Sigbjorn Finne and Simon Marlow and Simon {Peyton Jones} and Julian Seward and Reuben Thomas},
2613+ note = {Available from GHC CVS repository}
2614+}
2615+
2616+@inproceedings{lambdalift,
2617+ month = {September},
2618+ title = {Lambda Lifting: Transforming Programs to Recursive Equations},
2619+ year = {1985},
2620+ booktitle = {Functional Programming Languages and Computer Architecture},
2621+ pages = {190--203},
2622+ editor = {Jean-Pierre Jouannaud},
2623+ publisher = {Springer-Verlag},
2624+ author = {Thomas Johnsson}
2625+}
2626+
2627+@inproceedings{til,
2628+ title = {TIL: A Type-Directed Optimizing Compiler for ML},
2629+ year = {1996},
2630+ booktitle = {Proc. {{ACM}} {{SIGPLAN}} '96 Conference on Programming Language Design and Implementation},
2631+ pages = {181--192},
2632+ author = {D. Tarditi and G. Morrisett and P. Cheng and C. Stone and R. Harper and P. Lee}
2633+}
2634+
2635+@phdthesis{shao94,
2636+ school = {Princeton University},
2637+ title = {Compiling Standard {ML} for Efficient Execution on Modern Machines},
2638+ year = {1994},
2639+ author = {Zhong Shao}
2640+}
2641+
2642+@inproceedings{gmachine,
2643+ month = {September},
2644+ title = {The {G-Machine}: A fast, graph-reduction evaluator},
2645+ year = {1985},
2646+ booktitle = {Functional Programming Languages and Computer Architecture},
2647+ pages = {400--413},
2648+ editor = {Jean-Pierre Jouannaud},
2649+ publisher = {Springer-Verlag},
2650+ author = {R.B. Kieburtz}
2651+}
2652+
2653+@inproceedings{strictness,
2654+ month = {September},
2655+ title = {Strictness Analysis - A practical approach},
2656+ year = {1985},
2657+ booktitle = {Functional Programming Languages and Computer Hardware},
2658+ pages = {35--49},
2659+ editor = {Jean-Pierre Jouannaud},
2660+ publisher = {Springer-Verlag},
2661+ author = {Chris Clack and Simon {Peyton Jones}}
2662+}
2663+
2664+@book{fl-impl,
2665+ title = {Implementing Functional Languages - A Tutorial},
2666+ year = {1992},
2667+ publisher = {Prentice Hall International},
2668+ author = {Simon {Peyton Jones} and David Lester}
2669+}
2670+
2671+@phdthesis{capretta-thesis,
2672+ school = {Katholieke Universiteit Nijmegen},
2673+ title = {Abstraction and Computation},
2674+ year = {2002},
2675+ author = {Venanzio Capretta}
2676+}
2677+
2678+@article{bird-pointer,
2679+ journal = {Journal of Functional Programming},
2680+ number = {3},
2681+ month = {May},
2682+ volume = {11},
2683+ title = {Unfolding Pointer Algorithms},
2684+ year = {2001},
2685+ pages = {347--358},
2686+ author = {Richard S. Bird}
2687+}
2688+
2689+@article{impl-tp,
2690+ journal = {Journal of Functional Programming},
2691+ number = {2},
2692+ month = {March},
2693+ volume = {9},
2694+ title = {Implementing Theorem Provers in a Purely Functional Style},
2695+ year = {1999},
2696+ pages = {147--166},
2697+ author = {Keith Hanna}
2698+}
2699+
2700+@article{shrink-lambda,
2701+ journal = {Journal of Functional Programming},
2702+ number = {5},
2703+ month = {September},
2704+ volume = {7},
2705+ title = {Shrinking Lambda Expressions in Linear Time},
2706+ year = {1997},
2707+ pages = {515--540},
2708+ author = {Andrew W. Appel and Trevor Jim}
2709+}
2710+
2711+@article{stack-tal,
2712+ journal = {Journal of Functional Programming},
2713+ number = {1},
2714+ month = {January},
2715+ volume = {12},
2716+ title = {Stack-based Typed Assembly Language},
2717+ year = {2002},
2718+ pages = {43--88},
2719+ author = {Greg Morrisset and Karl Crart and Neal Glew and David Walker}
2720+}
2721+
2722+@article{runtime-lamsig,
2723+ journal = {Journal of Functional Programming},
2724+ number = {2},
2725+ month = {March},
2726+ volume = {8},
2727+ title = {Functional Runtime Systems within the lambda-sigma Calculus},
2728+ year = {1998},
2729+ pages = {131--176},
2730+ author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
2731+}
2732+
2733+@article{busylazy,
2734+ journal = {Journal of Functional Programming},
2735+ number = {6},
2736+ month = {November},
2737+ volume = {11},
2738+ title = {How to look busy while being as lazy as ever: the Implementation of a lazy functional debugger},
2739+ year = {2001},
2740+ pages = {629--671},
2741+ author = {Henrik Nilsson}
2742+}
2743+
2744+@article{lazyveager,
2745+ journal = {Journal of Functional Programming},
2746+ number = {5},
2747+ month = {September},
2748+ volume = {7},
2749+ title = {More haste, less speed: lazy versus eager evaluation},
2750+ year = {1997},
2751+ pages = {541--547},
2752+ author = {Richard Bird and Geraint Jones and Oege {de Moor}}
2753+}
2754+
2755+@article{jvm-fp,
2756+ journal = {Journal of Functional Programming},
2757+ number = {6},
2758+ month = {November},
2759+ volume = {9},
2760+ title = {Compiling lazy functional programs for the Java Virtual Machine},
2761+ year = {1999},
2762+ pages = {579--603},
2763+ author = {David Wakeling}
2764+}
2765+
2766+@book{isabelle,
2767+ publisher = {Springer-Verlag},
2768+ series = {LNCS},
2769+ volume = {2283},
2770+ month = {March},
2771+ title = {Isabelle/HOL - A proof assistant for higher order logic},
2772+ year = {2002},
2773+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}
2774+}
2775+
2776+@article{ghc-inliner,
2777+ journal = {Journal of Functional Programming},
2778+ number = {4},
2779+ month = {September},
2780+ volume = {12},
2781+ title = {Secrets of the {Glasgow Haskell Compiler} inliner},
2782+ year = {2002},
2783+ pages = {393--434},
2784+ author = {Simon {Peyton Jones} and Simon Marlow}
2785+}
2786+
2787+@article{dynamic-fp,
2788+ journal = {Journal of Functional Programming},
2789+ number = {1},
2790+ month = {January},
2791+ volume = {8},
2792+ title = {The dynamic compiliation of lazy functional programs},
2793+ year = {1998},
2794+ pages = {61--81},
2795+ author = {David Wakeling}
2796+}
2797+
2798+@misc{isabelle-ref,
2799+ month = {March},
2800+ title = {Isabelle Reference Manual},
2801+ year = {2002},
2802+ author = {Lawrence C. Paulson}
2803+}
2804+
2805+@article{debruijn-nested,
2806+ journal = {Journal of Functional Programming},
2807+ number = {1},
2808+ month = {January},
2809+ volume = {9},
2810+ title = {de Bruijn notation as a nested datatype},
2811+ year = {1999},
2812+ pages = {77--91},
2813+ author = {Richard S. Bird and Ross Paterson}
2814+}
2815+
2816+@article{perfect-trees,
2817+ journal = {Journal of Functional Programming},
2818+ number = {3},
2819+ month = {May},
2820+ volume = {10},
2821+ title = {Perfect trees and bit-reversal permutations},
2822+ year = {2000},
2823+ pages = {305--317},
2824+ author = {Ralf Hinze}
2825+}
2826+
2827+@phdthesis{paulin-extraction,
2828+ school = {Paris 7},
2829+ title = {Extraction de programmes dans le Calcul des Constructions},
2830+ year = {1989},
2831+ author = {Christine Paulin-Mohring}
2832+}
2833+
2834+@phdthesis{santos95,
2835+ school = {University of Glasgow},
2836+ title = {Compilation By Transformation In Non-Strict Functional Languages},
2837+ year = {1995},
2838+ author = {{Andr\'{e} Lu\'{i}s de Medeiros} Santos}
2839+}
2840+
2841+@book{cps,
2842+ title = {Compiling With Continuations},
2843+ year = {1992},
2844+ publisher = {Cambridge University Press},
2845+ author = {Andrew W. Appel}
2846+}
2847+
2848+@techreport{SKIM,
2849+ number = {31},
2850+ title = {The {SKIM} microprogrammer's guide},
2851+ year = {1983},
2852+ institution = {University of Cambridge},
2853+ author = {W.R. Stoye}
2854+}
2855+
2856+@misc{NORMA,
2857+ title = {An Overview of Burroughs {NORMA}},
2858+ year = {1985},
2859+ author = {H. Richards}
2860+}
2861+
2862+@book{ml,
2863+ title = {The Definition of Standard ML --- Revised},
2864+ year = {1997},
2865+ publisher = {MIT Press},
2866+ author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}
2867+}
2868+
2869+@misc{ml71,
2870+ title = {An intuitionistic theory of types},
2871+ year = {1971},
2872+ author = {Per Martin-L\"{o}f}
2873+}
2874+
2875+@phdthesis{girard-thesis,
2876+ school = {Universit\'{e} Paris VII},
2877+ title = {Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur},
2878+ year = {1972},
2879+ author = {Jean-Yves Girard}
2880+}
2881+
2882+@inproceedings{ml75,
2883+ title = {An intuitionistic theory of types: predicative part},
2884+ year = {1975},
2885+ booktitle = {Logic Colloquium '73},
2886+ editor = {H. Rose and J.C. Shepherdson},
2887+ publisher = {North-Holland},
2888+ author = {Per Martin-L\"{o}f}
2889+}
2890+
2891+@inproceedings{cpm90,
2892+ title = {Inductively defined types},
2893+ year = {1990},
2894+ author = {Thierry Coquand and Christine Paulin-Mohring},
2895+ series = {LNCS},
2896+ volume = {417},
2897+ publusher = {Springer-Verlag}
2898+}
2899+
2900+@phdthesis{fpcustom,
2901+ month = {May},
2902+ school = {Computer Lab, University of Cambridge},
2903+ title = {The Implementation of Functional Languages using Custom Hardware},
2904+ year = {1985},
2905+ author = {W.R. Stoye}
2906+}
2907+
2908+@phdthesis{hughesthesis,
2909+ month = {September},
2910+ school = {Programming Research Group, Oxford},
2911+ title = {The design and implementation of programming languages},
2912+ year = {1984},
2913+ author = {John Hughes}
2914+}
2915+
2916+@inproceedings{tim,
2917+ volume = {274},
2918+ title = {{TIM} -- A simple lazy abstract machine to execute supercombinators},
2919+ year = {1987},
2920+ booktitle = {Functional Programming Languages and Computer Architecture},
2921+ publisher = {Springer-Verlag},
2922+ author = {John Fairbairn and Stuart Wray},
2923+ pages = {34--45},
2924+ series = {LNCS}
2925+}
2926+
2927+@techreport{abc,
2928+ title = {The {ABC} machine -- A Sequential Stack-based Abstract Machine For Graph Rewriting},
2929+ year = {1990},
2930+ institution = {University of Nijmegen},
2931+ author = {P.W.M. Koopman and M.C.J.D. van {Eekelen} and E.G.J.M.H. Ncker and J.E.W. Smetsers and M.J. Plasmeijer}
2932+}
2933+
2934+@techreport{implicit,
2935+ title = {On Implicit Arguments},
2936+ year = {1994},
2937+ institution = {Faculty of Science, University of Tokyo},
2938+ author = {Masami Hagiya and Yozo Toda}
2939+}
2940+
2941+@book{semantics,
2942+ title = {Denotational Semantics},
2943+ year = {1986},
2944+ publisher = {Wm. C. Brown},
2945+ author = {David A. Schmidt}
2946+}
2947+
2948+@inproceedings{lazyml,
2949+ month = {August},
2950+ title = {A compiler for {Lazy} {ML}},
2951+ year = {1984},
2952+ booktitle = {Proceedings of the {{ACM}} Symposium on Lisp and Functional Programming},
2953+ pages = {218--227},
2954+ author = {Lennart Augustsson}
2955+}
2956+
2957+@inproceedings{nu-g,
2958+ title = {Parallel graph reduction with the $\langle\nu,G\rangle$-machine},
2959+ year = {1989},
2960+ booktitle = {Functional Programming Languages and Computer Architecture},
2961+ publisher = {{ACM} Press},
2962+ author = {Lennart Augustsson and Thomas Johnsson}
2963+}
2964+
2965+@book{k&r,
2966+ title = {The C programming language},
2967+ year = {1988},
2968+ publisher = {Prentice-Hall},
2969+ author = {Brian W. Kernighan and Dennis M. Ritchie}
2970+}
2971+
2972+@misc{c--garbage,
2973+ title = {C--: a portable assembly language that supports garbage collection},
2974+ year = {1999},
2975+ author = {Simon {Peyton Jones} and Norman Ramsey and Fermin Reig},
2976+ note = {Invited talk at PPDP'99}
2977+}
2978+
2979+@misc{epigram,
2980+ howpublished = {http://www.dur.ac.uk/CARG/epigram.html},
2981+ title = {Project Proposal: {Epigram}: Innovative Programming via Inductive Families},
2982+ year = {2002},
2983+ author = {Zhaohui Luo and James McKinna and Paul Callaghan and Conor McBride}
2984+}
2985+
2986+@misc{ghc-rewrite,
2987+ title = {Playing by the Rules: Rewriting as a practical optimisation technique in {GHC}},
2988+ year = {2001},
2989+ author = {Simon {Peyton Jones} and Andrew Tolmach and Tony Hoare}
2990+}
2991+
2992+@UNPUBLISHED{implicit-pollack,
2993+ AUTHOR = {Robert Pollack},
2994+ TITLE = {Implicit Syntax},
2995+ NOTE = {Informal Proceedings of First Workshop on
2996+ Logical Frameworks, Antibes},
2997+ YEAR = {1990},
2998+ MONTH = MAY
2999+}
3000+
3001+
3002+@article{transform-haskell,
3003+ journal = {Science of Computer Programming},
3004+ volume = {32},
3005+ title = {A transformation-based optimiser for {Haskell}},
3006+ year = {1998},
3007+ pages = {3--47},
3008+ author = {Simon {Peyton Jones} and Andr\'{e} L. M. Santos}
3009+}
3010+
3011+@inproceedings{knuth-bendix,
3012+ title = {Simple Word Problems in Universal Algebras},
3013+ year = {1970},
3014+ booktitle = {Computational Problems in Abstract Algebra},
3015+ pages = {263--298},
3016+ editor = {John Leech},
3017+ publisher = {Pergamon Press},
3018+ author = {Donald E. Knuth and Peter B. Bendix}
3019+}
3020+
3021+@inproceedings{phantomfun,
3022+ title = {Fun With Phantom Types},
3023+ author = {Ralf Hinze},
3024+ pages = {245--262},
3025+ year = {2003},
3026+ crossref = {funprogramming},
3027+ booktitle = {The Fun Of Programming},
3028+ publisher = {Palgrave}
3029+}
3030+
3031+@book{funprogramming,
3032+ month = {March},
3033+ title = {The Fun Of Programming},
3034+ year = {2003},
3035+ editor = {Jeremy Gibbons and Oege {de Moor}},
3036+ publisher = {Palgrave},
3037+ series = {Cornerstones of Computing}
3038+}
3039+
3040+@inproceedings{anderson-proof,
3041+ title = {Representing Proof Transformations For Program Optimization},
3042+ year = {1994},
3043+ booktitle = {International Conference On Automated Deduction},
3044+ publisher = {Springer Verlag},
3045+ author = {Penny Anderson}
3046+}
3047+
3048+@phdthesis{daria-thesis,
3049+ month = {April},
3050+ school = {Institute of Informatics, Warsaw University},
3051+ title = {Termination of Rewriting in the Calculus of Constructions},
3052+ year = {2003},
3053+ author = {Daria Walukiewicz-Chrzaszcz}
3054+}
3055+
3056+@inproceedings{change-data,
3057+ title = {Changing Data Structures In Type Theory: A Study Of Natural Numbers},
3058+ year = {2001},
3059+ booktitle = {Types For Proofs And Programs 2000},
3060+ pages = {181--196},
3061+ editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
3062+ publisher = {Springer},
3063+ author = {Nicolas Magaud and Yves Bertot}
3064+}
3065+
3066+@phdthesis{nico-thesis,
3067+ title = {Changement de Representation des donn\'{e}es dans le Calcul de Constructions},
3068+ author = {Nicolas Magaud},
3069+ year = {2003},
3070+ month = {October},
3071+ school = {Universit\'{e} de Nice - Sophia Antipolis}
3072+}
3073+
3074+
3075+@book{patterns,
3076+ title = {Design Patterns},
3077+ year = {1995},
3078+ publisher = {Addison Wesley},
3079+ author = {Erich Gamma and Richard Helm and Ralph Johnson and John Vlissides}
3080+}
3081+
3082+@misc{ghchugs,
3083+ month = {August},
3084+ title = {The New {GHC}/{Hugs} Runtime System},
3085+ year = {1998},
3086+ author = {Simon Marlow and Simon {Peyton Jones}}
3087+}
3088+
3089+@misc{stgrevised,
3090+ month = {February},
3091+ title = {The {STG} runtime system (revised)},
3092+ year = {1999},
3093+ author = {Simon {Peyton Jones} and Simon Marlow and Alastair Reid},
3094+ howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
3095+}
3096+
3097+@inproceedings{optimistic,
3098+ month = {March},
3099+ title = {Optimistic Evaluation --- an adaptive evaluation strategy for non-strict programs},
3100+ year = {2003},
3101+ author = {Robert Ennals and Simon {Peyton Jones}},
3102+ booktitle = {International Conference on Functional Programming},
3103+ pages = {287--298}
3104+}
3105+
3106+@phdthesis{ennals-thesis,
3107+ title = {Adaptive Evaluation of Non-Strict Programs},
3108+ author = {Robert Ennals},
3109+ year = {2003},
3110+ month = {December},
3111+ school = {King's College, University of Cambridge}
3112+}
3113+
3114+@article{garbage,
3115+ journal = {{ACM} Computing Surveys},
3116+ number = {3},
3117+ volume = {13},
3118+ title = {Garbage Collection of Linked Data Structures},
3119+ year = {1981},
3120+ pages = {341--367},
3121+ author = {Jacques Cohen}
3122+}
3123+
3124+@article{baker-gc,
3125+ journal = {Communications of the {ACM}},
3126+ number = {4},
3127+ month = {April},
3128+ volume = {21},
3129+ title = {List Processing In Real Time On A Serial Computer},
3130+ year = {1978},
3131+ pages = {280--294},
3132+ author = {Henry G. {Baker Jr}}
3133+}
3134+
3135+@misc{bc-rec,
3136+ month = {February},
3137+ title = {Modelling General Recursion in Type Theory},
3138+ year = {2003},
3139+ note = {Under consideration for publication in Math. Struct. in Comp. Science. Draft, DCS, CTH --- INRIA, Sophia Antipolis, France},
3140+ author = {Ana Bove and Venanzio Capretta}
3141+}
3142+
3143+@misc{global-tag,
3144+ title = {Global Tagging Optimization by Type Inference},
3145+ year = {1992},
3146+ author = {Fritz Henglein}
3147+}
3148+
3149+@book{esr,
3150+ month = {October},
3151+ title = {The Cathedral And The Bazaar},
3152+ year = {1999},
3153+ publisher = {O'Reilly},
3154+ author = {Eric Raymond}
3155+}
3156+
3157+@book{manmonth,
3158+ title = {The Mythical Man-month: Essays on Software Engineering},
3159+ year = {1975},
3160+ publisher = {Addison Wesley},
3161+ author = {Frederick P. Brooks}
3162+}
3163+
3164+@inproceedings{evalpush,
3165+ title = {How to make a fast curry: push/enter vs eval/apply},
3166+ year = {2004},
3167+ author = {Simon Marlow and Simon {Peyton Jones}},
3168+ booktitle = {International Conference on Functional Programming, Snowbird},
3169+ pages = {4--15}
3170+}
3171+
3172+@phdthesis{boquist-thesis,
3173+ month = {April},
3174+ school = {Chalmers University of Technology},
3175+ title = {Code Optimisation Techniques for Lazy Functional Languages},
3176+ year = {1999},
3177+ author = {Urban Boquist}
3178+}
3179+
3180+@book{formal-spec,
3181+ title = {Formal Specification Of Programming Languages},
3182+ year = {1981},
3183+ publisher = {Prentice-Hall},
3184+ author = {Frank G. Pagan}
3185+}
3186+
3187+@inproceedings{elim-motive,
3188+ title = {Elimination With A Motive},
3189+ year = {2000},
3190+ booktitle = {Types for Proofs and Programs},
3191+ pages = {197--216},
3192+ editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
3193+ publisher = {Springer},
3194+ author = {Conor McBride}
3195+}
3196+
3197+@article{telescope,
3198+ journal = {Information and Computation},
3199+ number = {2},
3200+ month = {April},
3201+ volume = {91},
3202+ title = {Telescoping Mappings in Typed Lambda Calculus},
3203+ year = {1991},
3204+ pages = {189--204},
3205+ author = {N.G. de Bruijn}
3206+}
3207+
3208+@misc{typeintype,
3209+ title = {Typechecking is undecidable when 'type' is a type},
3210+ year = {1989},
3211+ author = {Mark B. Reinhold}
3212+}
3213+
3214+@misc{core,
3215+ month = {September},
3216+ title = {An External Representation for the {GHC} Core Language},
3217+ year = {2001},
3218+ author = {Andrew Tolmach and {The GHC Team}}
3219+}
3220+
3221+@article{deforestation,
3222+ journal = {Theoretical Computer Science},
3223+ volume = {73},
3224+ title = {Deforestation: Transforming programs to eliminate trees},
3225+ year = {1990},
3226+ pages = {231--248},
3227+ author = {Philip Wadler}
3228+}
3229+
3230+@misc{hep,
3231+ month = {July},
3232+ title = {Architecture of the {Haskell} Execution Platform},
3233+ year = {1999},
3234+ author = {Julian Seward and Simon Marlow and Andy Gill and Sigbjorn Finne and Simon {Peyton Jones} },
3235+ note = {Version 6},
3236+ howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
3237+}
3238+
3239+@mastersthesis{wahlstedt-thesis,
3240+ month = {October},
3241+ school = {Chalmers University Of Technology},
3242+ title = {Detecting Termination Using Size Change In Parameter Values},
3243+ year = {2000},
3244+ author = {David Wahlstedt}
3245+}
3246+
3247+@inproceedings{size-change,
3248+ title = {The size-change principle for program termination},
3249+ year = {2001},
3250+ booktitle = {Proceedings of the 28th Annual {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
3251+ author = {Chin Soon Lee and Neil D. Jones and Amir Ben-Amram. }
3252+}
3253+
3254+@article{ski-turner,
3255+ journal = {Software -- Practice and Experience},
3256+ volume = {9},
3257+ title = {A new implementation technique for applicative languages},
3258+ year = {1979},
3259+ pages = {31--49},
3260+ author = {David Turner}
3261+}
3262+
3263+@inproceedings{turner-strong,
3264+ number = {1022},
3265+ title = {Elementary Strong Functional Programming},
3266+ year = {1996},
3267+ booktitle = {First International Symposium on Functional Programming Languages in Education, Nijmegen, Netherlands, December 1995.},
3268+ pages = {1--13},
3269+ publisher = {Springer},
3270+ author = {David Turner},
3271+ series = {LNCS}
3272+}
3273+
3274+@misc{clean,
3275+ title = {The {Concurrent CLEAN} Language Report (draft)},
3276+ year = {2003},
3277+ author = {Rinus Plasmeijer and Marko van Eekelen},
3278+ howpublished = {Available from \verb+http://www.cs.kun.nl/~clean/+}
3279+}
3280+
3281+@article{burstall-struct,
3282+ journal = {Computer Journal},
3283+ number = {1},
3284+ volume = {12},
3285+ title = {Proving Properties of Programs By Structural Induction},
3286+ year = {1969},
3287+ pages = {41--48},
3288+ author = {Rod Burstall}
3289+}
3290+
3291+@incollection{ barendregt-types,
3292+ author = "Henk Barendregt",
3293+ title = "Lambda Calculi with Types",
3294+ booktitle = "Handbook of Logic in Computer Science, Volumes 1 (Background: Mathematical Structures) and 2 (Background: Computational Structures), Abramsky \& Gabbay \& Maibaum (Eds.)",
3295+ publisher = "Clarendon",
3296+ volume = "2",
3297+ year = "1992",
3298+ url = "citeseer.nj.nec.com/barendregt92lambda.html" }
3299+
3300+@book{curry-feys,
3301+ title = {Combinatory Logic, volume 1},
3302+ year = {1958},
3303+ publisher = {North Holland},
3304+ author = {Haskell B. Curry and Robert Feys}
3305+}
3306+
3307+@phdthesis{bove-thesis,
3308+ month = {November},
3309+ school = {Chalmers University of Technology},
3310+ title = {General Recursion in Type Theory},
3311+ year = {2002},
3312+ author = {Ana Bove}
3313+}
3314+
3315+@inbook{ml-cm,
3316+ title = {Constructive Mathematics and Computer Programming},
3317+ year = {1985},
3318+ booktitle = {Mathematical Logic and Programming Languages},
3319+ publisher = {Prentice Hall},
3320+ author = {Per Martin-L\"{o}f}
3321+}
3322+
3323+@inproceedings{howard,
3324+ title = {The formulae-as-types notion of construction},
3325+ year = {1980},
3326+ booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},
3327+ editor = {Jonathan P. Seldin and J. Roger Hindley},
3328+ publisher = {Academic Press},
3329+ author = {William A. Howard},
3330+ note = {A reprint of an unpublished manuscript from 1969}
3331+}
3332+
3333+@inproceedings{talx86,
3334+ title = {TALx86: A Realistic Typed Assembly Language},
3335+ year = {1999},
3336+ booktitle = {{ACM} {SIGPLAN} Workshop on Compiler Support for System Software},
3337+ pages = {25--35},
3338+ author = {Greg Morrisett and Karl Crary and Neal Glew and Dan Grossman and Richard Samuels and Frederick Smith and David Walker and Stephanie Weirich and Steve Zdancewic}
3339+}
3340+
3341+@inproceedings{bove-capretta,
3342+ volume = {2152},
3343+ title = {Nested General Recursion and Partiality in Type Theory},
3344+ year = {2001},
3345+ booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLS 2001},
3346+ pages = {121--135},
3347+ editor = {Richard J. Boulton and Paul B. Jackson},
3348+ publisher = {Springer-Verlag},
3349+ author = {Ana Bove and Venanzio Capretta},
3350+ series = {LNCS}
3351+}
3352+
3353+@misc{lvm,
3354+ month = {November},
3355+ title = {LVM, the lazy virtual machine},
3356+ year = {2002},
3357+ author = {Daan Leijen}
3358+}
3359+
3360+@misc{ocaml,
3361+ howpublished = {\verb+http://caml.inria.fr/ocaml/htmlman/+},
3362+ month = {August},
3363+ title = {The {Objective Caml} system release 3.06},
3364+ year = {2002},
3365+ author = {Xavier Leroy}
3366+}
3367+
3368+@misc{lambdagoto,
3369+ title = {Lambda : The Ultimate Goto},
3370+ year = {1977},
3371+ author = {Guy L. {Steele Jr}},
3372+ note = {MIT AI Memo 443}
3373+}
3374+
3375+@inproceedings{ liu-tail,
3376+ author = "Yanhong A. Liu and Scott D. Stoller",
3377+ title = "From Recursion to Iteration: What are the Optimizations?",
3378+ booktitle = "Partial Evaluation and Semantic-Based Program Manipulation",
3379+ pages = "73-82",
3380+ year = "2000",
3381+ url = "citeseer.nj.nec.com/liu00from.html" }
3382+
3383+@inproceedings{aczel77,
3384+ title = {An Introduction To Inductive Definitions},
3385+ year = {1977},
3386+ booktitle = {Handbook of Mathematical Logic},
3387+ editor = {J. Barwise},
3388+ publisher = {North Holland},
3389+ author = {Peter Aczel}
3390+}
3391+
3392+@inproceedings{inductive-plastic,
3393+ volume = {1956},
3394+ title = {Implementation Techniques for Inductive Types in {Plastic}},
3395+ year = {1999},
3396+ booktitle = {Types for Proofs and Programs},
3397+ pages = {94--113},
3398+ editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith},
3399+ publisher = {Springer-Verlag},
3400+ author = {Paul Callaghan and Zhaohui Luo},
3401+ series = {LNCS}
3402+}
3403+
3404+@misc{graham,
3405+ howpublished = {Available from \verb+http://www.paulgraham.com/+},
3406+ month = {April},
3407+ title = {The Hundred Year Language},
3408+ year = {2003},
3409+ author = {Paul Graham},
3410+ note = {Keynote address at PyCon 2003}
3411+}
3412+
3413+@inproceedings{gimenez98,
3414+ volume = {1443},
3415+ title = {Structural Recursive Definitions in Type Theory},
3416+ year = {1998},
3417+ booktitle = {Proceedings of ICALP '98},
3418+ publisher = {Springer-Verlag},
3419+ author = {Eduardo Gim\'{e}nez},
3420+ series = {LNCS}
3421+}
3422+
3423+@article{quicksort,
3424+ journal = {Computer Journal},
3425+ number = {1},
3426+ volume = {5},
3427+ title = {Quicksort},
3428+ year = {1962},
3429+ pages = {10--15},
3430+ author = {C.A.R. Hoare}
3431+}
3432+
3433+@phdthesis{goguen-thesis,
3434+ school = {University of Edinburgh},
3435+ title = {A Typed Operational Semantics for Type Theory},
3436+ year = {1994},
3437+ author = {Healfdene Goguen}
3438+}
3439+
3440+@article{ph-universes,
3441+ journal = {Theoretical Computer Science},
3442+ number = {1},
3443+ volume = {89},
3444+ title = {Type Checking With Universes},
3445+ year = {1991},
3446+ pages = {107--136},
3447+ author = {Robert Harper and Randy Pollack}
3448+}
3449+
3450+@inproceedings{pm-compile,
3451+ month = {September},
3452+ title = {Compiling Pattern Matching},
3453+ year = {1985},
3454+ booktitle = {Functional Programming Languages and Computer Architecture},
3455+ pages = {368--381},
3456+ editor = {Jean-Pierre Jouannaud},
3457+ publisher = {Springer-Verlag},
3458+ author = {Lennart Augustsson}
3459+}
3460+
3461+@phdthesis{lena-thesis,
3462+ school = {Chalmers University of Technology, G\"{o}teborg},
3463+ title = {The implementation of {ALF} -- A Proof Editor based on {Martin-L\"{o}f}'s Monomorphic Type Theory with Explicit Substitutions},
3464+ year = {1994},
3465+ author = {Lena Magnusson}
3466+}
3467+
3468+@article{view-left,
3469+ journal = {Journal of Functional Programming},
3470+ number = {1},
3471+ volume = {14},
3472+ title = {The View From The Left},
3473+ year = {2004},
3474+ author = {Conor McBride and James McKinna},
3475+ pages = {69--111}
3476+}
3477+
3478+@inproceedings{not-a-number,
3479+ author = {Conor McBride and James McKinna},
3480+ title = {I am not a number, {I} am a free variable},
3481+ year = {2004},
3482+ booktitle = {Proceedings of the {ACM} {SIGPLAN} Haskell Workshop}
3483+}
3484+
3485+
3486+@misc{profiling,
3487+ title = {Time and Space Profiling for Non-Strict, Higher Order Functional Languages},
3488+ year = {1995},
3489+ author = {Patrick M. Sansom and Simon {Peyton Jones}}
3490+}
3491+
3492+@inbook{pattern-matching,
3493+ title = {The Implementation of Functional Programming Languages},
3494+ year = {1987},
3495+ booktitle = {The Implementation of Functional Programming Languages},
3496+ pages = {78--103},
3497+ editor = {Simon {Peyton Jones}},
3498+ chapter = {5},
3499+ publisher = {Prentice Hall},
3500+ author = {Philip Wadler},
3501+ crossref = {pj-imp}
3502+}
3503+
3504+@article{pe-problems,
3505+ author = {Jones, N. D.},
3506+ title = {Challenging problems in partial evaluation and mixed computation},
3507+ journal = {New Gen. Comput.},
3508+ volume = {6},
3509+ number = {2-3},
3510+ year = {1988},
3511+ issn = {0288-3635},
3512+ pages = {291--302},
3513+ doi = {http://dx.doi.org/10.1007/BF03037143},
3514+ publisher = {Ohmsha},
3515+ address = {Tokyo, Japan, Japan},
3516+ }
3517+
3518+@inproceedings{tag-elim,
3519+ title = {Tag Elimination -- or -- Type Specialisation is a Type Indexed Effect},
3520+ year = {2000},
3521+ booktitle = {Subtyping and Dependent Types in Programming, APPSEM Workshop},
3522+ author = {Walid Taha and Henning Makholm}
3523+}
3524+
3525+@inproceedings{extraction-coq,
3526+ title = {A New Extraction for {Coq}},
3527+ year = {2002},
3528+ booktitle = {Types for proofs and programs},
3529+ editor = {Herman Geuvers and Freek Wiedijk},
3530+ publisher = {Springer},
3531+ author = {Pierre Letouzey},
3532+ series = {LNCS}
3533+}
3534+
3535+@phdthesis{mcbride-snr-thesis,
3536+ school = {Queen's University of Belfast},
3537+ title = {Computer Aided Manipulation of Symbols},
3538+ year = {1970},
3539+ author = {Fred McBride}
3540+}
3541+
3542+@article{ho-strictness,
3543+ journal = {Science of Computer Programming},
3544+ volume = {7},
3545+ title = {Strictness analysis for higher-order functions},
3546+ year = {1986},
3547+ pages = {249--278},
3548+ author = { Geoffrey L. Burn and Chris Hankin and Samson Abramsky}
3549+}
3550+
3551+@phdthesis{mycroft-thesis,
3552+ school = {Dept Computer Science, University of Edinburgh},
3553+ title = {Abstract interpretation and optimising transformations for applicative programs},
3554+ year = {1981},
3555+ author = {A. Mycroft}
3556+}
3557+
3558+@inproceedings{bc-nested,
3559+ month = {September},
3560+ volume = {2152},
3561+ title = {Nested General Recursion and Partiality in Type Theory},
3562+ year = {2001},
3563+ booktitle = {Theorem Proving In Higher Order Logics: 14th International Conferences, TPHOLS 2001},
3564+ pages = {121--135},
3565+ publisher = {Springer--Verlag},
3566+ author = {Ana Bove and Venanzio Capretta},
3567+ series = {LNCS}
3568+}
3569+
3570+@techreport{bove-mutual,
3571+ month = {May},
3572+ title = {Mutual General Recursion in Type Theory},
3573+ year = {2002},
3574+ institution = {Department of Computing Science, Chalmers University of Technology},
3575+ author = {Ana Bove}
3576+}
3577+
3578+@article{berardi-pruning,
3579+ journal = {Journal of Logic and Computation},
3580+ number = {5},
3581+ volume = {6},
3582+ title = {Pruning Simply Typed Lambda Terms},
3583+ year = {1996},
3584+ pages = {663--681},
3585+ author = {Stefano Berardi}
3586+}
3587+
3588+@article{milner-tc,
3589+ journal = {Journal of Computer and System Science},
3590+ volume = {17},
3591+ title = {A Theory of Type Polymorphism in Programming},
3592+ year = {1978},
3593+ pages = {348--75},
3594+ author = {R. Milner}
3595+}
3596+
3597+@inproceedings{extt,
3598+ title = {Inductive Families Need Not Store Their Indices},
3599+ year = {2004},
3600+ booktitle = {Types for Proofs and Programs 2003},
3601+ author = {Edwin Brady and Conor McBride and James McKinna},
3602+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
3603+ series = {Lecture Notes in Computer Science},
3604+ publisher = {Springer},
3605+ volume = {3085},
3606+ pages = {115--129}
3607+}
3608+
3609+@book{luo94,
3610+ title = {Computation and Reasoning -- A Type Theory for Computer Science},
3611+ year = {1994},
3612+ publisher = {OUP},
3613+ author = {Zhaohui Luo},
3614+ series = {Intl. Series of Monographs on Comp. Sci.}
3615+}
3616+
3617+@article{backus78,
3618+ journal = {Communications of the {ACM}},
3619+ month = {August},
3620+ volume = {21},
3621+ title = {Can Programming Be Liberated From the {Von Neumann} Style?},
3622+ year = {1978},
3623+ pages = {280--294},
3624+ author = {John Backus}
3625+}
3626+
3627+@misc{henk,
3628+ month = {May},
3629+ title = {Henk: A Typed Intermediate Language},
3630+ year = {1997},
3631+ author = {Simon {Peyton Jones} and Erik Meijer}
3632+}
3633+
3634+@article{thunks,
3635+ journal = {Journal of Functional Programming},
3636+ number = {3},
3637+ month = {May},
3638+ volume = {7},
3639+ title = {Thunks and the $\lambda$-calculus},
3640+ year = {1997},
3641+ pages = {303--319},
3642+ author = {John Hatcliff and Olivier Danvy}
3643+}
3644+
3645+@inproceedings{grin-project,
3646+ author = "Urban Boquist and Thomas Johnsson",
3647+ title = "The {GRIN} Project: A Highly Optimising Back End for Lazy Functional Languages",
3648+ booktitle = "Implementation of Functional Languages",
3649+ pages = "58--84",
3650+ year = "1996",
3651+ url = "citeseer.ist.psu.edu/boquist96grin.html" }
3652+
3653+@misc{boehm-gc,
3654+ nothowpublished = {\url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}},
3655+ title = {A garbage collector for {C} and {C++}},
3656+ year = {2001},
3657+ author = {Hans-J. Boehm and Alan J. Demers and {Xerox Corporation Silicon Graphic} and {Hewlett-Packard Company}}
3658+}
3659+
3660+@misc{art-interpreter,
3661+ month = {May},
3662+ title = {The Art of the Interpreter or, the Modularity Complex (Parts Zero, One, and Two)},
3663+ year = {1978},
3664+ author = {Guy Lewis {Steele, Jr.} and Gerald Jay Sussman},
3665+ note = {MIT AI Lab. AI Lab Memo AIM-453}
3666+}
3667+
3668+@inproceedings{gimenez,
3669+ title = {Codifying Guarded Definitions With Recursive Schemes},
3670+ year = {1994},
3671+ booktitle = {Proceedings of TYPES 1994},
3672+ pages = {39--59},
3673+ author = {Eduardo Gim\'{e}nez}
3674+}
3675+
3676+@manual{ghc-manual,
3677+ title = {The Glasgow Haskell Compiler User's Guide, Version 6.0},
3678+ year = {2003},
3679+ author = {The {GHC Team}}
3680+}
3681+
3682+@article{rbtree,
3683+ journal = {Journal of Functional Programming},
3684+ number = {4},
3685+ month = {May},
3686+ volume = {9},
3687+ title = {Red-Black Trees In A Functional Setting},
3688+ year = {1999},
3689+ pages = {471--477},
3690+ author = {Chris Okasaki}
3691+}
3692+
3693+@inproceedings{dt-data,
3694+author = "Hongwei Xi",
3695+title = {{Dependently Typed Data Structures}},
3696+booktitle = "Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL '99)",
3697+year = 1999,
3698+month = "September",
3699+pages = "17--32",
3700+address = "Paris",
3701+}
3702+
3703+@misc{krivine,
3704+ title = {On the Correctness and Efficiency of the {Krivine} Machine},
3705+ year = {2003},
3706+ month = {October},
3707+ author = {Mitchell Wand and Daniel P. Friedman},
3708+ howpublished = {Submitted for publication}
3709+ }
3710+
3711+@inproceedings{nbe-filinski,
3712+ title = {Normalization by Evaluation for the Computational Lambda-Calculus},
3713+ year = {2001},
3714+ month = {May},
3715+ booktitle = {Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001},
3716+ author = {Andrzej Filinski},
3717+ pages = {151--165},
3718+ publisher = {Springer-Verlag},
3719+ series = {LNCS},
3720+ volume = {2044}
3721+}
3722+
3723+@inproceedings{filinski-nbesem,
3724+ title = {A semantic account of type-directed partial evaluation},
3725+ year = {1999},
3726+ author = {Andrzej Filinski},
3727+ editor = {G. Nadathur},
3728+ booktitle = {International Conference on Principles and Practice of Declarative Programming},
3729+ volume = {1702},
3730+ series = {LNCS},
3731+ pages = {378--395},
3732+ publisher = {Springer-Verlag}
3733+}
3734+
3735+@article{secd,
3736+ title = {The mechanical evaluation of expressions},
3737+ author = {P.J. Landin},
3738+ year = {1964},
3739+ journal = {Computer Journal},
3740+ volume = {6},
3741+ pages = {308--320}
3742+}
3743+
3744+@misc{lispkit,
3745+ title = {The {LispKit} Manual},
3746+ author = {Peter Henderson and Geraint Jones and Simon Jones},
3747+ year = {1982},
3748+ howpublished = {Oxford University Computing Laboratory}
3749+}
3750+
3751+@inproceedings{wells-undecidable,
3752+ title = {Typability and Type Checking in the Second-order $\lambda$-calculus are equivalent and undecidable},
3753+ author = {J. Wells},
3754+ year = {1994},
3755+ month = {July},
3756+ booktitle = {Proc. 9th Ann. {IEEE} Symp. Logic Comput. Sci.}
3757+}
3758+
3759+@misc{patguards,
3760+ title = {Pattern Guards and Transformational Patterns},
3761+ author = {Martin Erwig and Simon {Peyton Jones}},
3762+ year = {2000},
3763+ howpublished = {Haskell Workshop}
3764+}
3765+
3766+@misc{alfa-manual,
3767+ title = {Alfa Users' Guide},
3768+ author = {Thomas Hallgren},
3769+ year = {2001},
3770+ howpublished = {Available from \verb+http://www.cs.chalmers.se/~hallgren/Alfa/+}
3771+}
3772+
3773+@inproceedings{nofib,
3774+ title = {The nofib Benchmark Suite of {Haskell} Programs},
3775+ author = {Will Partain},
3776+ year = {1992},
3777+ booktitle = {Functional Programming},
3778+ editor = {J. Launchbury and P.L. Sansom},
3779+ series = {Workshops in Computing},
3780+ publisher = {Springer Verlag}
3781+}
3782+
3783+@article{shape,
3784+ title = {Shape in Computing},
3785+ author = {Barry Jay},
3786+ journal = "{{ACM}} Computing Surveys",
3787+ year = "1996",
3788+ volume = "28",
3789+ number = "2",
3790+ pages = "355--357",
3791+}
3792+
3793+@misc{ffi,
3794+ title = {The {Haskell 98} Foreign Function Interface 1.0: An Addendum to the {Haskell 98} Report},
3795+ editor = {Manuel Chakravarty},
3796+ key = {FFI},
3797+ year = {2002},
3798+ month = {December},
3799+ howpublished = {Available from \verb+http://www.haskell.org/+}
3800+}
3801+
3802+@misc{perlxs,
3803+ title = {Perl {XS} Reference Manual},
3804+ author = {Dean Roehrich and {The Perl Porters}},
3805+ year = {1996},
3806+ howpublished = {\verb+http://www.perldoc.com/perl5.6/pod/perlxs.html+}
3807+}
3808+
3809+@misc{swig,
3810+ title = {{SWIG} : An Easy to Use Tool for Integrating Scripting Languages with {C} and {C++}},
3811+ author = {David M. Beazley},
3812+ year = {1996},
3813+ howpublished = {\verb+http://www.swig.org/papers/Tcl96/tcl96.html+}
3814+}
3815+
3816+@inproceedings{types-prog,
3817+ title = {Type Systems for Programming Languages},
3818+ booktitle = {Handbook of Theoretical Computer Science},
3819+ author = {John C. Mitchell},
3820+ pages = {365--458},
3821+ year = {1990},
3822+ crossref = {htcs}
3823+}
3824+
3825+@book{htcs,
3826+ title = {Handbook of Theoretical Computer Science},
3827+ editor = {J. van Leeuwen},
3828+ publisher = {Elsevier Science},
3829+ year = {1990}
3830+}
3831+
3832+@misc{r5rs,
3833+ title = {Revised$^5$ Report on the Algorithmic Language Scheme},
3834+ author = {Richard Kelsey and William Clinger and Jonathan Rees},
3835+ year = {1998},
3836+ month = {February},
3837+ howpublished = {Available from \verb+http://www.schemers.org/+}
3838+ }
3839+
3840+@misc{gmail-outage,
3841+ title = {Update on today's {Gmail} Outage},
3842+ author = {{Official Gmail Blog}},
3843+ howpublished = {\url{http://gmailblog.blogspot.com/2009/02/update-on-todays-gmail-outage.html}},
3844+ note = {Retrieved 26th February 2009},
3845+ year = 2009
3846+}
tutorial/macros.ltxnew file+1062
@@ -0,0 +1,1062 @@
1+%\usepackage{amstex}
2+\usepackage{amssymb}
3+\usepackage{latexsym}
4+\usepackage{eepic}
5+
6+
7+%%%%%%%%% INFERENCE RULES
8+
9+\newlength{\rulevgap}
10+\setlength{\rulevgap}{0.05in}
11+\newlength{\ruleheight}
12+\newlength{\ruledepth}
13+\newsavebox{\rulebox}
14+\newlength{\GapLength}
15+\newcommand{\gap}[1]{\settowidth{\GapLength}{#1} \hspace*{\GapLength}}
16+\newcommand{\dotstep}[2]{\begin{tabular}[b]{@{}c@{}}
17+ #1\\$\vdots$\\#2
18+ \end{tabular}}
19+\newlength{\fracwid}
20+\newcommand{\dotfrac}[2]{\settowidth{\fracwid}{$\frac{#1}{#2}$}
21+ \addtolength{\fracwid}{0.1in}
22+ \begin{tabular}[b]{@{}c@{}}
23+ $#1$\\
24+ \parbox[c][0.02in][t]{\fracwid}{\dotfill} \\
25+ $#2$\\
26+ \end{tabular}}
27+\newcommand{\Rule}[2]{\savebox{\rulebox}[\width][b] %
28+ {\( \frac{\raisebox{0in} {\( #1 \)}} %
29+ {\raisebox{-0.03in}{\( #2 \)}} \)} %
30+ \settoheight{\ruleheight}{\usebox{\rulebox}} %
31+ \addtolength{\ruleheight}{\rulevgap} %
32+ \settodepth{\ruledepth}{\usebox{\rulebox}} %
33+ \addtolength{\ruledepth}{\rulevgap} %
34+ \raisebox{0in}[\ruleheight][\ruledepth] %
35+ {\usebox{\rulebox}}}
36+\newcommand{\Case}[2]{\savebox{\rulebox}[\width][b] %
37+ {\( \dotfrac{\raisebox{0in} {\( #1 \)}} %
38+ {\raisebox{-0.03in}{\( #2 \)}} \)} %
39+ \settoheight{\ruleheight}{\usebox{\rulebox}} %
40+ \addtolength{\ruleheight}{\rulevgap} %
41+ \settodepth{\ruledepth}{\usebox{\rulebox}} %
42+ \addtolength{\ruledepth}{\rulevgap} %
43+ \raisebox{0in}[\ruleheight][\ruledepth] %
44+ {\usebox{\rulebox}}}
45+\newcommand{\Axiom}[1]{\savebox{\rulebox}[\width][b] %
46+ {$\frac{}{\raisebox{-0.03in}{$#1$}}$} %
47+ \settoheight{\ruleheight}{\usebox{\rulebox}} %
48+ \addtolength{\ruleheight}{\rulevgap} %
49+ \settodepth{\ruledepth}{\usebox{\rulebox}} %
50+ \addtolength{\ruledepth}{\rulevgap} %
51+ \raisebox{0in}[\ruleheight][\ruledepth] %
52+ {\usebox{\rulebox}}}
53+\newcommand{\RuleSide}[3]{\gap{$#2$} \hspace*{0.1in} %
54+ \Rule{#1}{#3} %
55+ \hspace*{0.1in}$#2$}
56+\newcommand{\AxiomSide}[2]{\gap{$#1$} \hspace*{0.1in} %
57+ \Axiom{#2} %
58+ \hspace*{0.1in}$#1$}
59+\newcommand{\RULE}[1]{\textbf{#1}}
60+\newcommand{\hg}{\hspace{0.2in}}
61+
62+\newcommand{\ProofState}
63+ [2]{\parbox{10cm}{\AR{\hg\AR{#1}\\\Axiom{\hg#2\hg}}}}
64+
65+%%%%%%%%%%%% TRISTUFF
66+
67+\newcommand{\btr}{
68+\setlength{\unitlength}{0.0005in}
69+\begin{picture}(69,180)(0,12)
70+\blacken\path(57,192)(57,12)(12,102)
71+ (57,192)(57,192)
72+\path(57,192)(57,12)(12,102)
73+ (57,192)(57,192)
74+\end{picture}
75+}
76+
77+\newcommand{\btl}{
78+\setlength{\unitlength}{0.0005in}
79+\begin{picture}(69,180)(0,12)
80+\blacken\path(12,192)(12,12)(57,102)
81+ (12,192)(12,192)
82+\path(12,192)(12,12)(57,102)
83+ (12,192)(12,192)
84+\end{picture}
85+}
86+
87+\newcommand{\wtr}{
88+\setlength{\unitlength}{0.0005in}
89+\begin{picture}(69,180)(0,12)
90+%\blacken\path(57,192)(57,12)(12,102)
91+% (57,192)(57,192)
92+\path(57,192)(57,12)(12,102)
93+ (57,192)(57,192)
94+\end{picture}
95+}
96+
97+\newcommand{\wtl}{
98+\setlength{\unitlength}{0.0005in}
99+\begin{picture}(69,180)(0,12)
100+%\blacken\path(12,192)(12,12)(57,102)
101+% (12,192)(12,192)
102+\path(12,192)(12,12)(57,102)
103+ (12,192)(12,192)
104+\end{picture}
105+}
106+
107+
108+
109+%%%%%%%%%%%% FONTS
110+
111+\newcommand{\TC}[1]{\mathsf{#1}}
112+\newcommand{\DC}[1]{\mathsf{#1}}
113+\newcommand{\VV}[1]{\mathit{#1}}
114+\newcommand{\FN}[1]{\mathbf{#1}}
115+\newcommand{\HFN}[1]{\mathtt{#1}}
116+\newcommand{\RW}[1]{\underline{\textrm{#1}}}
117+\newcommand{\MO}[1]{\mbox{\textsc{#1}}}
118+
119+\newcommand{\HF}[1]{\mathtt{#1}}
120+
121+\newcommand{\MV}[1]{\nhole\mathit{#1}}
122+\newcommand{\Lang}[1]{\mathsf{#1}}
123+\newcommand{\Name}[1]{\mathit{#1}}
124+
125+\newcommand{\demph}[1]{\textbf{#1}}
126+\newcommand{\remph}[1]{\emph{#1}}
127+
128+%%%% Keywords for meta operations
129+\newcommand{\IF}{\;\RW{if}\;\;}
130+\newcommand{\THEN}{\RW{then}}
131+\newcommand{\ELSE}{\RW{else}}
132+\newcommand{\AND}{\RW{and}}
133+\newcommand{\Otherwise}{\RW{otherwise}}
134+\newcommand{\Do}{\RW{do}}
135+\newcommand{\Return}{\RW{return}}
136+
137+\newcommand{\CASE}{\RW{case}}
138+\newcommand{\LET}{\RW{let}}
139+\newcommand{\IN}{\RW{in}}
140+\newcommand{\of}{\RW{of}}
141+
142+\newcommand{\CLASS}{\mathtt{class}}
143+\newcommand{\INSTANCE}{\mathtt{instance}}
144+
145+%%%%%%%%%%%% GROUPING
146+
147+\newcommand{\G}{
148+\setlength{\unitlength}{1pt}
149+\begin{picture}(4,10)(0,0)
150+\path(2,10)(2,-10)
151+\end{picture}
152+}
153+
154+\newcommand{\E}{
155+\setlength{\unitlength}{1pt}
156+\begin{picture}(4,10)(0,0)
157+\path(2,10)(2,-2)(4,-2)
158+\end{picture}
159+}
160+
161+%\newcommand{\C}{
162+%\setlength{\unitlength}{1pt}
163+%\begin{picture}(4,10)(0,0)
164+%\path(4,8)(2,8)(2,-2)(4,-2)
165+%\end{picture}
166+%}
167+
168+\newcommand{\M}{
169+\setlength{\unitlength}{1pt}
170+\begin{picture}(4,10)(0,0)
171+\path(2,10)(2,-2)(6,-2)
172+\end{picture}
173+}
174+
175+\newcommand{\F}{
176+\setlength{\unitlength}{1pt}
177+\begin{picture}(4,10)(0,0)
178+\path(4,8)(2,8)(2,-6)
179+\end{picture}
180+}
181+
182+\newcommand{\K}{
183+\setlength{\unitlength}{1pt}
184+\begin{picture}(4,10)(0,0)
185+\path(0,8)(4,8)
186+\end{picture}
187+}
188+
189+\newcommand{\J}{
190+\setlength{\unitlength}{1pt}
191+\begin{picture}(4,10)(0,0)
192+\path(0,-2)(4,-2)
193+\end{picture}
194+}
195+
196+\newcommand{\W}{
197+\setlength{\unitlength}{1pt}
198+\begin{picture}(4,10)(0,0)
199+\end{picture}
200+}
201+
202+
203+
204+%%%%%%%%%%%% GUBBINS
205+
206+\newcommand{\mathskip}{\medskip}
207+
208+\newcommand{\fbx}[1]{\fbox{$#1$}}
209+\newcommand{\stk}[1]{\begin{array}{c}#1\end{array}}
210+%\newcommand{\DM}[1]{\hg\mbox{$#1$}}
211+\newcommand{\DM}[1]{\mathskip\par\(#1\)\mathskip}
212+\newcommand{\mbx}[1]{\mathskip\par\noindent\(#1\)\mathskip}
213+\newcommand{\AR}[1]{\begin{array}[t]{@{}l}#1\end{array}}
214+\newcommand{\ARt}[1]{\begin{array}[t]{@{}l@{}cl}#1\end{array}}
215+\newcommand{\ARc}[1]{\begin{array}{@{}l}#1\end{array}}
216+\newcommand{\ARd}[1]{\begin{array}[t]{cl}#1\end{array}}
217+\newcommand{\DAR}[1]{\begin{array}{ll}\hg & #1\end{array}}
218+\newcommand{\Dor}{\\ \hg\mid & }
219+\newcommand{\EA}[1]{\begin{array}[t]{r@{}c@{}l}#1\end{array}}
220+\newcommand{\A}{@{\:}c}
221+%\newcommand{\R}{@{\:}r}
222+\newcommand{\CA}{c}
223+\newcommand{\LA}{l}
224+\newcommand{\PAc}[2]{\begin{array}{l#1@{}r@{}l}#2\end{array}}
225+\newcommand{\PA}[2]{\begin{array}[t]{l@{\:}l#1@{}r@{\:}l}#2\end{array}}
226+\newcommand{\DTREE}[3]{\begin{array}[t]{l#1@{}r@{\:}l#2}#3\end{array}}
227+\newcommand{\IDTREE}[2]{%
228+ \begin{array}[t]{l@{\:}c@{\:}l@{\:}r@{\:}l#1}#2\end{array}}
229+\newcommand{\IA}[2]
230+ {\begin{array}[t]{l@{\:}r@{\:}c@{\:}l@{\:}#1@{\:}r@{\:}l}#2\end{array}}
231+\newcommand{\IAc}[2]
232+ {\begin{array}[c]{r@{\:}c@{\:}l@{\:}#1@{}r@{}l}#2\end{array}}
233+\newcommand{\CS}[1]{\left\lfloor\begin{array}{@{}l}#1\end{array}\right.}
234+\newcommand{\BY}[3]{\multicolumn{2}{l}{\;\RW{by}\; #1} \\ %
235+ \multicolumn{#2}{l}{\CS{#3}} }
236+\newcommand{\WITH}[3]{\multicolumn{2}{l}{\;\RW{with}\; #1} \\ %
237+ \multicolumn{#2}{l}{\CS{#3}} }
238+\newcommand{\WithBy}{\RW{with-by}}
239+\newcommand{\Wb}[1]{\WithBy& #1}
240+\newcommand{\By}[1]{\multicolumn{2}{l}{\Leftarrow #1}}
241+\newcommand{\andby}{\Leftarrow}
242+\newcommand{\MyWith}[1]{\multicolumn{2}{l}{|\;#1}}
243+\newcommand{\Byr}[1]{\;\RW{by}\; #1}
244+
245+\newcommand{\Bar}{|}
246+\newcommand{\Bart}{\settowidth{\GapLength}{$\Bar$}%
247+ \raisebox{6pt}[0pt][0pt]{$\Bar$}%
248+ \hspace*{-1\GapLength}%
249+ \Bar}
250+\newcommand{\With}[1]{\Bar & #1}
251+\newcommand{\Witt}[1]{\Bart & #1}
252+
253+\newcommand{\B}{@{\:}r@{\:}c}
254+\newcommand{\Ret}[1]{\multicolumn{2}{l}{\cq #1}}
255+\newcommand{\MRet}[2]{\multicolumn{#1}{l}{\cq #2}}
256+\newcommand{\HRet}[1]{\multicolumn{2}{l}{\hq #1}}
257+\newcommand{\MHRet}[2]{\multicolumn{#1}{l}{\hq #2}}
258+\newcommand{\IRet}[1]{\multicolumn{2}{l}{\iq #1}}
259+\newcommand{\IMRet}[2]{\multicolumn{#1}{l}{\iq #2}}
260+\newcommand{\MoRet}[1]{\multicolumn{2}{l}{\mq #1}}
261+\newcommand{\MMoRet}[2]{\multicolumn{#1}{l}{\mq #2}}
262+\newcommand{\Data}{\RW{data}}
263+\newcommand{\Codata}{\RW{codata}}
264+\newcommand{\Where}{\RW{where}}
265+\newcommand{\Let}{\RW{let}}
266+\newcommand{\Fact}{\RW{fact}}
267+\newcommand{\Rec}[1]{#1\textbf{-Rec}}
268+\newcommand{\Memo}[1]{#1\textbf{-Memo}}
269+\newcommand{\Elim}[1]{#1\textbf{-Elim}}
270+\newcommand{\Cases}[1]{#1\textbf{-Case}}
271+\newcommand{\View}[1]{#1\textbf{-View}}
272+\newcommand{\As}[2]{#1 \:\RW{as}\: #2}
273+\newcommand{\nhole}{\Box}
274+\newcommand{\turq}{\:\vdash_?\:}
275+\newcommand{\split}{\;\lhd\;}
276+\newcommand{\CType}[2]{\{#1 \split\; #2\}}
277+\newcommand{\CC}[2]{(#1)\:#2}
278+\newcommand{\UP}[2]{#1 | \{#2\}}
279+\newcommand{\Ured}{\:\Downarrow\:}
280+\newcommand{\gdd}{\prec}
281+\newcommand{\HC}[1]{\left<#1\right>}
282+\newcommand{\HT}[2]{\left<#1 \hab #2\right>}
283+
284+\newcommand{\view}{\RW{view}}
285+\newcommand{\ecase}{\RW{case}}
286+\newcommand{\rec}{\RW{rec}}
287+
288+\newcommand{\If}{\mathsf{if}}
289+\newcommand{\Then}{\mathsf{then}}
290+\newcommand{\Else}{\mathsf{else}}
291+\newcommand{\elim}{\RW{elim}}
292+
293+\newcommand{\Payload}{\mathsf{type}}
294+\newcommand{\Any}{\mathsf{Some}}
295+
296+\newcommand{\lbl}[2]{\langle #1 \Hab #2 \rangle}
297+\newcommand{\call}[2]{\RW{call}\:\langle#1\rangle\:#2}
298+\newcommand{\return}[1]{\RW{return}\:#1}
299+
300+\newcommand{\Remark}[1]{\noindent\textbf{Remark:} #1}
301+
302+\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}
303+
304+\newcommand{\useverbtb}[1]{\begin{tiny}\BUseVerbatim{#1}\end{tiny}}
305+\newcommand{\useverb}[1]{\BUseVerbatim{#1}}
306+\newcommand{\useverbs}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
307+\newcommand{\useverbb}[1]{\begin{small}\BUseVerbatim{#1}\end{small}}
308+
309+\newcommand{\diagfig}[3]{\begin{figure}[h]\begin{center}\includegraphics[width=#1]{#2}\end{center}
310+\caption{#3}\label{#2}\end{figure}}
311+\newcommand{\codefig}[2]{\begin{figure}[h]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
312+\newcommand{\codefigs}[2]{\begin{figure}[h]\useverbs{#1}\caption{#2}\label{#1}\end{figure}}
313+\newcommand{\codefigt}[2]{\begin{figure}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
314+\newcommand{\codefigb}[2]{\begin{figure}[b]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
315+\newcommand{\codefigtc}[2]{\begin{figure*}[t]\useverb{#1}\caption{#2}\label{#1}\end{figure}}
316+\newcommand{\diagfigtc}[3]{\begin{figure*}[t]\begin{center}\includegraphics[width=#1]{#2}\end{center}
317+\caption{#3}\label{#2}\end{figure*}}
318+
319+\newcommand{\FIG}[3]{\begin{figure}[h]\DM{#1}\caption{#2}\label{#3}\end{figure}}
320+\newcommand{\FFIG}[3]{\begin{figure}\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
321+\newcommand{\FFIGB}[3]{\begin{figure}[b]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
322+\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}
323+\newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}
324+\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}
325+\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
326+
327+\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}
328+\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}
329+
330+\newcommand{\RESFIG}[3]{
331+\TFIG{|l|c|c|c|c|c|c|c|c|}{
332+\hline
333+ & \multicolumn{4}{c|}{\Naive{} compilation} &
334+ \multicolumn{4}{|c|}{Optimised compilation} \\
335+\cline{2-9}
336+\raisebox{1.5ex}[0pt]{Program} & Instrs & Thunks & Cells &
337+Accesses & Instructions & Thunks & Cells & Accesses \\
338+%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
339+\hline
340+#1
341+\hline
342+}{#2}{#3}}
343+
344+\newcommand{\NEWRESFIG}[3]{
345+\TFIG{|l|l|c|c|c|c|}{
346+\hline
347+% & \multicolumn{4}{c|}{\Naive{} compilation} &
348+% \multicolumn{4}{|c|}{Optimised compilation} \\
349+%\cline{2-9}
350+Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
351+%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
352+\hline
353+#1
354+}{#2}{#3}}
355+
356+\newcommand{\NEWRESFIGTC}[3]{
357+\TFIGTC{|l|l|c|c|c|c|}{
358+\hline
359+% & \multicolumn{4}{c|}{\Naive{} compilation} &
360+% \multicolumn{4}{|c|}{Optimised compilation} \\
361+%\cline{2-9}
362+Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
363+%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
364+\hline
365+#1
366+}{#2}{#3}}
367+
368+\newcommand{\RESLINE}[9]{
369+& \Naive{} & #2 & #3 & #5 & #4 \\
370+#1
371+& Optimised & #6 & #7 & #9 & #8 \\
372+}
373+\newcommand{\RESCHANGE}[4]{
374+& Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\
375+\hline
376+}
377+\newcommand{\RESCHANGEa}[5]{
378+#5 & Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\
379+\hline
380+}
381+
382+%%%%%%%%%%%% PUNCTUATION
383+
384+\newcommand{\pad}[2]{#1#2#1}
385+
386+\newcommand{\hab}{\pad{\,}{:}}
387+\newcommand{\Hab}{\pad{\;}{:}}
388+\newcommand{\HHab}{\pad{\;}{::}}
389+
390+%%%%%%%%%%%% TYPE
391+
392+\newcommand{\Type}{\mbox{\texttt{\#}}} %\star}
393+
394+
395+%%%%%%%%%%%%% ARROWS
396+
397+\newcommand{\To}{\pad{\:}{\rightarrow}}
398+\newcommand{\Gets}{\leftarrow}
399+%\newcommand{\car}{\vartriangleright}
400+
401+%%%%%%%%%%%%% QUANTIFIERS
402+
403+\newcommand{\lam}[2]{\lambda#1\pad{\!}{:}#2}
404+\newcommand{\fbind}[3]{(#1\Hab#2)\to#3}
405+\newcommand{\all}[2]{\forall#1\pad{\!}{:}#2}
406+\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}
407+\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}
408+\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}
409+\newcommand{\remall}[2]{\forall\{#1\pad{\!}{:}#2\}}
410+\newcommand{\allpi}[2]{\Pi#1\pad{\!}{:}#2}
411+\newcommand{\ali}[2]{\forall#1|#2}
412+\newcommand{\exi}[2]{\exists#1\pad{\!}{:}#2}
413+\newcommand{\wit}[2]{\ang{#1,#2}}
414+\newcommand{\X}{\times}
415+\newcommand{\sig}[2]{\Sigma#1\pad{\!}{:}#2}
416+
417+\newcommand{\SC}{.\:}
418+
419+\newcommand{\letbind}[3]{\mathsf{let}\:#1{:}#2\:=\:#3\:\mathsf{in}}
420+\newcommand{\ifthen}[3]{\mathsf{if}\:#1\:\mathsf{then}\:#2\:\mathsf{else}\:#3}
421+
422+%%%%%%%%%%%%% EQUALITIES
423+
424+\newcommand{\cq}{\pad{\:}{\mapsto}}
425+\newcommand{\xq}{\pad{}{\doteq}}
426+\newcommand{\pq}{\pad{\:}{=}}
427+\newcommand{\dq}{\pad{\:}{:=}}
428+\newcommand{\iq}{\pad{\:}{\leadsto}}
429+\newcommand{\mq}{\Longrightarrow}
430+\newcommand{\retq}{\Rightarrow}
431+\newcommand{\hq}{\pad{\:}{=}}
432+\newcommand{\defq}{\mapsto}
433+
434+\newcommand{\refl}{\TC{refl}}
435+
436+
437+
438+
439+%%%%%%%%%%%%% CATSTUFF
440+
441+\newlength{\Lwibrs}
442+\newlength{\Lwobrs}
443+\newsavebox{\Bwibrs}
444+\newsavebox{\Bwobrs}
445+\newcommand{\Db}[5]{%
446+ \savebox{\Bwobrs}[\width][b]{$#5$}%
447+ \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right#3$}%
448+ \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
449+ \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
450+ \addtolength{\Lwibrs}{-\Lwobrs}%
451+ \left#1\pad{\hspace*{-0.25\Lwibrs}}{\usebox{\Bwibrs}}\right#4}
452+\newcommand{\LDb}[3]{%
453+ \savebox{\Bwobrs}[\width][b]{$#3$}%
454+ \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right.$}%
455+ \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
456+ \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
457+ \addtolength{\Lwibrs}{-\Lwobrs}%
458+ \left#1\hspace*{-0.4\Lwibrs}\usebox{\Bwibrs}\right.}
459+\newcommand{\RDb}[3]{%
460+ \savebox{\Bwobrs}[\width][b]{$#3$}%
461+ \savebox{\Bwibrs}[\width][b]{$\left.\usebox{\Bwobrs}\right#1$}%
462+ \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
463+ \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
464+ \addtolength{\Lwibrs}{-\Lwobrs}%
465+ \left.\usebox{\Bwibrs}\hspace*{-0.4\Lwibrs}\right#2}
466+\newcommand{\Sc}{\Db{[}{[}{]}{]}}
467+\newcommand{\Mo}{\Db{|}{>}{<}{|}}
468+\newcommand{\MoL}{\LDb{|}{>}}
469+\newcommand{\MoR}{\RDb{<}{|}}
470+
471+\newcommand{\car}{\mbox{$-\!\triangleright$}}
472+\newcommand{\io}[1]{\iota_{#1}}
473+\newcommand{\cc}{\diamond}
474+
475+
476+%%%%%%%%%%%%% FNS
477+
478+\newcommand{\Wk}{\Uparrow}
479+
480+%%%%%%%%%%%%% Transformation
481+
482+\newcommand{\Transform}[3]{\textsc{Trans}\:_{\Name{#1}}
483+ \interp{#2}\:\mq\:#3}
484+%\:[\:#2\:\Longrightarrow\:#3\:]}
485+\newcommand{\Morphism}[2]{\textsc{Morphism}\:#1\:\Longrightarrow\:#2}
486+\newcommand{\MI}[1]{\begin{array}{ll} #1 \end{array}\\}
487+\newcommand{\MorphItem}[2]{& #1 \:\Longrightarrow\: #2}
488+
489+%%%%%%%%%%%%% Stuff
490+
491+% Motive and methods
492+
493+\newcommand{\motive}{\vP}
494+\newcommand{\meth}[1]{\vm_{#1}}
495+
496+% Tuples
497+\newcommand{\tuple}[1]{\langle#1\rangle}
498+\newcommand{\Tuple}[1]{\mathsf{Tuple}}
499+\newcommand{\proj}{\mathsf{proj}}
500+\newcommand{\app}{\mathrm{+\!+}}
501+
502+% Commenting out
503+\newcommand{\ig}[1]{[#1]}
504+\newcommand{\rem}[1]{\{\!#1\!\}}
505+\newcommand{\igc}[1]{[#1]}
506+\newcommand{\remc}[1]{\{\!#1\!\}}
507+
508+
509+\newcommand{\ind}{\hspace*{0.1cm}}
510+
511+% Content free type
512+\newcommand{\CF}{\TC{CF}}
513+\newcommand{\cf}{\DC{cf}}
514+
515+% Error token
516+\newcommand{\error}{\DC{error}}
517+\newcommand{\fail}{\perp}
518+
519+% Constructor stripping
520+\newcommand{\conarg}[2]{#1!#2}
521+
522+\newcommand{\Vect}{\TC{Vect}}
523+\newcommand{\VectM}{\TC{Vect^-}}
524+\newcommand{\Vnil}{\DC{\epsilon}}
525+\newcommand{\Vcons}{\DC{::}}
526+
527+\newcommand{\Vsnoc}{\DC{::}}
528+
529+\newcommand{\VnilM}{\DC{\epsilon^-}}
530+\newcommand{\VconsM}{\DC{::^-}}
531+
532+\newcommand{\Vnilcase}{\VV{vNilCase}}
533+\newcommand{\Vconscase}{\VV{vConsCase}}
534+
535+\newcommand{\DSigma}{\TC{Sigma}}
536+\newcommand{\Exists}{\DC{Exists}}
537+
538+\newcommand{\ListPair}[2]{\sig{#1}{\List\:\vA}.#2 = \FN{length}\:#1}
539+\newcommand{\lpNilDef}{\lpNil{\FN{refl}\:\Z}}
540+\newcommand{\lpNil}[1]{(\nil\:\vA,#1)}
541+\newcommand{\lpConsDef}[3]{\lpCons{#1}{(\FN{fst\:#2})}{\FN{resp}\:(\FN{snd}\:#2)}}
542+\newcommand{\lpCons}[3]{(\cons\:#1\:#2,#3)}
543+\newcommand{\lp}[2]{(#1, #2)}
544+
545+\newcommand{\VnilTop}{\DC{vNil}^\ast}
546+\newcommand{\VconsTop}{\DC{vCons}^\ast}
547+
548+\newcommand{\VnilBot}{\DC{\epsilon}^-}
549+\newcommand{\VconsBot}{\DC{::}^-}
550+
551+\newcommand{\VectTop}{\TC{Vect}^\ast}
552+\newcommand{\VectBot}{\TC{Vect}^-}
553+
554+\newcommand{\VectDrop}{\FN{vectDropIdx}}
555+\newcommand{\VectRebuild}{\FN{vectRebuild}}
556+
557+\newcommand{\Prop}{\TC{Prop}}
558+\newcommand{\Set}{\TC{Set}}
559+\newcommand{\CoqType}{\TC{Type}}
560+
561+\newcommand{\List}{\TC{List}}
562+\newcommand{\nil}{\DC{nil}}
563+\newcommand{\cons}{\DC{cons}}
564+
565+\newcommand{\Zip}{\TC{Tsil}}
566+\newcommand{\zip}{\FN{tsil}}
567+\newcommand{\zipcons}{\FN{tsilcons}}
568+\newcommand{\snoc}{\DC{Snoc}}
569+\newcommand{\lin}{\DC{Empty}}
570+
571+\newcommand{\BigInt}{\TC{BigInt}}
572+\newcommand{\False}{\TC{False}}
573+\newcommand{\Unit}{\TC{Unit}}
574+\newcommand{\UnitI}{\DC{unit}}
575+
576+\newcommand{\genType}{\TC{X}}
577+\newcommand{\genIndicesDec}{\tb\Hab\tB}
578+\newcommand{\genIndices}{\tb}
579+\newcommand{\genConArgsDec}[1]{\vec{\VV{a_#1}}\Hab\vec{\VV{A_#1}}}
580+\newcommand{\genConArgs}[1]{\vec{\VV{a_#1}}}
581+\newcommand{\genConIndicesDec}[1]{\vec{\VV{b_#1}}\Hab\vec{\VV{B_#1}}}
582+\newcommand{\genConIndices}[1]{\vec{\VV{b_#1}}}
583+\newcommand{\genCon}[1]{\DC{x}_#1}
584+
585+\newcommand{\genTypeTop}{\TC{X^\ast}}
586+\newcommand{\genTypeBot}{\TC{X^-}}
587+
588+\newcommand{\genTypeDrop}{\FN{XDropIdx}}
589+\newcommand{\genTypeRebuild}{\FN{XRebuild}}
590+
591+\newcommand{\HTerm}{\texttt{Term}}
592+\newcommand{\Term}{\TC{Term}}
593+\newcommand{\Var}{\DC{var}}
594+\newcommand{\Lam}{\DC{lam}}
595+\newcommand{\App}{\DC{app}}
596+\newcommand{\TermM}{\TC{Term^-}}
597+\newcommand{\VarM}{\DC{var^-}}
598+\newcommand{\LamM}{\DC{lam^-}}
599+\newcommand{\AppM}{\DC{app^-}}
600+\newcommand{\Env}{\TC{Env}}
601+\newcommand{\SType}{\TC{STy}}
602+\newcommand{\farrow}{\Rightarrow}
603+\newcommand{\lookup}{\FN{lookup}}
604+
605+% \newcommand{\source}{\Lang{TT}}
606+\newcommand{\source}{\textbf{DT-Res}}
607+\newcommand{\target}{\Lang{ExTT}}
608+\newcommand{\runtime}{\Lang{RunTT}}
609+
610+\newcommand{\lt}{\TC{<}}
611+\newcommand{\ltO}{\DC{ltO}}
612+\newcommand{\ltS}{\DC{ltS}}
613+
614+\newcommand{\interp}[1]{\llbracket #1 \rrbracket}
615+\newcommand{\inferrable}[2]{\FN{inferrable}(#1,#2)}
616+\newcommand{\mkPat}{\FN{mkPat}}
617+
618+\newcommand{\FinM}{\TC{Fin^-}}
619+\newcommand{\fzM}{\DC{f0^-}}
620+\newcommand{\fsM}{\DC{fs^-}}
621+
622+\newcommand{\concat}{\mathrm{++}}
623+
624+%\newcommand{\bottom}{\perp}
625+
626+% Reductions
627+
628+\newcommand{\reduces}{\mapsto}
629+\newcommand{\translation}{\Rightarrow}
630+%\newcommand{\reducesn}[1]{\reduces\hspace*{-0.15cm}_{#1}}
631+%\newcommand{\reducesto}{\reduces\hspace*{-0.15cm}^{*}}
632+\newcommand{\reducesn}[1]{\reduces_{#1}}
633+\newcommand{\reducesto}{\reduces^{*}}
634+
635+% Equality
636+
637+\newcommand{\Refl}{\DC{refl}}
638+\newcommand{\leZ}{\DC{O_{\le}}}
639+\newcommand{\leS}{\DC{S_{\le}}}
640+
641+% Random elimination things
642+
643+\newcommand{\lte}{\TC{\leq}}
644+\newcommand{\lten}{\DC{leN}}
645+\newcommand{\lteO}{\DC{leO}}
646+\newcommand{\lteS}{\DC{leS}}
647+
648+\newcommand{\ltelim}{\Elim{\lt}}
649+\newcommand{\leelim}{\Elim{\lte}}
650+
651+\newcommand{\dD}{\TC{D}}
652+\newcommand{\delim}{\Elim{\TC{D}}}
653+\newcommand{\drec}{\Rec{\TC{D}}}
654+\newcommand{\dcase}{\Cases{\TC{D}}}
655+\newcommand{\dview}{\View{\TC{D}}}
656+\newcommand{\dmemo}{\Memo{\TC{D}}}
657+\newcommand{\natrec}{\Rec{\Nat}}
658+\newcommand{\natmemo}{\Memo{\Nat}}
659+\newcommand{\natmemogen}{\Nat\textbf{-MemoGen}}
660+\newcommand{\natelim}{\Elim{\Nat}}
661+\newcommand{\boolcase}{\Cases{\Bool}}
662+\newcommand{\vectrec}{\Rec{\Vect}}
663+\newcommand{\vectelim}{\Elim{\Vect}}
664+\newcommand{\listrec}{\Rec{\List}}
665+\newcommand{\listelim}{\Elim{\List}}
666+\newcommand{\finrec}{\Rec{\Fin}}
667+\newcommand{\finelim}{\Elim{\Fin}}
668+\newcommand{\natcase}{\Cases{\Nat}}
669+\newcommand{\vectcase}{\Cases{\Vect}}
670+\newcommand{\natdoublerec}{\Nat\textbf{-double-elim}}
671+\newcommand{\eqelim}{=\textbf{-elim}}
672+\newcommand{\falsecase}{\Cases{\False}}
673+
674+% Code
675+\newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}
676+
677+% Quicksort
678+
679+\newcommand{\QSView}{\TC{QuickSort}}
680+\newcommand{\qsempty}{\DC{empty}}
681+\newcommand{\partition}{\DC{partition}}
682+\newcommand{\qsview}{\FN{mkQuickSort}}
683+
684+% More gubbins
685+
686+\newcommand{\converts}{\simeq}
687+\newcommand{\cumul}{\preceq}
688+\newcommand{\whnf}{\Downarrow}
689+\newcommand{\elem}{\in}
690+\newcommand{\proves}{\vdash}
691+\newcommand{\biimplies}{\Longleftrightarrow}
692+
693+\newcommand{\lc}{\lambda_{\mathsf{AC}}}
694+\newcommand{\zed}{\mathbb{Z}}
695+
696+% Haskell keywords
697+
698+\newcommand{\hdata}{\mathtt{data}}
699+\newcommand{\newtype}{\mathtt{newtype}}
700+%\newcommand{\htype}{\mathtt{type}}
701+
702+\newcommand{\HTC}[1]{\mathtt{#1}}
703+\newcommand{\HDC}[1]{\mathtt{#1}}
704+
705+% Nobby
706+
707+\newcommand{\Value}{\HTC{Value}}
708+\newcommand{\VGamma}{\HTC{Env}}
709+\newcommand{\Ctxt}{\HTC{Ctxt}}
710+\newcommand{\Defs}{\HTC{Defs}}
711+\newcommand{\ECtxt}{\HTC{ECtxt}}
712+\newcommand{\TCtxt}{\HTC{TCtxt}}
713+\newcommand{\VG}{\HDC{Env}}
714+\newcommand{\Model}{\HTC{Model}}
715+\newcommand{\Const}{\HTC{Const}}
716+\newcommand{\Normal}{\HTC{Normal}}
717+\newcommand{\Scope}{\HTC{Scope}}
718+\newcommand{\Kripke}{\HTC{Kripke}}
719+\newcommand{\Weakening}{\HTC{Weakening}}
720+\newcommand{\Ready}{\HTC{Ready}}
721+\newcommand{\Blocked}{\HTC{Blocked}}
722+\newcommand{\Spine}{\HTC{Spine}}
723+
724+\newcommand{\BV}{\HDC{BV}}
725+\newcommand{\BCon}{\HDC{BCon}}
726+\newcommand{\BTyCon}{\HDC{BTyCon}}
727+\newcommand{\RCon}{\HDC{RCon}}
728+\newcommand{\RTyCon}{\HDC{RTyCon}}
729+\newcommand{\BElim}{\HDC{BElim}}
730+\newcommand{\DV}{\HDC{V}}
731+\newcommand{\DP}{\HDC{P}}
732+
733+\newcommand{\MR}{\HDC{R}}
734+\newcommand{\MB}{\HDC{B}}
735+\newcommand{\DSc}{\HDC{Sc}}
736+\newcommand{\DKr}{\HDC{Kr}}
737+\newcommand{\DWk}{\HDC{Wk}}
738+\newcommand{\DSnoc}{\HDC{;}}
739+\newcommand{\DType}{\HDC{Type}}
740+\newcommand{\DName}{\HDC{Name}}
741+\newcommand{\DInt}{\HDC{Int}}
742+\newcommand{\DString}{\HDC{String}}
743+\newcommand{\DElim}{\HDC{Elim}}
744+\newcommand{\Empty}{\HDC{\emptyset}}
745+
746+\newcommand{\ConCode}{\HTC{ConCode}}
747+\newcommand{\ElimRule}{\HTC{ElimRule}}
748+
749+\newcommand{\DConst}{\HDC{Const}}
750+\newcommand{\DCon}{\HDC{Con}}
751+\newcommand{\DTyCon}{\HDC{TyCon}}
752+\newcommand{\RConst}{\HDC{RConst}}
753+\newcommand{\RLam}{\HDC{RLam}}
754+\newcommand{\RPi}{\HDC{RPi}}
755+\newcommand{\DLam}{\HDC{Lam}}
756+\newcommand{\DLet}{\HDC{Let}}
757+\newcommand{\DPi}{\HDC{Pi}}
758+\newcommand{\DApp}{\HDC{App}}
759+
760+\newcommand{\TMaybe}{\HTC{Maybe}}
761+\newcommand{\DNothing}{\HDC{Nothing}}
762+\newcommand{\DJust}{\HDC{Just}}
763+
764+
765+% G-machine and heap
766+
767+\newcommand{\PUSH}{\mathsf{PUSH}}
768+\newcommand{\PUSHNAME}{\mathsf{PUSHNAME}}
769+\newcommand{\POP}{\mathsf{DISCARD}}
770+\newcommand{\PUSHFUN}{\mathsf{PUSHFUN}}
771+\newcommand{\APPLY}{\mathsf{MKAP}}
772+\newcommand{\EVAL}{\mathsf{EVAL}}
773+\newcommand{\GCON}{\mathsf{MKCON}}
774+\newcommand{\GTUP}{\mathsf{MKTUP}}
775+\newcommand{\GTYPE}{\mathsf{MKTYPE}}
776+\newcommand{\UPDATE}{\mathsf{UPDATE}}
777+\newcommand{\RET}{\mathsf{RET}}
778+\newcommand{\UNWIND}{\mathsf{UNWIND}}
779+\newcommand{\CASEJUMP}{\mathsf{CASEJUMP}}
780+\newcommand{\LABEL}{\mathsf{LABEL}}
781+\newcommand{\MOVE}{\mathsf{MOVE}}
782+\newcommand{\JUMP}{\mathsf{JUMP}}
783+\newcommand{\SPLIT}{\mathsf{SPLIT}}
784+\newcommand{\SQUEEZE}{\mathsf{SQUEEZE}}
785+\newcommand{\JFUN}{\mathsf{JFUN}}
786+\newcommand{\PROJ}{\mathsf{PROJ}}
787+\newcommand{\ERROR}{\mathsf{ERROR}}
788+\newcommand{\SLIDE}{\mathsf{SLIDE}}
789+\newcommand{\ALLOC}{\mathsf{ALLOC}}
790+
791+\newcommand{\PUSHBIG}{\mathsf{PUSHBIG}}
792+\newcommand{\PUSHBASIC}{\mathsf{PUSHBASIC}}
793+\newcommand{\PUSHINT}{\mathsf{PUSHINT}}
794+\newcommand{\PUSHBOOL}{\mathsf{PUSHBOOL}}
795+\newcommand{\GET}{\mathsf{GET}}
796+\newcommand{\MKINT}{\mathsf{MKINT}}
797+\newcommand{\MKBOOL}{\mathsf{MKBOOL}}
798+\newcommand{\ADD}{\mathsf{ADD}}
799+\newcommand{\SUB}{\mathsf{SUB}}
800+\newcommand{\MULT}{\mathsf{MULT}}
801+\newcommand{\LT}{\mathsf{LT}}
802+\newcommand{\EQ}{\mathsf{EQ}}
803+\newcommand{\GT}{\mathsf{GT}}
804+\newcommand{\JTRUE}{\mathsf{JTRUE}}
805+
806+\newcommand{\APP}{\mathsf{APP}}
807+\newcommand{\FUN}{\mathsf{FUN}}
808+\newcommand{\CON}{\mathsf{CON}}
809+\newcommand{\TYCON}{\mathsf{TYCON}}
810+\newcommand{\TUP}{\mathsf{TUP}}
811+\newcommand{\TYPE}{\mathsf{TYPE}}
812+\newcommand{\INT}{\mathsf{INT}}
813+\newcommand{\BIGINT}{\mathsf{BIGINT}}
814+\newcommand{\BOOL}{\mathsf{BOOL}}
815+\newcommand{\HOLE}{\mathsf{HOLE}}
816+
817+% G machine translation scheme
818+
819+\newcommand{\sinterp}[1]{\mathcal{S}\interp{#1}}
820+\newcommand{\sinterpm}[1]{\mathcal{S}\AR{\interp{#1}}}
821+\newcommand{\einterp}[3]{\mathcal{E}\interp{#1}\:#2\:#3}
822+\newcommand{\cinterp}[3]{\mathcal{C}\interp{#1}\:#2\:#3}
823+\newcommand{\binterp}[3]{\mathcal{B}\interp{#1}\:#2\:#3}
824+\newcommand{\rinterp}[3]{\mathcal{R}\interp{#1}\:#2\:#3}
825+\newcommand{\iinterp}[3]{\mathcal{I}\interp{#1}\:#2\:#3}
826+\newcommand{\len}[1]{\MO{length}(#1)}
827+
828+\newcommand{\casecomp}[2]{\mathcal{I}(#1,\left\{\ARc{#2}\right\})}
829+\newcommand{\casecompA}[3]{\mathcal{I}(#1,\left\{\ARc{#2}\right\}[#3])}
830+\newcommand{\ischeme}{\mathcal{I}}
831+
832+% tail call markup
833+
834+\newcommand{\tailcall}{\mathsf{tail}}
835+
836+% Trees
837+
838+\newcommand{\Tree}{\TC{Tree}}
839+\newcommand{\Leaf}{\DC{Leaf}}
840+\newcommand{\Node}{\DC{Node}}
841+\newcommand{\treecase}{\Cases{\Tree}}
842+
843+% Languages
844+
845+\newcommand{\Coq}{\textsc{Coq}}
846+\newcommand{\Lego}{\textsc{Lego}}
847+\newcommand{\Oleg}{\textsc{Oleg}}
848+\newcommand{\Alf}{\textsc{Alf}}
849+\newcommand{\Epigram}{\textsc{Epigram}}
850+\newcommand{\SystemF}{System $\mathcal{F}$}
851+\newcommand{\Iswim}{\textsc{Iswim}}
852+\newcommand{\Cynthia}{\textit{C$^Y$\hspace*{-0.1cm}NTHIA}}
853+
854+% Accessibility
855+
856+\newcommand{\Acc}{\TC{Acc}}
857+\newcommand{\acc}{\DC{acc}}
858+\newcommand{\qsAcc}{\TC{qsAcc}}
859+\newcommand{\qsNil}{\DC{qsNil}}
860+\newcommand{\qsCons}{\DC{qsCons}}
861+\newcommand{\allQsAcc}{\FN{allQsAcc}}
862+
863+% Lazy shortcuts
864+
865+\newcommand{\naive}{na\"{\i}ve}
866+\newcommand{\Naive}{Na\"{\i}ve}
867+
868+% Conor's bits
869+
870+\newcommand{\remem}[1]{\left|#1\right|}
871+\newcommand{\idsb}{\MO{id}}
872+\newcommand{\ang}[1]{\langle#1\rangle}
873+
874+\newcommand{\vePm}[1]{\vP #1 \vm_{\Vnil} #1 \vm_{\Vcons}}%
875+\newcommand{\vcrhs}{\vm_{\Vcons}\:\vk\:\va\:\vv\:%
876+ (\vectelim\:\vA\:\vk\:\vv\:\vePm{\:})}%
877+
878+\newcommand{\igV}[2]{#1^{\ig{#2}}}
879+\newcommand{\remV}[2]{#1^{\rem{#2}}}
880+
881+% More gubbins
882+
883+\newcommand{\Between}{\TC{between}}
884+\newcommand{\bZ}{\DC{bO}}
885+\newcommand{\bZZS}{\DC{bOOs}}
886+\newcommand{\bZSS}{\DC{b0ss}}
887+\newcommand{\bSSS}{\DC{bsss}}
888+\newcommand{\betelim}{\Elim{\Between}}
889+\newcommand{\betrhs}[1]{\motive#1\meth{\bZ}#1\meth{\bZZS}#1\meth{\bZSS}#1\meth{\bSSS}}
890+
891+
892+\newcommand{\valenv}{\TC{ValEnv}}
893+\newcommand{\vempty}{\DC{empty}}
894+\newcommand{\vextend}{\DC{extend}}
895+
896+\newcommand{\EpiVal}{\TC{Epigram}}
897+\newcommand{\unsafeCoerce}{\HF{unsafeCoerce\mbox{\texttt{\#}}}}
898+
899+\newcommand{\qq}{\mbox{\texttt{"}}}
900+\newcommand{\impossible}{\RW{Impossible}}
901+
902+\newcommand{\Real}{\mathbb{R}}
903+
904+\newcommand{\DoubleRec}{\TC{DoubleElim}}
905+\newcommand{\DoubleOn}{\DC{Double_{\Z\vn}}}
906+\newcommand{\DoubleSO}{\DC{Double_{\suc\Z}}}
907+\newcommand{\DoubleSS}{\DC{Double_{\suc\suc}}}
908+
909+\newcommand{\doublerec}{\textbf{double-elim}}
910+
911+\newcommand{\set}{\TC{DList}}
912+\newcommand{\setuser}{\TC{DListTop}}
913+\newcommand{\setempty}{\emptyset}
914+\newcommand{\setinsert}{\DC{insert}}
915+
916+
917+%%%% Type systems
918+
919+\newcommand{\stlc}{\lambda\hspace*{-0.15cm}\to}
920+\newcommand{\plc}{\lambda2}
921+\newcommand{\dlc}{\lambda{}P}
922+
923+\newcommand{\EC}{\mathcal{E}}
924+
925+%%%% reductions
926+
927+\newcommand{\betared}{\iq\hspace*{-0.15cm}_{\beta}}
928+\newcommand{\deltared}{\iq\hspace*{-0.15cm}_{\delta}}
929+\newcommand{\gammared}{\iq\hspace*{-0.15cm}_{\gamma}}
930+\newcommand{\etared}{\iq\hspace*{-0.15cm}_{\eta}}
931+\newcommand{\iotared}{\iq\hspace*{-0.15cm}_{\iota}}
932+\newcommand{\rhored}{\iq\hspace*{-0.15cm}_{\rho}}
933+
934+%%%% ExTT rules
935+
936+\newcommand{\exconverts}{\stackrel{\mathsf{Ex}}{\converts}}
937+\newcommand{\excumul}{\stackrel{\mathsf{Ex}}{\cumul}}
938+\newcommand{\exequiv}{\stackrel{\mathsf{Ex}}{\equiv}}
939+\newcommand{\exreduces}{\stackrel{\mathsf{Ex}}\reduces}
940+\newcommand{\exreducesto}{\stackrel{\mathsf{Ex}}{\reducesto}}
941+\newcommand{\exreducesn}[1]{\exreduces_{#1}}
942+
943+\newcommand{\ttequiv}{\stackrel{\mathsf{TT}}{\equiv}}
944+\newcommand{\ttreduces}{\stackrel{\mathsf{TT}}\reduces}
945+\newcommand{\ttreducesn}[1]{\ttreduces_{#1}}
946+
947+%%% Type synthesis
948+
949+\newcommand{\hastype}{\Longrightarrow}
950+\newcommand{\whnfs}{\twoheadrightarrow}
951+\newcommand{\conv}{\converts}
952+
953+\newcommand{\exhastype}{\stackrel{\mathsf{Ex}}{\hastype}}
954+\newcommand{\exwhnfs}{\stackrel{\mathsf{Ex}}{\whnfs}}
955+\newcommand{\exconv}{\stackrel{\mathsf{Ex}}{\conv}}
956+\newcommand{\exproves}{\stackrel{\mathsf{Ex}}{\proves}}
957+
958+\newcommand{\tthastype}{\stackrel{\mathsf{TT}}{\hastype}}
959+\newcommand{\ttwhnfs}{\stackrel{\mathsf{TT}}{\whnfs}}
960+\newcommand{\ttconv}{\stackrel{\mathsf{TT}}{\conv}}
961+\newcommand{\ttproves}{\stackrel{\mathsf{TT}}{\proves}}
962+
963+%%% Lightning
964+
965+\newcommand{\light}[1]{\lightning^{#1}}
966+\newcommand{\LHab}[1]{\pad{\;}{:^{#1}}}
967+\newcommand{\llam}[3]{\lambda#1\pad{\!}{:}^{#2}#3}
968+\newcommand{\lall}[3]{\forall#1\pad{\!}{:}^{#2}#3}
969+\newcommand{\lapp}[3]{#1(#2)^{#3}}
970+\newcommand{\larg}[2]{(#1)^{#2}}
971+
972+\newcommand{\RName}[1]{\hspace*{0.1in}\mathsf{#1}}
973+
974+%%% LOcal macros
975+
976+\newcommand{\ResState}{\TC{ResourceState}}
977+\newcommand{\Locked}{\DC{Locked}}
978+\newcommand{\ResHandle}{\TC{ResourceHandle}}
979+\newcommand{\Res}{\DC{Resource}}
980+\newcommand{\CLang}{\TC{CLang}}
981+\newcommand{\CFLang}{\TC{CFLang}}
982+\newcommand{\CFType}{\TC{CFType}}
983+\newcommand{\CLType}{\TC{CType}}
984+\newcommand{\RHandle}{\DC{RHandle}}
985+\newcommand{\RType}{\DC{RType}}
986+\newcommand{\RUnit}{\DC{RUnit}}
987+\newcommand{\LOCK}{\DC{LOCK}}
988+\newcommand{\UNLOCK}{\DC{UNLOCK}}
989+\newcommand{\ACTION}{\DC{ACTION}}
990+\newcommand{\FORK}{\DC{FORK}}
991+
992+\newcommand{\FSLang}{\TC{FSLang}}
993+\newcommand{\OPEN}{\DC{OPEN}}
994+\newcommand{\CLOSE}{\DC{CLOSE}}
995+\newcommand{\READ}{\DC{READ}}
996+\newcommand{\WRITE}{\DC{WRITE}}
997+\newcommand{\PRINT}{\DC{PRINT}}
998+\newcommand{\BIND}{\DC{BIND}}
999+
1000+\newcommand{\FSType}{\TC{FSType}}
1001+\newcommand{\FHandle}{\DC{FHandle}}
1002+\newcommand{\FString}{\DC{FString}}
1003+\newcommand{\FUnit}{\DC{FUnit}}
1004+\newcommand{\ElemIs}{\TC{ElemIs}}
1005+\newcommand{\elemHd}{\TC{atHead}}
1006+\newcommand{\elemTl}{\TC{inTail}}
1007+
1008+\newcommand{\emptyEnv}{\DC{empty}}
1009+\newcommand{\extendEnv}{\DC{extend}}
1010+
1011+\newcommand{\usera}{\FN{Alice}}
1012+\newcommand{\userb}{\FN{Bob}}
1013+\newcommand{\userc}{\FN{Charlie}}
1014+
1015+\newcommand{\FAcc}{\TC{FAcc}}
1016+\newcommand{\UserA}{\DC{UserAcc}}
1017+\newcommand{\GroupA}{\DC{GroupAcc}}
1018+\newcommand{\GlobalA}{\DC{GlobalAcc}}
1019+
1020+\newcommand{\Perm}{\TC{Perm}}
1021+\newcommand{\Username}{\TC{Username}}
1022+\newcommand{\GroupData}{\TC{GroupData}}
1023+\newcommand{\File}{\TC{File}}
1024+\newcommand{\FS}{\DC{file}}
1025+\newcommand{\Filepath}{\TC{Filepath}}
1026+
1027+\newcommand{\Read}{\DC{Read}}
1028+\newcommand{\Write}{\DC{Write}}
1029+\newcommand{\Execute}{\DC{Execute}}
1030+
1031+\newcommand{\Purpose}{\TC{Mode}}
1032+\newcommand{\Reading}{\DC{Reading}}
1033+\newcommand{\Writing}{\DC{Writing}}
1034+
1035+\newcommand{\FileState}{\TC{FileState}}
1036+\newcommand{\FileHandle}{\TC{FileHandle}}
1037+\newcommand{\OpenH}{\DC{OpenH}}
1038+\newcommand{\ClosedH}{\DC{ClosedH}}
1039+\newcommand{\Handle}{\TC{Handle}}
1040+\newcommand{\Open}{\DC{Open}}
1041+\newcommand{\Closed}{\DC{Closed}}
1042+
1043+\newcommand{\UserIO}{\TC{UserIO}}
1044+\newcommand{\uio}{\DC{uio}}
1045+
1046+\newcommand{\CFS}{\TC{C_{fs}}}
1047+\newcommand{\RFS}{\FN{R_{fs}}}
1048+
1049+\newcommand{\String}{\TC{String}}
1050+
1051+% inline idris code
1052+
1053+\newcommand{\Tcon}[1]{\texttt{#1}}
1054+\newcommand{\Dcon}[1]{\texttt{#1}}
1055+\newcommand{\Fname}[1]{\texttt{#1}}
1056+\newcommand{\Vv}[1]{\texttt{#1}}
1057+\newcommand{\TyTy}{\texttt{\#}}
1058+
1059+\newcommand{\direct}[1]{\texttt{\%#1}}
1060+
1061+\newcommand{\Feature}[1]{\textbf{Remark:}}
1062+%\newcommand{\Remark}[1]{\textbf{Remark:}}
tutorial/miscellany.texnew file+15
@@ -0,0 +1,15 @@
1+\section{Miscellany}
2+
3+Small things which don't quite fit elsewhere:
4+
5+\begin{itemize}
6+\item Namespaces (other than modules)
7+\item Literate programming
8+\item Totality checking
9+\item Foreign functions
10+\end{itemize}
11+
12+\subsection{Comparison}
13+
14+How does \Idris{} compare with other dependently typed languages and proof
15+assistants, such as Coq, Agda and Epigram?
tutorial/starting.texnew file+144
@@ -0,0 +1,144 @@
1+\section{Getting Started}
2+
3+\subsection{Prerequisites}
4+
5+Before installing \Idris{}, you will need to make sure you have all of the necessary
6+libraries and tools. You will need:
7+
8+\begin{itemize}
9+\item A fairly recent Haskell platform. Version 2010.1.0.0.1 is currently
10+sufficiently recent.
11+\item The Boehm-Demers-Weiser garbage collector library. This is available in
12+all major Linux distributions, or can be installed from source, available
13+from \url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}. Installing from
14+source is painless on MacOS.
15+\item The GNU multiprecision arithmetic library, GMP, available from MacPorts and
16+all major Linux distributions.
17+\end{itemize}
18+
19+\subsection{Downloading and Installing}
20+
21+The easiest way to install \Idris{}, if you have all of the prerequisites, is to type:
22+
23+\begin{SaveVerbatim}{install}
24+
25+cabal install idris
26+
27+\end{SaveVerbatim}
28+\useverb{install}
29+
30+\noindent
31+This will install the latest version released on Hackage\footnote{However version 0.9, which
32+this tutorial describes, is not yet there, so don't do this. Finishing this tutorial is the
33+last requirement before releasing it :-).}, along with any dependencies.
34+If, however, you would like the most up
35+to date development version, you can find it on GitHub at
36+\url{https://github.com/edwinb/Idris-dev}.
37+
38+To check that installation has succeeded, and to write your first \Idris{}
39+program, create a file called ``\texttt{hello.idr}'' containing the following
40+text:
41+
42+\begin{SaveVerbatim}{hello}
43+
44+module main;
45+
46+main : IO();
47+main = putStrLn "Hello world";
48+
49+\end{SaveVerbatim}
50+\useverb{hello}
51+
52+\noindent
53+If you are familiar with Haskell, it should be fairly clear what the program is doing
54+and how it works, but if not, we will explain the details later.
55+You can compile the program to an executable by entering \texttt{idris hello.idr -o hello}
56+at the shell prompt. This will create an executable called \texttt{hello}, which you can run:
57+
58+\begin{SaveVerbatim}{hello}
59+
60+$ idris hello.idr -o hello
61+$ ./hello
62+Hello world
63+
64+\end{SaveVerbatim}
65+\useverb{hello}
66+
67+\noindent
68+(Note that the \texttt{\$} indicates the shell prompt!)
69+
70+\subsection{The interactive environment}
71+
72+Entering \texttt{idris} at the shell prompt starts up the interactive
73+environment. You should see something like the following:
74+
75+\begin{SaveVerbatim}{prompt1}
76+
77+$ idris
78+ ____ __ _
79+ / _/___/ /____(_)____
80+ / // __ / ___/ / ___/ Version 0.9
81+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
82+ /___/\__,_/_/ /_/____/ Type :? for help
83+
84+Idris>
85+
86+\end{SaveVerbatim}
87+%$
88+
89+\useverb{prompt1}
90+
91+This gives a \texttt{ghci}-style interface which allows evaluation of expressions,
92+as well as type checking expressions, theorem proving, compilation, editing
93+and various other operations. \texttt{:?} gives a list of supported commands,
94+as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
95+\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
96+the program is compiled to the executable \texttt{hello}.
97+
98+\begin{SaveVerbatim}{cmds}
99+Idris version 0.9
100+-----------------
101+
102+ Command Arguments Purpose
103+
104+ <expr> Evaluate an expression
105+ :t <expr> Check the type of an expression
106+ :r :reload Reload current file
107+ :e :edit Edit current file using $EDITOR or $VISUAL
108+ :m :metavars Show remaining proof obligations (metavariables)
109+ :p :prove <name> Prove a metavariable
110+ :a :addproof Add last proof to source file
111+ :c :compile <filename> Compile to an executable <filename>
112+ :exec :execute <filename> Compile to an executable <filename> and run
113+ :? :h :help Display this help text
114+ :q :quit Exit the Idris system
115+\end{SaveVerbatim}
116+\codefigs{cmds}{Interactive environment commands}
117+
118+
119+\begin{SaveVerbatim}{run1}
120+
121+$ idris hello.idr
122+ ____ __ _
123+ / _/___/ /____(_)____
124+ / // __ / ___/ / ___/ Version 0.9
125+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
126+ /___/\__,_/_/ /_/____/ Type :? for help
127+
128+Type checking ./hello.idr
129+*hello> :t main
130+main : IO ()
131+*hello> :c hello
132+*hello> :q
133+Bye bye
134+$ ./hello
135+Hello world
136+
137+\end{SaveVerbatim}
138+
139+\codefig{run1}{Sample interactive run}
140+
141+Type checking a file, if successful, creates a bytecode version of the file (in this
142+case \texttt{hello.ibc} to speed up loading in future. The bytecode is regenerated if
143+the source file changes.
144+