git.iko.soy/Idris-dev
on master help sign in
Some proofreading, filling in some gaps.
a3569e5Edwin Brady
impl-paper/Makefile+1−1
compare with master
unifiedsplit
@@ -3,7 +3,7 @@ PAPER = impldtp
3all: ${PAPER}.pdf .PHONY
3all: ${PAPER}.pdf .PHONY
4
4
5TEXFILES = ${PAPER}.tex intro.tex conclusions.tex hll.tex\
5TEXFILES = ${PAPER}.tex intro.tex conclusions.tex hll.tex\
6− typechecking.tex elaboration.tex compiling.tex\
6+ typechecking.tex elaboration.tex \
7 syntax.tex
7 syntax.tex
8
8
9DIAGS =
9DIAGS =
impl-paper/conclusions.tex+14
@@ -2,6 +2,13 @@
2
2
3\label{sect:discussion}
3\label{sect:discussion}
4
4
5+Since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it makes
6+sense to expose the tactic language to the programmer.
7+Also tactic-implicit arguments as a generalisation of instance resolution.
8+
9+Discuss performance (anecdotally, how big is the library and how long to check,
10+and relative to previous version).
11+
5\subsection{Related Work}
12\subsection{Related Work}
6
13
7Oleg~\cite{McBride1999} as inspiration. \Epigram{}~\cite{McBride2004a}.
14Oleg~\cite{McBride1999} as inspiration. \Epigram{}~\cite{McBride2004a}.
@@ -17,4 +24,11 @@ type checks the high level language and produces a type correct core language.
17Elaboration is effectively a type checker for the high level language, so we have
24Elaboration is effectively a type checker for the high level language, so we have
18a hope of providing reasonable error messages related to the original code.]
25a hope of providing reasonable error messages related to the original code.]
19
26
27+
20\subsection{Further Work}
28\subsection{Further Work}
29+
30+[Would the EDSL approach work in other languages? Adding components of DTP
31+to imperative languages, say, using \TT{} as a verified core.
32+\Idris{} implementation as the beginning of a project to explore practical
33+DTP --- systems, protocols, security especially. And just having full
34+dependent types for lightweight correctness guarantees.]
impl-paper/elaboration.tex+52−33
@@ -9,8 +9,7 @@ functions, type classes and instances. In this section, we describe how these
9high level declarations are translated into a \TT{} program consisting of
9high level declarations are translated into a \TT{} program consisting of
10inductive families and pattern matching function definitions. We will need to
10inductive families and pattern matching function definitions. We will need to
11work at the \remph{declaration} level, and at the \remph{expression} level,
11work at the \remph{declaration} level, and at the \remph{expression} level,
12−defining the following meta-operations which together constitute an algorithm
12+defining the following meta-operations.
13−for elaborating \Idris{} programs to \TT{}.
14
13
15\begin{itemize}
14\begin{itemize}
16\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression.
15\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression.
@@ -90,10 +89,10 @@ A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:
90The \remph{hole queue} is a priority queue of names of hole and guess binders
89The \remph{hole queue} is a priority queue of names of hole and guess binders
91$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$
90$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$
92in the proof term ---
91in the proof term ---
93−we ensure that each bound name is unique. Holes essentially refer to \remph{sub goals}
92+ensuring that each bound name is unique. Holes refer to \remph{sub goals}
94in the proof.
93in the proof.
95When this queue is empty, the proof term is complete.
94When this queue is empty, the proof term is complete.
96−Creating a \TT{} expression from an \Idris{} expresson involves creating
95+Creating a \TT{} expression from an \Idris{} expression involves creating
97a new proof state, with an empty proof term, and using the high level definition
96a new proof state, with an empty proof term, and using the high level definition
98to direct the building of a final proof state, with a complete proof term.
97to direct the building of a final proof state, with a complete proof term.
99
98
@@ -162,7 +161,8 @@ The system state is a tuple, $(\vC,\vA,\vI)$, containing:
162\item Type class instances, $\vI$, containing dictionaries for type classes
161\item Type class instances, $\vI$, containing dictionaries for type classes
163\end{itemize}
162\end{itemize}
164
163
165−In the implementation, the system state is captured in a monad, \texttt{Idris}, and
164+In the implementation, the system state is captured in a monad, \texttt{Idris},
165+which also wraps the current proof state. This monad
166includes additional information such as syntax overloadings,
166includes additional information such as syntax overloadings,
167command line options, and optimisations, which do not concern us here. Elaboration
167command line options, and optimisations, which do not concern us here. Elaboration
168of expressions requires access to the system state in particular in order to expand
168of expressions requires access to the system state in particular in order to expand
@@ -226,7 +226,7 @@ for $\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
226if it cannot find such values. If successful, $\MO{Unify}$ will update the proof state.
226if it cannot find such values. If successful, $\MO{Unify}$ will update the proof state.
227\end{itemize}
227\end{itemize}
228
228
229−\remph{Tactics} are specifically meta-operations which operate on the sub-term given
229+\demph{Tactics} are meta-operations which operate on the sub-term given
230by the hole at the head of the hole queue in the proof state. They take the following form:
230by the hole at the head of the hole queue in the proof state. They take the following form:
231
231
232\DM{
232\DM{
@@ -264,7 +264,8 @@ keeping $\vx$ at the head:
264
264
265An obvious difficulty is in ensuring that names are unique throughout a proof term.
265An obvious difficulty is in ensuring that names are unique throughout a proof term.
266In the implementation, we ensure that any hole created by the $\MO{Claim}$ tactic
266In the implementation, we ensure that any hole created by the $\MO{Claim}$ tactic
267+has a unique name by checking against existing names in scope and modifying
267−has a unique name. In this paper, we will assume that all names are fresh.
268+the name if necessary. In this paper, we will assume that all created names are fresh.
268
269
269The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal
270The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal
270with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to
271with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to
@@ -445,7 +446,8 @@ For example, consider the following simple
445
446
446We can build $\FN{id}$ either as a complete term, or by applying a sequence of tactics.
447We can build $\FN{id}$ either as a complete term, or by applying a sequence of tactics.
447To achieve this, we create a proof state initialised with the type of $\FN{id}$ and
448To achieve this, we create a proof state initialised with the type of $\FN{id}$ and
448−apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$:
449+apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$.
450+Note that the types on each $\MO{Lambda}$ are solved by unification:
449
451
450\DM{
452\DM{
451\AR{
453\AR{
@@ -466,7 +468,9 @@ apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$:
466}
468}
467
469
468To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate
470To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate
471+sequencing --- in the implementation we use wrapper functions for each tactic to
472+apply $\MO{RunTac}$.
469−sequencing. Using this convention, we can build $\FN{id}$'s type and definition as shown
473+Using this convention, we can build $\FN{id}$'s type and definition as shown
470in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
474in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
471state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
475state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
472Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,
476Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,
@@ -566,8 +570,6 @@ a Coq proof script.
566\va :: = & \ve & (\mbox{normal argument}) \\
570\va :: = & \ve & (\mbox{normal argument}) \\
567\mid & \iarg{\vx}{\ve} & (\mbox{implicit argument with value}) \\
571\mid & \iarg{\vx}{\ve} & (\mbox{implicit argument with value}) \\
568\mid & \carg{\ve} & (\mbox{explicit class instance})
572\mid & \carg{\ve} & (\mbox{explicit class instance})
569−\medskip\\
570−\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\
571\end{array}
573\end{array}
572\medskip\\
574\medskip\\
573\begin{array}{rll}
575\begin{array}{rll}
@@ -645,11 +647,11 @@ than one at a time.
645%it's the global name after all and we do that by type).
647%it's the global name after all and we do that by type).
646
648
647To elaborate expressions, we define a meta-operation $\ttinterp{\cdot}$ which
649To elaborate expressions, we define a meta-operation $\ttinterp{\cdot}$ which
648−runs relative to a proof state (see Section \ref{sect:prfstate}. Its effect is
650+runs relative to a proof state (see Section \ref{sect:prfstate}). Its effect is
649to update the proof state so that the hole in focus contains a representation
651to update the proof state so that the hole in focus contains a representation
650of the given expression, by applying tactics. We assume that the proof state
652of the given expression, by applying tactics. We assume that the proof state
651has already been set up, which means that elaboration can always be
653has already been set up, which means that elaboration can always be
652−\remph{type-directed}. The proof state contains the type of the expression we
654+\remph{type-directed} since the proof state contains the type of the expression we
653are building.
655are building.
654
656
655\subsubsection{Elaborating variables and constants}
657\subsubsection{Elaborating variables and constants}
@@ -689,11 +691,13 @@ the current hole to the end of the queue with $\MO{Unfocus}$:
689}
691}
690
692
691On encountering a placeholder, our assumption is that unification will eventually solve
693On encountering a placeholder, our assumption is that unification will eventually solve
692−the hole.
694+the hole. At the end of elaboration, any holes remaining unsolved on the left hand side
695+become pattern variables. If there are any unsolved on the right hand side, elaboration
696+fails.
693
697
694\subsubsection{Elaborating bindings}
698\subsubsection{Elaborating bindings}
695
699
696−To elaborate a $\lambda$ binding, we $\MO{Attack}$ the hole, which must be a function type,
700+To elaborate a $\lambda$-binding, we $\MO{Attack}$ the hole, which must be a function type,
697apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges
701apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges
698the $\MO{Attack}$:
702the $\MO{Attack}$:
699
703
@@ -843,7 +847,8 @@ class instance arguments with the built-in $\MO{Instance}$ tactic (see Section
843
847
844The $\MO{Instance}$ tactic focuses on the given hole and searches the context for
848The $\MO{Instance}$ tactic focuses on the given hole and searches the context for
845a type class instance which would solve the goal directly. First, it examines the local
849a type class instance which would solve the goal directly. First, it examines the local
846−context, then recursively searches the global context.
850+context, then recursively searches the global context. $\MO{Instance}$ is covered
851+in detail in Section \ref{sect:instance}.
847
852
848To elaborate a simple function application, of an arbitrary expression to an arbitrary
853To elaborate a simple function application, of an arbitrary expression to an arbitrary
849argument, we need not worry about implicit arguments or class constraints. Instead,
854argument, we need not worry about implicit arguments or class constraints. Instead,
@@ -929,19 +934,20 @@ declaration.
929
934
930\subsubsection{Elaborating Pattern Matching}
935\subsubsection{Elaborating Pattern Matching}
931
936
932−[Work clause by clause, $\MO{ElabClause}$ returns a left and right hand side, and
937+To elaborate a pattern matching definition, we work clause by clause, elaborating
938+the left and right hand sides in turn. $\MO{ElabClause}$ returns the elaborated
939+left and right hand sides, and may have the side effect of adding entries
933−may have the side effect of adding things to the context, such as definitions in
940+to the global context, such as definitions in $\iwhere$ clauses.
934−$\iwhere$ clauses. Collect together in a full definition at the end.
935−
936−In the simplest case, no $\iwhere$ clause:]
941+First, let us consider the simplest case, with no $\iwhere$ clause:
937
942
938\DM{
943\DM{
939\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
944\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
940}
945}
941
946
942How do we elaborate the left hand side, given that elaboration is type directed, and
947How do we elaborate the left hand side, given that elaboration is type directed, and
943−we do not know its type until after we have elaborated it? The easiest way, which
948+we do not know its type until after we have elaborated it?
944−requires no change to the elaborator, is to define a type $\TC{Infer}$:
949+We can achieve this without any change to the elaborator by defining
950+a type $\TC{Infer}$:
945
951
946\DM{
952\DM{
947\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}
953\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}
@@ -978,7 +984,7 @@ the clauses and add the resulting collection to \TT{}.
978\MO{Elab}\:\vec{\VV{pclause}}\:\mq\:
984\MO{Elab}\:\vec{\VV{pclause}}\:\mq\:
979\edo{
985\edo{
980\tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\
986\tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\
981−\MO{TTDecl}\:\tc
987+\vec{\MO{TTDecl}}\:\tc
982}
988}
983}
989}
984}
990}
@@ -1189,6 +1195,7 @@ OrdEq (instanceOrd {{eq}} compare' max') = eq
1189\end{SaveVerbatim}
1195\end{SaveVerbatim}
1190\useverb{ordparent}
1196\useverb{ordparent}
1191
1197
1198+\noindent
1192In general, we elaborate \texttt{class} declarations as follows:
1199In general, we elaborate \texttt{class} declarations as follows:
1193
1200
1194\DM{
1201\DM{
@@ -1201,7 +1208,13 @@ In general, we elaborate \texttt{class} declarations as follows:
1201\MO{Elab}\:
1208\MO{Elab}\:
1202\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Set\:\iwhere\\
1209\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Set\:\iwhere\\
1203\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}
1210\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}
1204−\\
1211+}
1212+}
1213+}
1214+
1215+\DM{
1216+\AR{
1217+\AR{
1205\vec{\MO{ElabMeth}}\:\vec{\VV{meth}}\:\td\\
1218\vec{\MO{ElabMeth}}\:\vec{\VV{meth}}\:\td\\
1206\vec{\MO{ElabParent}}\:\tc
1219\vec{\MO{ElabParent}}\:\tc
1207}
1220}
@@ -1220,6 +1233,7 @@ In general, we elaborate \texttt{class} declarations as follows:
1220}
1233}
1221}
1234}
1222
1235
1236+\noindent
1223Then we elaborate \texttt{instance} declarations as follows:
1237Then we elaborate \texttt{instance} declarations as follows:
1224
1238
1225\DM{
1239\DM{
@@ -1242,12 +1256,12 @@ Then we elaborate \texttt{instance} declarations as follows:
1242Adding default definitions is straightforward: simply insert the default definition where
1256Adding default definitions is straightforward: simply insert the default definition where
1243there is a method missing in an \texttt{instance} declaration.
1257there is a method missing in an \texttt{instance} declaration.
1244
1258
1245−[Key point: we've added a higher level language construct simply by elaborating in terms of
1259+\textbf{Remark:} Here, we have added a higher level language construct (type
1246−a lower level language construct. In particular, we don't need to worry about type
1260+classes) simply by elaborating in terms of lower level language constructs
1247−class \remph{resolution}, because we have a tactic to do that.
1261+(data types and functions). We achieve type class resolution by implementing a
1248−We can build a lot of extensions this way because we
1262+tactic, $\MO{Instance}$. We can build several extensions this way because we
1249−have effectively built, bottom up, an Embedded Domain Specific Language for constructing
1263+have effectively built, bottom up, an Embedded Domain Specific Language for
1250−programs in \TT{}.]
1264+constructing programs in \TT{}.
1251
1265
1252\subsubsection{The $\MO{Instance}$ tactic}
1266\subsubsection{The $\MO{Instance}$ tactic}
1253
1267
@@ -1356,6 +1370,8 @@ and $\icase$ expressions:
1356\ve ::= & \ldots \\
1370\ve ::= & \ldots \\
1357\mid & \mvar{\vx} & (\mbox{metavariable}) &
1371\mid & \mvar{\vx} & (\mbox{metavariable}) &
1358\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) \\
1372\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) \\
1373+\medskip\\
1374+\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\
1359\end{array}
1375\end{array}
1360}
1376}
1361}
1377}
@@ -1412,7 +1428,7 @@ it to the current context:
1412\edo{
1428\edo{
1413(\tv\Hab\ttt)\gets\MO{Context}\\
1429(\tv\Hab\ttt)\gets\MO{Context}\\
1414\vT\gets\MO{Type}\\
1430\vT\gets\MO{Type}\\
1415−\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vt)\\
1431+\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vT)\\
1416\ttinterp{\vx\:\tv}
1432\ttinterp{\vx\:\tv}
1417}
1433}
1418}
1434}
@@ -1422,7 +1438,7 @@ it to the current context:
1422A \texttt{case} expression allows pattern matching on intermediate values. The difficulty
1438A \texttt{case} expression allows pattern matching on intermediate values. The difficulty
1423in elaborating \texttt{case} expressions is that \TT{} allows matching only on
1439in elaborating \texttt{case} expressions is that \TT{} allows matching only on
1424\emph{top level} values. To elaborate a \texttt{case} expression, therefore,
1440\emph{top level} values. To elaborate a \texttt{case} expression, therefore,
1425−we create a new top level function standing for the expression, and call it. The natural
1441+we create a new top level function standing for the expression, and apply it. The natural
1426way to implement this is to use a metavariable. For example, we have already seen
1442way to implement this is to use a metavariable. For example, we have already seen
1427\texttt{lookup\_default}:
1443\texttt{lookup\_default}:
1428
1444
@@ -1466,6 +1482,9 @@ $\MO{Elab}$. Again, because of the way we have set up an Embedded Domain Specifi
1466Language for describing elaboration, we have been able to implement a new higher
1482Language for describing elaboration, we have been able to implement a new higher
1467level language feature in terms of elaboration of lower level language features.
1483level language feature in terms of elaboration of lower level language features.
1468
1484
1485+%\subsubsection{Tactic-implicit arguments}
1486+
1487+
1469%\subsubsection{Pairs and Dependent Pairs}
1488%\subsubsection{Pairs and Dependent Pairs}
1470
1489
1471% Other extensions: do notation, idiom brackets, pairs, etc, are easily expressed
1490% Other extensions: do notation, idiom brackets, pairs, etc, are easily expressed
impl-paper/hll.tex+39−16
@@ -4,7 +4,7 @@
4
4
5\Idris{} is
5\Idris{} is
6a pure functional programming language with dependent types. It is
6a pure functional programming language with dependent types. It is
7−eagerly evaluted by default, and is compiled via the Epic supercombinator
7+eagerly evaluted by default, and compiled via the Epic supercombinator
8library \cite{brady2011epic}.
8library \cite{brady2011epic}.
9In this section, I will give a brief introduction to programming in \Idris{},
9In this section, I will give a brief introduction to programming in \Idris{},
10covering the most important features. A full tutorial is available elsewhere
10covering the most important features. A full tutorial is available elsewhere
@@ -75,7 +75,8 @@ infixr 10 ::
75\end{SaveVerbatim}
75\end{SaveVerbatim}
76\useverb{infixcons}
76\useverb{infixcons}
77
77
78−\noindent
78+This declares that \texttt{::} is a right associative operator (\texttt{infixr})
79+with a precedence level of 10.
79Functions, data constructors and type constuctors may all be given infix
80Functions, data constructors and type constuctors may all be given infix
80operators as names. They may be used in prefix form if enclosed in brackets,
81operators as names. They may be used in prefix form if enclosed in brackets,
81e.g. \tDC{(::)}.
82e.g. \tDC{(::)}.
@@ -105,10 +106,11 @@ mult (S k) y = plus y (mult k y)
105The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
106The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
106for use by \texttt{Nat}, and are implemented
107for use by \texttt{Nat}, and are implemented
107using the above functions. Unlike Haskell, there is no restriction on whether
108using the above functions. Unlike Haskell, there is no restriction on whether
108−types and function names must begin with a capital letter or not. Function
109+types and function names must begin with a capital letter or not.
110+%Function
109−names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
111+%names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},
110−\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
112+%\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are
111−all part of the same namespace.
113+%all part of the same namespace.
112
114
113\Idris{} has an interactive prompt, at which we can test these functions:
115\Idris{} has an interactive prompt, at which we can test these functions:
114
116
@@ -160,7 +162,8 @@ further than the outer function.
160\textbf{Scope:}
162\textbf{Scope:}
161Any names which are visible in the outer scope are also visible in the \texttt{where}
163Any names which are visible in the outer scope are also visible in the \texttt{where}
162clause (unless they have been redefined, such as \texttt{xs} here).
164clause (unless they have been redefined, such as \texttt{xs} here).
163−\emph{However}, names which appear in the type are \emph{not} in scope. In particular,
165+\emph{However}, names which appear in the type are \emph{not} automatically
166+in scope. In particular,
164in the above example, the \texttt{a} in the top level type and the \texttt{a} in the
167in the above example, the \texttt{a} in the top level type and the \texttt{a} in the
165auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required
168auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required
166behaviour, the \texttt{a} can be brought into scope as follows:
169behaviour, the \texttt{a} can be brought into scope as follows:
@@ -178,7 +181,8 @@ reverse {a} xs = revAcc [] xs where
178\subsubsection{Dependent Types}
181\subsubsection{Dependent Types}
179
182
180A standard example of a dependent type is the type of ``lists with length'',
183A standard example of a dependent type is the type of ``lists with length'',
184+conventionally called ``vectors'' in the dependently typed programming
181−conventionally called ``vectors''. In \Idris{}, we declare vectors as follows:
185+literature. In \Idris{}, we declare vectors as follows:
182
186
183\begin{SaveVerbatim}{vect}
187\begin{SaveVerbatim}{vect}
184
188
@@ -196,7 +200,7 @@ are declared in different namespaces (in practice, normally in different modules
196Ambiguous constructor names are resolved by type.
200Ambiguous constructor names are resolved by type.
197
201
198This declares a family of types, which requires a different form of declaration
202This declares a family of types, which requires a different form of declaration
199−different from the simple type declarations above. It resembles a Haskell GADT
203+from the simple type declarations above. It resembles a Haskell GADT
200declaration: we explicitly state the type
204declaration: we explicitly state the type
201of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an
205of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an
202argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}
206argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}
@@ -293,6 +297,17 @@ with \texttt{n} elements of type \texttt{a}. But there are also two names,
293\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
297\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}
294arguments to \texttt{index}. We could also write the type of \texttt{index} as:
298arguments to \texttt{index}. We could also write the type of \texttt{index} as:
295
299
300+\begin{SaveVerbatim}{vindeximppl}
301+
302+index : {a:_} -> {n:_} -> Fin n -> Vect a n -> a
303+
304+\end{SaveVerbatim}
305+\useverb{vindeximppl}
306+
307+\noindent
308+Here we have given bindings for \texttt{a} and \texttt{n} with placeholders for
309+their types, to be inferred by the machine. We could also give the types explicitly:
310+
296\begin{SaveVerbatim}{vindeximpty}
311\begin{SaveVerbatim}{vindeximpty}
297
312
298index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
313index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
@@ -339,11 +354,14 @@ this constructors of \texttt{List} and \texttt{Vect}, names
339can be overloaded in an ad-hoc manner and resolved according to the context in which
354can be overloaded in an ad-hoc manner and resolved according to the context in which
340they are used. This is mostly for convenience, to eliminate the need to decorate
355they are used. This is mostly for convenience, to eliminate the need to decorate
341constructor names in similarly structured data types, and eliminate explicit qualification
356constructor names in similarly structured data types, and eliminate explicit qualification
342−of ambiguous names where only one is well-typed.
357+of ambiguous names where only one is well-typed --- this is especially useful
358+for disambiguating record field names\footnote{Records are however beyond the scope
359+of this paper}.
343
360
344−Secondly, \Idris{} implements \remph{type classes}. This allows a more principled approach
361+Secondly, \Idris{} implements \remph{type classes}, following Haskell. This
362+allows a more principled approach to overloading --- a type class gives a
345−to overloading --- a type class gives a collection of overloaded operations which describe
363+collection of overloaded operations which describe the interface for
346−the interface for \remph{instances} of that class.
364+\remph{instances} of that class.
347
365
348A simple example
366A simple example
349is the \texttt{Show} type class, which is defined in the library and
367is the \texttt{Show} type class, which is defined in the library and
@@ -380,11 +398,16 @@ instance Show Nat where
380 show O = "O"
398 show O = "O"
381 show (S k) = "s" ++ show k
399 show (S k) = "s" ++ show k
382
400
401+\end{SaveVerbatim}
402+\useverb{shownat}
403+
404+\begin{SaveVerbatim}{shownati}
405+
383Idris> show (S (S (S O)))
406Idris> show (S (S (S O)))
384"sssO" : String
407"sssO" : String
385
408
386\end{SaveVerbatim}
409\end{SaveVerbatim}
387−\useverb{shownat}
410+\useverb{shownati}
388
411
389\noindent
412\noindent
390Only one instance of a class can be given for a type --- instances may not overlap.
413Only one instance of a class can be given for a type --- instances may not overlap.
@@ -473,7 +496,7 @@ mirror xs = let xs' = rev xs in
473\useverb{letb}
496\useverb{letb}
474
497
475\noindent
498\noindent
476−We can also do simple pattern matching in \texttt{let} bindings. For example, we can extract
499+We can also pattern match in \texttt{let} bindings. For example, we can extract
477fields from a record as follows, as well as by pattern matching at the top level:
500fields from a record as follows, as well as by pattern matching at the top level:
478
501
479\begin{SaveVerbatim}{letp}
502\begin{SaveVerbatim}{letp}
@@ -507,7 +530,7 @@ at the point where the given function returns true. We then deconstruct the
507pair it returns, and remove the first character of the second string.
530pair it returns, and remove the first character of the second string.
508
531
509A \texttt{case} expression can match several cases, for example, to inspect an
532A \texttt{case} expression can match several cases, for example, to inspect an
510−intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
533+intermediate value of type \texttt{Maybe a}. For example, \texttt{list\_lookup}
511looks up an index in a list, returning \texttt{Nothing} if the index is out
534looks up an index in a list, returning \texttt{Nothing} if the index is out
512of bounds. We can use this to write \texttt{lookup\_default}, which
535of bounds. We can use this to write \texttt{lookup\_default}, which
513looks up an index and returns a default value if the index is out of bounds:
536looks up an index and returns a default value if the index is out of bounds:
impl-paper/impldtp.tex+8−8
@@ -67,9 +67,9 @@ KY16 9SX, UK}
67
67
68\begin{abstract}
68\begin{abstract}
69Many components of a dependently typed programming language are by now well
69Many components of a dependently typed programming language are by now well
70−understood, such as the underlying type theory, type checking, unification and
70+understood, for example the underlying type theory, type checking, unification and
71evaluation. How to combine these components into a realistic and usable high
71evaluation. How to combine these components into a realistic and usable high
72−level language is, however, folklore, discovered anew by each succesive
72+level language is, however, folklore, discovered anew by succesive
73language implementations. In this paper, I describe the implementation of a
73language implementations. In this paper, I describe the implementation of a
74new dependently typed functional programming language, \Idris{}.
74new dependently typed functional programming language, \Idris{}.
75\Idris{} is intended to be a \emph{general purpose} programming language
75\Idris{} is intended to be a \emph{general purpose} programming language
@@ -127,14 +127,14 @@ implementation of new high level language constructs.
127
127
128\appendix
128\appendix
129
129
130−\section{Elaboration meta-operations}
130+%\section{Elaboration meta-operations}
131
131
132−It's possible that it would be useful to have a quick reference of meta-operations
132+%It's possible that it would be useful to have a quick reference of meta-operations
133−used by the elaborator here.
133+%used by the elaborator here.
134
134
135−They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
135+%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,
136−$\MO{NewProof}$, $\MO{NewTerm}$,
136+%$\MO{NewProof}$, $\MO{NewTerm}$,
137−$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
137+%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.
138
138
139%\input{code}
139%\input{code}
140
140
impl-paper/intro.tex+4−2
@@ -50,11 +50,13 @@ an EDSL based method for translating programs in a
50high level dependently typed programming language to a small core type theory,
50high level dependently typed programming language to a small core type theory,
51\TT{}, based on UTT \cite{luo1994}. The paper describes the structure of the
51\TT{}, based on UTT \cite{luo1994}. The paper describes the structure of the
52EDSL including proof and system state, and introduces a collection of \remph{tactics}
52EDSL including proof and system state, and introduces a collection of \remph{tactics}
53−for manipulating incompete programs.
53+for manipulating incomplete programs.
54Secondly, the paper gives a detailed description of the core type theory used
54Secondly, the paper gives a detailed description of the core type theory used
55by \Idris{}, including a full description of the typing rules. Finally, through
55by \Idris{}, including a full description of the typing rules. Finally, through
56describing the EDSL and the specific tactics, the paper shows how to extend
56describing the EDSL and the specific tactics, the paper shows how to extend
57\Idris{} with higher level features.
57\Idris{} with higher level features.
58+While we apply these ideas to \Idris{} specifically, the method for term construction
59+is equally applicable to other typed programming languages.
58
60
59The paper is structured as follows: In Section \ref{sect:hll} I give an overview of
61The paper is structured as follows: In Section \ref{sect:hll} I give an overview of
60programming in \Idris{}, introducing the high level constructs which will be
62programming in \Idris{}, introducing the high level constructs which will be
@@ -68,7 +70,7 @@ Section \ref{sect:discussion} we discuss related work and conclude.
68
70
69\subsection{Typographical conventions}
71\subsection{Typographical conventions}
70
72
71−This paper includes programs in two different but related languages: a high level
73+This paper presents programs in two different but related languages: a high level
72language \Idris{} intended for programmers, and a low level language \TT{} to
74language \Idris{} intended for programmers, and a low level language \TT{} to
73which \Idris{} is elaborated. We distinguish these languages typographically as
75which \Idris{} is elaborated. We distinguish these languages typographically as
74follows:
76follows:
impl-paper/library.bib+828−828
@@ -1,297 +1,276 @@
1Automatically generated by Mendeley 1.3.1
1Automatically generated by Mendeley 1.3.1
2Any changes to this file will be lost if it is regenerated by Mendeley.
2Any changes to this file will be lost if it is regenerated by Mendeley.
3
3
4−@inproceedings{Sculthorpe2009,
4+@inproceedings{ko2011modularising,
5−author = {Sculthorpe, Neil and Nilsson, Henrik},
5+author = {Ko, H.S. and Gibbons, J.},
6−booktitle = {International Conference on Functional Programming ({ICFP} '09)},
6+booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
7−file = {:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},
7+file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
8−title = {{Safe functional reactive programming through dependent types}},
8+pages = {13--24},
9+publisher = {ACM},
10+title = {{Modularising inductive families}},
9−url = {http://dl.acm.org/citation.cfm?id=1596558},
11+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},
10−year = {2009}
12+year = {2011}
11}
13}
12−@inproceedings{Augustsson1985,
14+@inproceedings{gibbons2011modularising,
13−address = {Berlin, Heidelberg},
15+author = {Gibbons, J. and Ko, H.S. and Others},
14−author = {Augustsson, Lennart},
16+file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
15−booktitle = {Functional Programming Languages and Computer Architecture},
17+title = {{Modularising inductive families}},
16−doi = {10.1007/3-540-15975-4},
18+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
17−editor = {Jouannaud, Jean-Pierre},
18−isbn = {978-3-540-15975-9},
19−keywords = {Computer Science},
20−pages = {368----381},
21−publisher = {Springer Berlin Heidelberg},
22−series = {Lecture Notes in Computer Science},
23−title = {{Compiling Pattern Matching}},
24−url = {http://www.springerlink.com/content/y647423656557505/},
25−volume = {201},
26−year = {1985}
19+year = {2011}
27}
20}
28−@inproceedings{NanevskiAAMorrisett2008,
21+@article{Okasaki1993,
29−abstract = {We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions. The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which, abstracts the implementation details and ensures that the modules properly implement the finite map abstraction. Copyright 2008 ACM.},
22+author = {Okasaki, Chris},
30−author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},
23+file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
31−booktitle = {International Conference on Functional Programming},
24+journal = {Journal of functional programming},
32−doi = {10.1145/1411204.1411237},
25+title = {{Red-Black Trees in A Functional Setting}},
33−file = {:home/edwin/Research/Papers/Mendeley/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},
26+year = {1993}
34−isbn = {9781595939197},
27+}
35−issn = {15232867},
28+@misc{Brady2012b,
29+author = {Brooks, Fred},
30+doi = {10.1093/epirev/mxr031},
31+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
32+isbn = {9780321702081},
33+issn = {1478-6729},
34+pmid = {22215642},
35+title = {{The Design of Design Chapter 2}}
36+}
37+@inproceedings{Brady2003,
38+author = {Brady, Edwin and McBride, Conor and McKinna, James},
39+booktitle = {Types for Proofs and Programs},
40+file = {:home/edwin/Research/Papers/Mendeley/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},
36keywords = {Dependent Types},
41keywords = {Dependent Types},
37mendeley-tags = {Dependent Types},
42mendeley-tags = {Dependent Types},
38−number = {9},
43+title = {{Inductive families need not store their indices}},
39−pages = {229--240},
44+url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},
40−title = {{Ynot: Dependent types for imperative programs}},
41−url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},
42−volume = {43},
43−year = {2008}
45+year = {2003}
44}
46}
45−@inproceedings{McBride2004b,
47+@misc{TheMendeleySupportTeam2011,
46−author = {McBride, Conor and McKinna, James},
48+abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
47−booktitle = {Haskell Workshop},
49+address = {London},
48−file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},
50+author = {{The Mendeley Support Team}},
49−title = {{I am not a number : I am a free variable}},
51+booktitle = {Mendeley Desktop},
52+file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
53+keywords = {Mendeley,how-to,user manual},
54+pages = {1--16},
55+publisher = {Mendeley Ltd.},
56+title = {{Getting Started with Mendeley}},
57+url = {http://www.mendeley.com},
50−year = {2004}
58+year = {2011}
51}
59}
52−@article{marlow2006making,
60+@inproceedings{Wadler1989,
53−author = {Marlow, S. and {Peyton Jones}, S.},
61+abstract = {From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds' abstraction theorem for the polymorphic lambda calculus.},
54−file = {:home/edwin/Research/Papers/Mendeley/Marlow, Peyton Jones/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},
62+author = {Wadler, Philip},
55−journal = {Journal of Functional Programming},
63+booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
64+doi = {10.1145/99370.99404},
65+file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},
66+isbn = {0897913280},
56−number = {4-5},
67+number = {June},
57−pages = {415--449},
68+pages = {347--359},
58−publisher = {Cambridge University Press},
69+publisher = {ACM},
59−title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}},
70+series = {FPCA '89},
71+title = {{Theorems for free!}},
72+url = {http://portal.acm.org/citation.cfm?id=99404},
73+year = {1989}
74+}
75+@phdthesis{norell2007thesis,
76+author = {Norell, Ulf},
77+file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
78+keywords = {Dependent Types},
79+mendeley-tags = {Dependent Types},
80+publisher = {Citeseer},
81+school = {Chalmers University of Technology},
82+title = {{Towards a practical programming language based on dependent type theory}},
83+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
84+year = {2007}
85+}
86+@inproceedings{l,
87+author = {L\"{a}mmel, R. and Jones, S.P.},
88+booktitle = {ACM SIGPLAN Notices},
89+file = {:home/edwin/Research/Papers/Mendeley/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},
90+number = {3},
91+pages = {26--37},
92+publisher = {ACM},
93+title = {{Scrap your boilerplate: a practical design pattern for generic programming}},
60−url = {http://dl.acm.org/citation.cfm?id=1166018},
94+url = {http://dl.acm.org/citation.cfm?id=640136.604179},
61−volume = {16},
95+volume = {38},
96+year = {2003}
97+}
98+@inproceedings{Xi1999,
99+abstract = {Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.},
100+author = {Xi, Hongwei and Pfenning, Frank},
101+booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},
102+doi = {10.1145/292540.292560},
103+file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},
104+isbn = {1581130953},
105+issn = {07439016},
106+keywords = {Dependent Types},
107+mendeley-tags = {Dependent Types},
108+organization = {Carnegie Mellon University},
109+pages = {214--227},
110+publisher = {ACM Press},
111+series = {POPL '99},
112+title = {{Dependent types in practical programming}},
113+url = {http://portal.acm.org/citation.cfm?doid=292540.292560},
114+volume = {26},
115+year = {1999}
116+}
117+@inproceedings{morris2006exploring,
118+author = {Morris, P. and Altenkirch, T. and McBride, C.},
119+booktitle = {Types for Proofs and Programs},
120+file = {:home/edwin/Research/Papers/Mendeley/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},
121+pages = {252--267},
122+publisher = {Springer},
123+title = {{Exploring the regular tree types}},
124+url = {http://www.springerlink.com/index/f9p1317716614834.pdf},
62year = {2006}
125year = {2006}
63}
126}
64−@book{Choosing2012,
127+@book{Approach2012,
65−author = {Fowler, Martin},
128+author = {Hunt, Andrew and Thomas, David},
66booktitle = {Carcinogenesis},
129booktitle = {Carcinogenesis},
67doi = {10.1093/carcin/bgs054},
130doi = {10.1093/carcin/bgs054},
68−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
131+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
69−isbn = {9780132107549},
132+isbn = {020161622X},
70issn = {1460-2180},
133issn = {1460-2180},
71number = {3},
134number = {3},
72pmid = {22383472},
135pmid = {22383472},
73−title = {{Domain Specific Languages Chapter 6}},
136+title = {{The Pragmatic Programmer Chapter 2}},
74url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
137url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
75volume = {33}
138volume = {33}
76}
139}
77−@misc{Protocols2012a,
140+@article{Miller1992,
78−author = {Anderson, Ross},
141+author = {Miller, D},
142+file = {:home/edwin/Research/Papers/Mendeley/Miller/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},
143+journal = {Journal of symbolic computation},
144+title = {{Unification under a mixed prefix}},
145+url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},
146+year = {1992}
147+}
148+@misc{Interface2012a,
149+author = {Kreibich, Jay A.},
79doi = {10.1093/epirev/mxr031},
150doi = {10.1093/epirev/mxr031},
80−file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
151+file = {:home/edwin/Research/Papers/Mendeley/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
81−isbn = {9780470068526},
152+isbn = {9781449394592},
82issn = {1478-6729},
153issn = {1478-6729},
83pmid = {22215642},
154pmid = {22215642},
84−title = {{Security Engineering Chapter 3}}
155+title = {{Using SQLite Chapter 7}}
85−}
86−@inproceedings{czarnecki2004dsl,
87−author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},
88−booktitle = {Domain-Specific Program Generation},
89−file = {:home/edwin/Research/Papers/Mendeley/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},
90−pages = {51--72},
91−publisher = {Springer},
92−title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},
93−url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},
94−year = {2004}
95}
156}
96−@article{Steiner1988,
157+@inproceedings{chlipala2010ur,
97−author = {Steiner, JG},
158+author = {Chlipala, Adam},
98−file = {:home/edwin/Research/Papers/Mendeley/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
159+booktitle = {ACM SIGPLAN Notices},
99−journal = {Proc. Winter USENIX Conference},
160+file = {:home/edwin/Research/Papers/Mendeley/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
100−title = {{Kerberos: An authentication service for open network systems}},
161+number = {6},
101−url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},
162+pages = {122--133},
163+publisher = {ACM},
164+title = {{Ur: statically-typed metaprogramming with type-level record computation}},
165+url = {http://dl.acm.org/citation.cfm?id=1806612},
166+volume = {45},
102−year = {1988}
167+year = {2010}
103}
168}
104−@book{Fowler,
169+@book{peyton1987implementation,
105−author = {Fowler, Martin},
170+author = {{Peyton Jones}, S.L.},
106−booktitle = {Language},
171+publisher = {Prentice-Hall, Inc.},
107−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
172+title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}},
108−isbn = {9780132107549},
173+url = {http://dl.acm.org/citation.cfm?id=1096899},
109−title = {{Domain Specific Languages Chapter 2}}
174+year = {1987}
110}
175}
111−@article{Brady2006a,
176+@article{dybjer1994inductive,
112−author = {Brady, E and Hammond, K},
177+author = {Dybjer, P.},
113−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},
178+journal = {Formal aspects of computing},
114−journal = {\ldots of the 5th international conference on \ldots},
179+number = {4},
115−keywords = {Dependent Types},
180+pages = {440--465},
116−mendeley-tags = {Dependent Types},
181+publisher = {Springer},
117−title = {{A verified staged interpreter is a verified compiler}},
182+title = {{Inductive families}},
118−url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},
183+url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
184+volume = {6},
119−year = {2006}
185+year = {1994}
120}
186}
121−@inproceedings{oury2008power,
187+@inproceedings{lempsink2009type,
122−author = {Oury, N. and Swierstra, W.},
188+author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},
123−booktitle = {International Conference on Functional Programming},
189+booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},
124−file = {:home/edwin/Research/Papers/Mendeley/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
190+file = {:home/edwin/Research/Papers/Mendeley/Lempsink, Leather, L\"{o}h/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},
125−keywords = {Dependent Types},
126−mendeley-tags = {Dependent Types},
127−number = {9},
128−pages = {39--50},
191+pages = {61--72},
129publisher = {ACM},
192publisher = {ACM},
130−title = {{The power of Pi}},
193+title = {{Type-safe diff for families of datatypes}},
131−url = {http://dl.acm.org/citation.cfm?id=1411213},
194+url = {http://dl.acm.org/citation.cfm?id=1596624},
132−volume = {43},
133−year = {2008}
195+year = {2009}
134−}
135−@phdthesis{McBride1999,
136−author = {McBride, Conor},
137−file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
138−keywords = {Dependent Types},
139−mendeley-tags = {Dependent Types},
140−school = {University of Edinburgh},
141−title = {{Dependently typed functional programs and their proofs}},
142−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
143−year = {1999}
144−}
145−@article{mcbride2010ornamental,
146−author = {McBride, Conor},
147−file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
148−journal = {Journal of Functional Programming},
149−title = {{Ornamental algebras, algebraic ornaments}},
150−url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},
151−year = {2010}
152−}
153−@article{Hughes1989,
154−abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},
155−author = {Hughes, J},
156−chapter = {2},
157−doi = {10.1093/comjnl/32.2.98},
158−editor = {Turner, David A},
159−file = {:home/edwin/Research/Papers/Mendeley/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
160−institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},
161−isbn = {0201172364},
162−issn = {00104620},
163−journal = {The Computer Journal},
164−number = {2},
165−pages = {98--107},
166−publisher = {Br Computer Soc},
167−title = {{Why Functional Programming Matters}},
168−url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},
169−volume = {32},
170−year = {1989}
171−}
172−@article{Chapman2005epigram,
173−author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},
174−file = {:home/edwin/Research/Papers/Mendeley/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},
175−journal = {Trends in Functional Programming},
176−publisher = {Intellect Books},
177−title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
178−url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
179−year = {2005}
180−}
181−@article{McBride2004a,
182−abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.},
183−author = {McBride, Conor and McKinna, James},
184−doi = {10.1017/S0956796803004829},
185−file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
186−issn = {09567968},
187−journal = {Journal of Functional Programming},
188−keywords = {Dependent Types},
189−mendeley-tags = {Dependent Types},
190−number = {1},
191−pages = {69--111},
192−publisher = {Cambridge University Press},
193−title = {{The view from the left}},
194−url = {http://www.journals.cambridge.org/abstract_S0956796803004829},
195−volume = {14},
196−year = {2004}
197−}
198−@phdthesis{Okasaki1996,
199−author = {Okasaki, Chris},
200−file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
201−school = {Carnegie Mellon University},
202−title = {{Purely Functional Data Structures}},
203−year = {1996}
204−}
205−@misc{pollack1997believe,
206−author = {Pollack, R.},
207−file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
208−title = {{How to believe a machine-checked proof}},
209−url = {http://books.google.co.uk/books?hl=en&lr=&id=pLnKggT_In4C&oi=fnd&pg=PA205&dq=how+to+believe+a+machine+checked+proof&ots=c2OI8krqqA&sig=EF3QonGFVdOpYdKO1KmW6ljCkjY},
210−year = {1997}
211}
196}
212−@article{Abel2010,
197+@misc{The2012b,
213−abstract = {Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.},
198+author = {Brooks, Fred},
214−author = {Abel, Andreas},
199+doi = {10.1093/epirev/mxr031},
215−file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
200+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
216−journal = {EPTCS},
201+isbn = {9780321702081},
217−pages = {1--15},
202+issn = {1478-6729},
218−title = {{MiniAgda: Integrating Sized and Dependent Types}},
203+pmid = {22215642},
219−url = {http://arxiv.org/abs/1012.4896},
204+title = {{The Design of Design Chapter 1}}
220−volume = {43},
221−year = {2010}
222}
205}
223−@inproceedings{fisher2005pads,
206+@misc{The2012c,
224−author = {Fisher, K. and Gruber, R.},
207+author = {Robbins, A and Hannah, E and Lamb, L},
225−booktitle = {ACM SIGPLAN Notices},
208+doi = {10.1093/epirev/mxr031},
226−number = {6},
209+file = {:home/edwin/Research/Papers/Mendeley/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
227−pages = {295--304},
210+isbn = {9780596529833},
228−publisher = {ACM},
211+issn = {1478-6729},
229−title = {{PADS: a domain-specific language for processing ad hoc data}},
212+pmid = {22215642},
230−url = {http://dl.acm.org/citation.cfm?id=1065046},
213+title = {{Learning the vi and Vim Editors}}
231−volume = {40},
232−year = {2005}
233}
214}
234−@article{mccann2000packet,
215+@book{Brady2012,
235−author = {McCann, P.J. and Chandra, S.},
216+author = {Hunt, Andrew and Thomas, David},
236−journal = {ACM SIGCOMM Computer Communication Review},
217+booktitle = {Carcinogenesis},
218+doi = {10.1093/carcin/bgs054},
219+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
220+isbn = {020161622X},
221+issn = {1460-2180},
237−number = {4},
222+number = {3},
238−pages = {321--333},
223+pmid = {22383472},
239−publisher = {ACM},
224+title = {{The Pragmatic Programmer Chapter 5}},
240−title = {{Packet types: abstract specification of network protocol messages}},
225+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
241−url = {http://dl.acm.org/citation.cfm?id=347563},
242−volume = {30},
226+volume = {33}
243−year = {2000}
244}
227}
245−@inproceedings{Brady2003,
228+@inproceedings{Pasalic2002,
246−author = {Brady, Edwin and McBride, Conor and McKinna, James},
229+author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},
247−booktitle = {Types for Proofs and Programs},
230+booktitle = {International Conference on Functional Programming},
248−file = {:home/edwin/Research/Papers/Mendeley/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},
231+doi = {10.1145/583852.581499},
249−keywords = {Dependent Types},
232+file = {:home/edwin/Research/Papers/Mendeley/Pa\v{s}alic, Taha, Sheard/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},
250−mendeley-tags = {Dependent Types},
233+isbn = {1-58113-487-8},
251−title = {{Inductive families need not store their indices}},
234+issn = {03621340},
252−url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},
235+keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},
236+month = sep,
237+number = {9},
238+pages = {218--229},
239+title = {{Tagless staged interpreters for typed languages}},
240+url = {http://dl.acm.org/citation.cfm?id=583852.581499},
241+volume = {37},
253−year = {2003}
242+year = {2002}
254}
243}
255−@misc{TheMendeleySupportTeam2011,
244+@misc{Nodes2012a,
256−abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
245+author = {Brooks, Fred},
257−address = {London},
246+doi = {10.1093/epirev/mxr031},
258−author = {{The Mendeley Support Team}},
259−booktitle = {Mendeley Desktop},
260−file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
247+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
261−keywords = {Mendeley,how-to,user manual},
248+isbn = {9780321702081},
262−pages = {1--16},
249+issn = {1478-6729},
263−publisher = {Mendeley Ltd.},
250+pmid = {22215642},
264−title = {{Getting Started with Mendeley}},
251+title = {{The Design of Design Chapter 3}}
265−url = {http://www.mendeley.com},
266−year = {2011}
267}
252}
268−@inproceedings{Sheard2005,
253+@article{Haskell2012a,
269−address = {New York, New York, USA},
254+author = {Biancuzzi, F and Warden, S},
270−author = {Sheard, Tim},
255+doi = {10.1093/epirev/mxr031},
271−booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},
272−doi = {10.1145/1088348.1088356},
273−file = {:home/edwin/Research/Papers/Mendeley/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},
256+file = {:home/edwin/Research/Papers/Mendeley/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
274−isbn = {159593071X},
257+isbn = {9780596801670},
275−keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},
258+issn = {1478-6729},
276−month = sep,
259+pmid = {22215642},
277−pages = {74--85},
260+title = {{Masterminds of Programming Chapter 8}}
278−publisher = {ACM Press},
279−title = {{Putting curry-howard to work}},
280−url = {http://dl.acm.org/citation.cfm?id=1088348.1088356},
281−year = {2005}
282}
261}
283−@article{Jones2003,
262+@book{An2012,
284−abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},
263+author = {Fowler, Martin},
285−author = {Jones, Simon Peyton},
264+booktitle = {Carcinogenesis},
286−editor = {Jones, Simon Peyton},
265+doi = {10.1093/carcin/bgs054},
287−isbn = {0521826144},
266+file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
288−journal = {Language},
267+isbn = {9780132107549},
268+issn = {1460-2180},
289−number = {1},
269+number = {3},
290−publisher = {Cambridge University Press},
270+pmid = {22383472},
291−title = {{Haskell 98 Language and Libraries The Revised Report}},
271+title = {{Domain Specific Languages Chapter 1}},
292−url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},
272+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
293−volume = {13},
273+volume = {33}
294−year = {2003}
295}
274}
296@article{McBride2005,
275@article{McBride2005,
297author = {McBride, Conor},
276author = {McBride, Conor},
@@ -308,18 +287,6 @@ url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},
308volume = {3622},
287volume = {3622},
309year = {2005}
288year = {2005}
310}
289}
311−@inproceedings{chlipala2010ur,
312−author = {Chlipala, Adam},
313−booktitle = {ACM SIGPLAN Notices},
314−file = {:home/edwin/Research/Papers/Mendeley/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
315−number = {6},
316−pages = {122--133},
317−publisher = {ACM},
318−title = {{Ur: statically-typed metaprogramming with type-level record computation}},
319−url = {http://dl.acm.org/citation.cfm?id=1806612},
320−volume = {45},
321−year = {2010}
322−}
323@misc{Resolution2012a,
290@misc{Resolution2012a,
324author = {Fall, Kevin R and Stevens, W. Richard},
291author = {Fall, Kevin R and Stevens, W. Richard},
325doi = {10.1093/epirev/mxr031},
292doi = {10.1093/epirev/mxr031},
@@ -328,225 +295,31 @@ issn = {1478-6729},
328pmid = {22215642},
295pmid = {22215642},
329title = {{TCP/IP Illustrated Volume 1 Chapter 11}}
296title = {{TCP/IP Illustrated Volume 1 Chapter 11}}
330}
297}
331−@inproceedings{gibbons2011modularising,
298+@phdthesis{Brady2005,
332−author = {Gibbons, J. and Ko, H.S. and Others},
299+author = {Brady, Edwin},
333−file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
300+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
334−title = {{Modularising inductive families}},
335−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
336−year = {2011}
337−}
338−@article{burrows1990,
339−author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
340−file = {:home/edwin/Research/Papers/Mendeley/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},
341−journal = {ACM Transactions on Computer Systems},
342−pages = {18----36},
343−title = {{A logic of authentication}},
344−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569},
345−volume = {8},
346−year = {1990}
347−}
348−@misc{Brady2012b,
349−author = {Brooks, Fred},
350−doi = {10.1093/epirev/mxr031},
351−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
352−isbn = {9780321702081},
353−issn = {1478-6729},
354−pmid = {22215642},
355−title = {{The Design of Design Chapter 2}}
356−}
357−@inproceedings{Levitation2010,
358−author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},
359−booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},
360−doi = {10.1145/1932681.1863547},
361−file = {:home/edwin/Research/Papers/Mendeley/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},
362−isbn = {978-1-60558-794-3},
363−issn = {03621340},
364−keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},
365−mendeley-tags = {Dependent Types},
366−month = sep,
367−number = {9},
368−pages = {3},
369−title = {{The gentle art of levitation}},
370−url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},
371−volume = {45},
372−year = {2010}
373−}
374−@inproceedings{Wadler1989,
375−abstract = {From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds' abstraction theorem for the polymorphic lambda calculus.},
376−author = {Wadler, Philip},
377−booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
378−doi = {10.1145/99370.99404},
379−file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},
380−isbn = {0897913280},
381−number = {June},
382−pages = {347--359},
383−publisher = {ACM},
384−series = {FPCA '89},
385−title = {{Theorems for free!}},
386−url = {http://portal.acm.org/citation.cfm?id=99404},
387−year = {1989}
388−}
389−@article{Altenkirch2010a,
390−abstract = {We begin by revisiting the idea of using a universe of types to write generic programs in a dependently typed setting by constructing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Positive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach presented here we are able to represent all of Epigrams datatypes within Epigram including the universe of datatypes itself.},
391−author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},
392−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
393−journal = {Citeseer},
394−publisher = {Citeseer},
395−title = {{Generic Programming with Dependent Types}},
396−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf},
397−year = {2010}
398−}
399−@inproceedings{l,
400−author = {L\"{a}mmel, R. and Jones, S.P.},
401−booktitle = {ACM SIGPLAN Notices},
402−file = {:home/edwin/Research/Papers/Mendeley/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},
403−number = {3},
404−pages = {26--37},
405−publisher = {ACM},
406−title = {{Scrap your boilerplate: a practical design pattern for generic programming}},
407−url = {http://dl.acm.org/citation.cfm?id=640136.604179},
408−volume = {38},
409−year = {2003}
410−}
411−@inproceedings{Xi1999,
412−abstract = {Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.},
413−author = {Xi, Hongwei and Pfenning, Frank},
414−booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},
415−doi = {10.1145/292540.292560},
416−file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},
417−isbn = {1581130953},
418−issn = {07439016},
419keywords = {Dependent Types},
301keywords = {Dependent Types},
420mendeley-tags = {Dependent Types},
302mendeley-tags = {Dependent Types},
421−organization = {Carnegie Mellon University},
303+school = {University of Durham},
422−pages = {214--227},
304+title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},
423−publisher = {ACM Press},
305+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf},
424−series = {POPL '99},
425−title = {{Dependent types in practical programming}},
426−url = {http://portal.acm.org/citation.cfm?doid=292540.292560},
427−volume = {26},
428−year = {1999}
429−}
430−@book{Approach2012,
431−author = {Hunt, Andrew and Thomas, David},
432−booktitle = {Carcinogenesis},
433−doi = {10.1093/carcin/bgs054},
434−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
435−isbn = {020161622X},
436−issn = {1460-2180},
437−number = {3},
438−pmid = {22383472},
439−title = {{The Pragmatic Programmer Chapter 2}},
440−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
441−volume = {33}
442−}
443−@article{Miller1992,
444−author = {Miller, D},
445−file = {:home/edwin/Research/Papers/Mendeley/Miller/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},
446−journal = {Journal of symbolic computation},
447−title = {{Unification under a mixed prefix}},
448−url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},
449−year = {1992}
306+year = {2005}
450−}
451−@misc{Interface2012a,
452−author = {Kreibich, Jay A.},
453−doi = {10.1093/epirev/mxr031},
454−file = {:home/edwin/Research/Papers/Mendeley/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
455−isbn = {9781449394592},
456−issn = {1478-6729},
457−pmid = {22215642},
458−title = {{Using SQLite Chapter 7}}
459}
307}
460−@inproceedings{Brady2006b,
308+@inproceedings{Brady2011a,
309+address = {New York, New York, USA},
461author = {Brady, Edwin},
310author = {Brady, Edwin},
462−booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},
311+booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},
312+doi = {10.1145/1929529.1929536},
463−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
313+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},
464−isbn = {978-3-540-74129-9},
314+isbn = {9781450304870},
315+keywords = {Dependent Types,data description,dependent types},
316+mendeley-tags = {Dependent Types},
465−month = sep,
317+month = jan,
466−pages = {145----162},
318+publisher = {ACM Press},
467−title = {{Ivor, a proof engine}},
319+title = {{Idris --- Systems Programming Meets Full Dependent Types}},
468−url = {http://dl.acm.org/citation.cfm?id=1757028.1757037},
320+url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
469−year = {2006}
470−}
471−@misc{TheMendeleySupportTeam2011a,
472−abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
473−address = {London},
474−author = {{The Mendeley Support Team}},
475−booktitle = {Mendeley Desktop},
476−file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
477−keywords = {Mendeley,how-to,user manual},
478−pages = {1--16},
479−publisher = {Mendeley Ltd.},
480−title = {{Getting Started with Mendeley}},
481−url = {http://www.mendeley.com},
482year = {2011}
321year = {2011}
483}
322}
484−@book{peyton1987implementation,
485−author = {{Peyton Jones}, S.L.},
486−publisher = {Prentice-Hall, Inc.},
487−title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}},
488−url = {http://dl.acm.org/citation.cfm?id=1096899},
489−year = {1987}
490−}
491−@article{dybjer1994inductive,
492−author = {Dybjer, P.},
493−journal = {Formal aspects of computing},
494−number = {4},
495−pages = {440--465},
496−publisher = {Springer},
497−title = {{Inductive families}},
498−url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
499−volume = {6},
500−year = {1994}
501−}
502−@inproceedings{lempsink2009type,
503−author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},
504−booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},
505−file = {:home/edwin/Research/Papers/Mendeley/Lempsink, Leather, L\"{o}h/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},
506−pages = {61--72},
507−publisher = {ACM},
508−title = {{Type-safe diff for families of datatypes}},
509−url = {http://dl.acm.org/citation.cfm?id=1596624},
510−year = {2009}
511−}
512−@misc{The2012b,
513−author = {Brooks, Fred},
514−doi = {10.1093/epirev/mxr031},
515−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
516−isbn = {9780321702081},
517−issn = {1478-6729},
518−pmid = {22215642},
519−title = {{The Design of Design Chapter 1}}
520−}
521−@book{Brady2012,
522−author = {Hunt, Andrew and Thomas, David},
523−booktitle = {Carcinogenesis},
524−doi = {10.1093/carcin/bgs054},
525−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
526−isbn = {020161622X},
527−issn = {1460-2180},
528−number = {3},
529−pmid = {22383472},
530−title = {{The Pragmatic Programmer Chapter 5}},
531−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
532−volume = {33}
533−}
534−@inproceedings{Pasalic2002,
535−author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},
536−booktitle = {International Conference on Functional Programming},
537−doi = {10.1145/583852.581499},
538−file = {:home/edwin/Research/Papers/Mendeley/Pa\v{s}alic, Taha, Sheard/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},
539−isbn = {1-58113-487-8},
540−issn = {03621340},
541−keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},
542−month = sep,
543−number = {9},
544−pages = {218--229},
545−title = {{Tagless staged interpreters for typed languages}},
546−url = {http://dl.acm.org/citation.cfm?id=583852.581499},
547−volume = {37},
548−year = {2002}
549−}
550@misc{dagand2011transporting,
323@misc{dagand2011transporting,
551author = {Dagand, Pierre-Evariste and McBride, Conor},
324author = {Dagand, Pierre-Evariste and McBride, Conor},
552file = {:home/edwin/Research/Papers/Mendeley/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
325file = {:home/edwin/Research/Papers/Mendeley/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
@@ -554,13 +327,6 @@ title = {{Transporting Functions across Ornaments}},
554url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},
327url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},
555year = {2011}
328year = {2011}
556}
329}
557−@article{Okasaki1993,
558−author = {Okasaki, Chris},
559−file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
560−journal = {Journal of functional programming},
561−title = {{Red-Black Trees in A Functional Setting}},
562−year = {1993}
563−}
564@inproceedings{taha2004gentle,
330@inproceedings{taha2004gentle,
565author = {Taha, W.},
331author = {Taha, W.},
566booktitle = {Domain-Specific Program Generation},
332booktitle = {Domain-Specific Program Generation},
@@ -570,42 +336,25 @@ title = {{A gentle introduction to multi-stage programming}},
570url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},
336url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},
571year = {2004}
337year = {2004}
572}
338}
573−@inproceedings{pj2006gadts,
339+@inproceedings{augustsson2008paradise,
574−author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
340+author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
575−booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
341+booktitle = {International Conference on Functional Programming},
576−file = {:home/edwin/Research/Papers/Mendeley/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
342+file = {:home/edwin/Research/Papers/Mendeley/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},
577number = {9},
343number = {9},
578−pages = {50--61},
344+pages = {225--228},
579publisher = {ACM},
345publisher = {ACM},
580−title = {{Simple unification-based type inference for GADTs}},
346+title = {{Paradise: a two-stage DSL embedded in Haskell}},
581−url = {http://dl.acm.org/citation.cfm?id=1159811},
347+url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},
582−volume = {41},
348+volume = {43},
583−year = {2006}
349+year = {2008}
584}
350}
585−@misc{altenkirch2008nσ,
351+@misc{altenkirch2005dependent,
586−author = {Altenkirch, T. and Oury, N.},
352+author = {Altenkirch, T. and McBride, C. and McKinna, J.},
353+booktitle = {Manuscript, available online},
587−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
354+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
588−title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},
355+title = {{Why dependent types matter}},
589−url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},
356+url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},
590−year = {2008}
357+year = {2005}
591−}
592−@misc{Nodes2012a,
593−author = {Brooks, Fred},
594−doi = {10.1093/epirev/mxr031},
595−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
596−isbn = {9780321702081},
597−issn = {1478-6729},
598−pmid = {22215642},
599−title = {{The Design of Design Chapter 3}}
600−}
601−@article{Haskell2012a,
602−author = {Biancuzzi, F and Warden, S},
603−doi = {10.1093/epirev/mxr031},
604−file = {:home/edwin/Research/Papers/Mendeley/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
605−isbn = {9780596801670},
606−issn = {1478-6729},
607−pmid = {22215642},
608−title = {{Masterminds of Programming Chapter 8}}
609}
358}
610@article{Xi1998,
359@article{Xi1998,
611abstract = {We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.},
360abstract = {We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.},
@@ -626,82 +375,6 @@ url = {http://portal.acm.org/citation.cfm?doid=277652.277732},
626volume = {33},
375volume = {33},
627year = {1998}
376year = {1998}
628}
377}
629−@inproceedings{morris2006exploring,
630−author = {Morris, P. and Altenkirch, T. and McBride, C.},
631−booktitle = {Types for Proofs and Programs},
632−file = {:home/edwin/Research/Papers/Mendeley/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},
633−pages = {252--267},
634−publisher = {Springer},
635−title = {{Exploring the regular tree types}},
636−url = {http://www.springerlink.com/index/f9p1317716614834.pdf},
637−year = {2006}
638−}
639−@article{landin1966next,
640−author = {Landin, P.J.},
641−file = {:home/edwin/Research/Papers/Mendeley/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
642−journal = {Communications of the ACM},
643−number = {3},
644−pages = {157--166},
645−publisher = {ACM},
646−title = {{The next 700 programming languages}},
647−url = {http://dl.acm.org/citation.cfm?id=365257 )},
648−volume = {9},
649−year = {1966}
650−}
651−@phdthesis{Brady2005,
652−author = {Brady, Edwin},
653−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
654−keywords = {Dependent Types},
655−mendeley-tags = {Dependent Types},
656−school = {University of Durham},
657−title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},
658−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf},
659−year = {2005}
660−}
661−@inproceedings{Brady2011a,
662−address = {New York, New York, USA},
663−author = {Brady, Edwin},
664−booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},
665−doi = {10.1145/1929529.1929536},
666−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},
667−isbn = {9781450304870},
668−keywords = {Dependent Types,data description,dependent types},
669−mendeley-tags = {Dependent Types},
670−month = jan,
671−publisher = {ACM Press},
672−title = {{Idris --- Systems Programming Meets Full Dependent Types}},
673−url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
674−year = {2011}
675−}
676−@article{Altenkirch2010,
677−abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
678−author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas},
679−doi = {10.1007/978-3-642-12251-4_5},
680−editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
681−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
682−isbn = {9783642122507},
683−journal = {Computing},
684−number = {Sheard 2005},
685−pages = {40--55},
686−publisher = {Springer Berlin Heidelberg},
687−series = {Lecture Notes in Computer Science},
688−title = {{Dependent Types without the Sugar}},
689−url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
690−volume = {6009},
691−year = {2010}
692−}
693−@inproceedings{augustsson2008paradise,
694−author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
695−booktitle = {International Conference on Functional Programming},
696−file = {:home/edwin/Research/Papers/Mendeley/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},
697−number = {9},
698−pages = {225--228},
699−publisher = {ACM},
700−title = {{Paradise: a two-stage DSL embedded in Haskell}},
701−url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},
702−volume = {43},
703−year = {2008}
704−}
705@inproceedings{augustsson1999exercise,
378@inproceedings{augustsson1999exercise,
706author = {Augustsson, L. and Carlsson, M.},
379author = {Augustsson, L. and Carlsson, M.},
707booktitle = {In Workshop on Dependent Types in Programming, Gothenburg},
380booktitle = {In Workshop on Dependent Types in Programming, Gothenburg},
@@ -723,18 +396,6 @@ url = {http://journals.cambridge.org/abstract_S0956796811000207},
723volume = {21},
396volume = {21},
724year = {2011}
397year = {2011}
725}
398}
726−@article{fisher2006next,
727−author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},
728−file = {:home/edwin/Research/Papers/Mendeley/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},
729−journal = {Journal of the ACM},
730−number = {2},
731−pages = {1--51},
732−publisher = {ACM},
733−title = {{The next 700 data description languages}},
734−url = {http://dl.acm.org/citation.cfm?id=1111039},
735−volume = {15},
736−year = {2010}
737−}
738@inproceedings{norell2009dependently,
399@inproceedings{norell2009dependently,
739author = {Norell, Ulf},
400author = {Norell, Ulf},
740booktitle = {Advanced Functional Programming},
401booktitle = {Advanced Functional Programming},
@@ -781,14 +442,50 @@ title = {{Typing Haskell in Haskell}},
781url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
442url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
782year = {1999}
443year = {1999}
783}
444}
784−@article{Epstein2011,
445+@article{Altenkirch2010,
785−author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},
446+abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
786−institution = {Microsoft Research},
447+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas},
787−journal = {researchmicrosoftcom},
448+doi = {10.1007/978-3-642-12251-4_5},
449+editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
450+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
451+isbn = {9783642122507},
452+journal = {Computing},
788−number = {Section 8},
453+number = {Sheard 2005},
789−pages = {1--12},
454+pages = {40--55},
790−title = {{Haskell for the cloud}},
455+publisher = {Springer Berlin Heidelberg},
791−url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf},
456+series = {Lecture Notes in Computer Science},
457+title = {{Dependent Types without the Sugar}},
458+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
459+volume = {6009},
460+year = {2010}
461+}
462+@book{Bertot2004,
463+author = {Bertot, Yves and Cast\'{e}ran, Pierre},
464+publisher = {Springer},
465+title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},
466+url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},
467+year = {2004}
468+}
469+@book{The2012,
470+author = {Hunt, Andrew and Thomas, David},
471+booktitle = {Carcinogenesis},
472+doi = {10.1093/carcin/bgs054},
473+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
474+isbn = {020161622X},
475+issn = {1460-2180},
476+number = {3},
477+pmid = {22383472},
478+title = {{The Pragmatic Programmer Chapter 3}},
479+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
480+volume = {33}
481+}
482+@inproceedings{ko2011modularising,
483+author = {Ko, H.S. and Gibbons, J.},
484+booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
485+pages = {13--24},
486+publisher = {ACM},
487+title = {{Modularising inductive families}},
488+url = {http://dl.acm.org/citation.cfm?id=2036921},
792year = {2011}
489year = {2011}
793}
490}
794@article{danielsson2011parsing,
491@article{danielsson2011parsing,
@@ -828,28 +525,17 @@ title = {{Programming in Idris : a tutorial}},
828url = {http://idris-lang.org/tutorial},
525url = {http://idris-lang.org/tutorial},
829year = {2012}
526year = {2012}
830}
527}
831−@book{An2012,
528+@inproceedings{madhavapeddy2007melange,
832−author = {Fowler, Martin},
529+author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
833−booktitle = {Carcinogenesis},
530+booktitle = {ACM SIGOPS Operating Systems Review},
834−doi = {10.1093/carcin/bgs054},
835−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
531+file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},
836−isbn = {9780132107549},
837−issn = {1460-2180},
838number = {3},
532number = {3},
839−pmid = {22383472},
840−title = {{Domain Specific Languages Chapter 1}},
841−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
842−volume = {33}
843−}
844−@inproceedings{ko2011modularising,
845−author = {Ko, H.S. and Gibbons, J.},
846−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
847−file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
848−pages = {13--24},
533+pages = {101--114},
849publisher = {ACM},
534publisher = {ACM},
850−title = {{Modularising inductive families}},
535+title = {{Melange: creating a functional internet}},
851−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},
536+url = {http://dl.acm.org/citation.cfm?id=1273009},
537+volume = {41},
852−year = {2011}
538+year = {2007}
853}
539}
854@inproceedings{Augustsson1998,
540@inproceedings{Augustsson1998,
855abstract = {Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value , and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts. Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.},
541abstract = {Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value , and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts. Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.},
@@ -877,6 +563,23 @@ title = {{Epic --- A Library for Generating Compilers}},
877url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},
563url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},
878year = {2011}
564year = {2011}
879}
565}
566+@article{Epstein2011,
567+author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},
568+institution = {Microsoft Research},
569+journal = {researchmicrosoftcom},
570+number = {Section 8},
571+pages = {1--12},
572+title = {{Haskell for the cloud}},
573+url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf},
574+year = {2011}
575+}
576+@book{Hunt,
577+author = {Hunt, Andrew and Thomas, David},
578+booktitle = {Design},
579+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
580+isbn = {020161622X},
581+title = {{The Pragmatic Programmer Chapter 4}}
582+}
880@inproceedings{swierstra2007beauty,
583@inproceedings{swierstra2007beauty,
881author = {Swierstra, W. and Altenkirch, T.},
584author = {Swierstra, W. and Altenkirch, T.},
882booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
585booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
@@ -887,42 +590,43 @@ title = {{Beauty in the beast}},
887url = {http://dl.acm.org/citation.cfm?id=1291206},
590url = {http://dl.acm.org/citation.cfm?id=1291206},
888year = {2007}
591year = {2007}
889}
592}
890−@inproceedings{Brady2010,
593+@inproceedings{bradyresource,
891author = {Brady, Edwin and Hammond, Kevin},
594author = {Brady, Edwin and Hammond, Kevin},
892−booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
595+booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},
893−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},
596+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},
894−isbn = {9781605587943},
597+pages = {242----257},
895−keywords = {Dependent Types,code generation gives,contrast,dependent types,efficient,harder,however,implementation,likely efficient,ness interpreter,partial evaluation,resulting implementation,un,verify its correctness},
598+title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},
896−mendeley-tags = {Dependent Types},
599+url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},
600+year = {2012}
601+}
602+@article{fisher2006next,
603+author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},
604+file = {:home/edwin/Research/Papers/Mendeley/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},
605+journal = {Journal of the ACM},
606+number = {2},
897−pages = {297--308},
607+pages = {1--51},
898publisher = {ACM},
608publisher = {ACM},
899−title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},
609+title = {{The next 700 data description languages}},
900−url = {http://portal.acm.org/citation.cfm?id=1863587},
610+url = {http://dl.acm.org/citation.cfm?id=1111039},
611+volume = {15},
901year = {2010}
612year = {2010}
902}
613}
903−@misc{The2012c,
614+@book{Bird2010,
904−author = {Robbins, A and Hannah, E and Lamb, L},
615+author = {Bird, Richard},
905−doi = {10.1093/epirev/mxr031},
906−file = {:home/edwin/Research/Papers/Mendeley/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
616+file = {:home/edwin/Research/Papers/Mendeley/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
907−isbn = {9780596529833},
617+isbn = {9780521513388},
908−issn = {1478-6729},
618+title = {{Pearls of Functional Algorithm Design}},
909−pmid = {22215642},
619+year = {2010}
910−title = {{Learning the vi and Vim Editors}}
911}
620}
912−@misc{altenkirch2005dependent,
621+@inproceedings{stump2010resource,
913−author = {Altenkirch, T. and McBride, C. and McKinna, J.},
622+author = {Stump, A. and Austin, E.},
914−booktitle = {Manuscript, available online},
623+booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},
915−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
624+file = {:home/edwin/Research/Papers/Mendeley/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},
916−title = {{Why dependent types matter}},
625+pages = {27--38},
917−url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},
626+publisher = {ACM},
627+title = {{Resource typing in Guru}},
628+url = {http://dl.acm.org/citation.cfm?id=1707796},
918−year = {2005}
629+year = {2010}
919−}
920−@book{Hunt,
921−author = {Hunt, Andrew and Thomas, David},
922−booktitle = {Design},
923−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
924−isbn = {020161622X},
925−title = {{The Pragmatic Programmer Chapter 4}}
926}
630}
927@inproceedings{taha1997multi,
631@inproceedings{taha1997multi,
928author = {Taha, W. and Sheard, T.},
632author = {Taha, W. and Sheard, T.},
@@ -935,66 +639,6 @@ url = {http://dl.acm.org/citation.cfm?id=259019},
935volume = {32},
639volume = {32},
936year = {1997}
640year = {1997}
937}
641}
938−@book{Philosophy2012,
939−author = {Hunt, Andrew and Thomas, David},
940−booktitle = {Carcinogenesis},
941−doi = {10.1093/carcin/bgs054},
942−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
943−isbn = {020161622X},
944−issn = {1460-2180},
945−number = {3},
946−pmid = {22383472},
947−title = {{The Pragmatic Programmer Chapter 1}},
948−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
949−volume = {33}
950−}
951−@inproceedings{bradyresource,
952−author = {Brady, Edwin and Hammond, Kevin},
953−booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},
954−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},
955−pages = {242----257},
956−title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},
957−url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},
958−year = {2012}
959−}
960−@book{The2012,
961−author = {Hunt, Andrew and Thomas, David},
962−booktitle = {Carcinogenesis},
963−doi = {10.1093/carcin/bgs054},
964−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
965−isbn = {020161622X},
966−issn = {1460-2180},
967−number = {3},
968−pmid = {22383472},
969−title = {{The Pragmatic Programmer Chapter 3}},
970−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
971−volume = {33}
972−}
973−@book{Bird2010,
974−author = {Bird, Richard},
975−file = {:home/edwin/Research/Papers/Mendeley/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
976−isbn = {9780521513388},
977−title = {{Pearls of Functional Algorithm Design}},
978−year = {2010}
979−}
980−@inproceedings{stump2010resource,
981−author = {Stump, A. and Austin, E.},
982−booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},
983−file = {:home/edwin/Research/Papers/Mendeley/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},
984−pages = {27--38},
985−publisher = {ACM},
986−title = {{Resource typing in Guru}},
987−url = {http://dl.acm.org/citation.cfm?id=1707796},
988−year = {2010}
989−}
990−@article{McBride2007,
991−author = {McBride, Conor and Paterson, Ross},
992−file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
993−journal = {Journal of functional programming},
994−title = {{Applicative programming with effects}},
995−url = {http://journals.cambridge.org/abstract_S0956796807006326},
996−year = {2007}
997−}
998@article{Wadler2001,
642@article{Wadler2001,
999abstract = {The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.},
643abstract = {The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.},
1000author = {Wadler, Philip},
644author = {Wadler, Philip},
@@ -1013,18 +657,6 @@ url = {http://www.springerlink.com/index/715264614rh13340.pdf},
1013volume = {925},
657volume = {925},
1014year = {2001}
658year = {2001}
1015}
659}
1016−@inproceedings{madhavapeddy2007melange,
1017−author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
1018−booktitle = {ACM SIGOPS Operating Systems Review},
1019−file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},
1020−number = {3},
1021−pages = {101--114},
1022−publisher = {ACM},
1023−title = {{Melange: creating a functional internet}},
1024−url = {http://dl.acm.org/citation.cfm?id=1273009},
1025−volume = {41},
1026−year = {2007}
1027−}
1028@article{Hoare1978,
660@article{Hoare1978,
1029abstract = {This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of a familiar programming exercises.},
661abstract = {This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of a familiar programming exercises.},
1030author = {Hoare, C A R},
662author = {Hoare, C A R},
@@ -1044,16 +676,44 @@ url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},
1044volume = {21},
676volume = {21},
1045year = {1978}
677year = {1978}
1046}
678}
1047−@phdthesis{norell2007thesis,
679+@book{Philosophy2012,
1048−author = {Norell, Ulf},
680+author = {Hunt, Andrew and Thomas, David},
1049−file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
681+booktitle = {Carcinogenesis},
1050−keywords = {Dependent Types},
682+doi = {10.1093/carcin/bgs054},
683+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
684+isbn = {020161622X},
685+issn = {1460-2180},
686+number = {3},
687+pmid = {22383472},
688+title = {{The Pragmatic Programmer Chapter 1}},
689+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
690+volume = {33}
691+}
692+@book{While2012,
693+author = {Hunt, Andrew and Thomas, David},
694+booktitle = {Carcinogenesis},
695+doi = {10.1093/carcin/bgs054},
696+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
697+isbn = {020161622X},
698+issn = {1460-2180},
699+number = {3},
700+pmid = {22383472},
701+title = {{The Pragmatic Programmer Chapter 6}},
702+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
703+volume = {33}
704+}
705+@inproceedings{Brady2010,
706+author = {Brady, Edwin and Hammond, Kevin},
707+booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
708+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},
709+isbn = {9781605587943},
710+keywords = {Dependent Types,code generation gives,contrast,dependent types,efficient,harder,however,implementation,likely efficient,ness interpreter,partial evaluation,resulting implementation,un,verify its correctness},
1051mendeley-tags = {Dependent Types},
711mendeley-tags = {Dependent Types},
712+pages = {297--308},
1052−publisher = {Citeseer},
713+publisher = {ACM},
1053−school = {Chalmers University of Technology},
714+title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},
1054−title = {{Towards a practical programming language based on dependent type theory}},
715+url = {http://portal.acm.org/citation.cfm?id=1863587},
1055−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
1056−year = {2007}
716+year = {2010}
1057}
717}
1058@inproceedings{Visser2008,
718@inproceedings{Visser2008,
1059author = {Visser, E},
719author = {Visser, E},
@@ -1062,6 +722,19 @@ title = {{WebDSL: A case study in domain-specific language engineering}},
1062url = {http://www.springerlink.com/index/A3213003X6268032.pdf},
722url = {http://www.springerlink.com/index/A3213003X6268032.pdf},
1063year = {2008}
723year = {2008}
1064}
724}
725+@misc{TheMendeleySupportTeam2011a,
726+abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
727+address = {London},
728+author = {{The Mendeley Support Team}},
729+booktitle = {Mendeley Desktop},
730+file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
731+keywords = {Mendeley,how-to,user manual},
732+pages = {1--16},
733+publisher = {Mendeley Ltd.},
734+title = {{Getting Started with Mendeley}},
735+url = {http://www.mendeley.com},
736+year = {2011}
737+}
1065@inproceedings{Brady2005a,
738@inproceedings{Brady2005a,
1066author = {Brady, E and Hammond, K},
739author = {Brady, E and Hammond, K},
1067booktitle = {Implementation and Application of Functional \ldots},
740booktitle = {Implementation and Application of Functional \ldots},
@@ -1072,40 +745,6 @@ title = {{A dependently typed framework for static analysis of program execution
1072url = {http://www.springerlink.com/index/P446P2HH70107759.pdf},
745url = {http://www.springerlink.com/index/P446P2HH70107759.pdf},
1073year = {2005}
746year = {2005}
1074}
747}
1075−@book{Bertot2004,
1076−author = {Bertot, Yves and Cast\'{e}ran, Pierre},
1077−publisher = {Springer},
1078−title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},
1079−url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},
1080−year = {2004}
1081−}
1082−@inproceedings{ko2011modularising,
1083−author = {Ko, H.S. and Gibbons, J.},
1084−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
1085−pages = {13--24},
1086−publisher = {ACM},
1087−title = {{Modularising inductive families}},
1088−url = {http://dl.acm.org/citation.cfm?id=2036921},
1089−year = {2011}
1090−}
1091−@inproceedings{barras2008implicit,
1092−author = {Barras, B. and Bernardo, B.},
1093−booktitle = {Foundations of Software Science and Computational Structures},
1094−file = {:home/edwin/Research/Papers/Mendeley/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},
1095−pages = {365--379},
1096−publisher = {Springer},
1097−title = {{The implicit calculus of constructions as a programming language with dependent types}},
1098−url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
1099−year = {2008}
1100−}
1101−@inproceedings{Fournet2011,
1102−author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},
1103−booktitle = {Foundations of security analysis and design {VI}},
1104−file = {:home/edwin/Research/Papers/Mendeley/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},
1105−title = {{Cryptographic verification by typing for a sample protocol implementation}},
1106−url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
1107−year = {2010}
1108−}
1109@inproceedings{madhavapeddy2010turning,
748@inproceedings{madhavapeddy2010turning,
1110author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
749author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
1111booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
750booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
@@ -1115,6 +754,14 @@ title = {{Turning down the LAMP: software specialisation for the cloud}},
1115url = {http://dl.acm.org/citation.cfm?id=1863114},
754url = {http://dl.acm.org/citation.cfm?id=1863114},
1116year = {2010}
755year = {2010}
1117}
756}
757+@article{McBride2007,
758+author = {McBride, Conor and Paterson, Ross},
759+file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
760+journal = {Journal of functional programming},
761+title = {{Applicative programming with effects}},
762+url = {http://journals.cambridge.org/abstract_S0956796807006326},
763+year = {2007}
764+}
1118@inproceedings{bhargavan2010modular,
765@inproceedings{bhargavan2010modular,
1119author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},
766author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},
1120booktitle = {ACM Sigplan Notices},
767booktitle = {ACM Sigplan Notices},
@@ -1135,12 +782,21 @@ title = {{An analysis of Girard's paradox}},
1135url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},
782url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},
1136year = {1986}
783year = {1986}
1137}
784}
1138−@misc{Abel1998,
785+@inproceedings{Augustsson1985,
1139−author = {Abel, Andreas},
786+address = {Berlin, Heidelberg},
1140−booktitle = {Language},
787+author = {Augustsson, Lennart},
1141−file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
788+booktitle = {Functional Programming Languages and Computer Architecture},
1142−title = {{foetus - Termination Checker for Simple Functional Programs}},
789+doi = {10.1007/3-540-15975-4},
790+editor = {Jouannaud, Jean-Pierre},
791+isbn = {978-3-540-15975-9},
792+keywords = {Computer Science},
793+pages = {368----381},
794+publisher = {Springer Berlin Heidelberg},
795+series = {Lecture Notes in Computer Science},
796+title = {{Compiling Pattern Matching}},
797+url = {http://www.springerlink.com/content/y647423656557505/},
798+volume = {201},
1143−year = {1998}
799+year = {1985}
1144}
800}
1145@misc{Bloat,
801@misc{Bloat,
1146author = {Brooks, Fred},
802author = {Brooks, Fred},
@@ -1148,6 +804,16 @@ file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Desig
1148isbn = {9780321702081},
804isbn = {9780321702081},
1149title = {{The Design of Design Chapter 4}}
805title = {{The Design of Design Chapter 4}}
1150}
806}
807+@inproceedings{barras2008implicit,
808+author = {Barras, B. and Bernardo, B.},
809+booktitle = {Foundations of Software Science and Computational Structures},
810+file = {:home/edwin/Research/Papers/Mendeley/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},
811+pages = {365--379},
812+publisher = {Springer},
813+title = {{The implicit calculus of constructions as a programming language with dependent types}},
814+url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
815+year = {2008}
816+}
1151@misc{Brady2012c,
817@misc{Brady2012c,
1152author = {Brooks, Fred},
818author = {Brooks, Fred},
1153doi = {10.1093/epirev/mxr031},
819doi = {10.1093/epirev/mxr031},
@@ -1160,31 +826,31 @@ pmid = {22215642},
1160title = {{The Design of Design Chapter 5}},
826title = {{The Design of Design Chapter 5}},
1161volume = {34}
827volume = {34}
1162}
828}
1163−@inproceedings{atkey2009unembedding,
829+@inproceedings{Fournet2011,
1164−author = {Atkey, R. and Lindley, S. and Yallop, J.},
830+author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},
1165−booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
831+booktitle = {Foundations of security analysis and design {VI}},
1166−pages = {37--48},
832+file = {:home/edwin/Research/Papers/Mendeley/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},
1167−publisher = {ACM},
833+title = {{Cryptographic verification by typing for a sample protocol implementation}},
1168−title = {{Unembedding domain-specific languages}},
834+url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
1169−url = {http://dl.acm.org/citation.cfm?id=1596644},
1170−year = {2009}
1171−}
1172−@article{loh2010tutorial,
1173−author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},
1174−file = {:home/edwin/Research/Papers/Mendeley/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},
1175−journal = {Fundamenta Informaticae},
1176−number = {2},
1177−pages = {177--207},
1178−publisher = {IOS Press},
1179−title = {{A tutorial implementation of a dependently typed lambda calculus}},
1180−url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},
1181−volume = {102},
1182year = {2010}
835year = {2010}
1183}
836}
1184−@article{mcbride2008functional,
837+@book{Choosing2012,
1185−author = {McBride, C. and Paterson, R.},
838+author = {Fowler, Martin},
1186−file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
839+booktitle = {Carcinogenesis},
1187−journal = {Journal of functional programming},
840+doi = {10.1093/carcin/bgs054},
841+file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
842+isbn = {9780132107549},
843+issn = {1460-2180},
844+number = {3},
845+pmid = {22383472},
846+title = {{Domain Specific Languages Chapter 6}},
847+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
848+volume = {33}
849+}
850+@article{mcbride2008functional,
851+author = {McBride, C. and Paterson, R.},
852+file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
853+journal = {Journal of functional programming},
1188number = {1},
854number = {1},
1189pages = {1--13},
855pages = {1--13},
1190publisher = {Cambridge Univ Press},
856publisher = {Cambridge Univ Press},
@@ -1202,18 +868,61 @@ title = {{Implicit syntax}},
1202url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
868url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
1203year = {1990}
869year = {1990}
1204}
870}
1205−@book{While2012,
871+@misc{altenkirch2008nσ,
1206−author = {Hunt, Andrew and Thomas, David},
872+author = {Altenkirch, T. and Oury, N.},
1207−booktitle = {Carcinogenesis},
873+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
1208−doi = {10.1093/carcin/bgs054},
874+title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},
1209−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
875+url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},
1210−isbn = {020161622X},
876+year = {2008}
1211−issn = {1460-2180},
877+}
1212−number = {3},
878+@misc{Abel1998,
1213−pmid = {22383472},
879+author = {Abel, Andreas},
1214−title = {{The Pragmatic Programmer Chapter 6}},
880+booktitle = {Language},
1215−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
881+file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
1216−volume = {33}
882+title = {{foetus - Termination Checker for Simple Functional Programs}},
883+year = {1998}
884+}
885+@misc{pollack1997believe,
886+author = {Pollack, R.},
887+file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
888+title = {{How to believe a machine-checked proof}},
889+url = {http://books.google.co.uk/books?hl=en&lr=&id=pLnKggT_In4C&oi=fnd&pg=PA205&dq=how+to+believe+a+machine+checked+proof&ots=c2OI8krqqA&sig=EF3QonGFVdOpYdKO1KmW6ljCkjY},
890+year = {1997}
891+}
892+@inproceedings{atkey2009unembedding,
893+author = {Atkey, R. and Lindley, S. and Yallop, J.},
894+booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
895+pages = {37--48},
896+publisher = {ACM},
897+title = {{Unembedding domain-specific languages}},
898+url = {http://dl.acm.org/citation.cfm?id=1596644},
899+year = {2009}
900+}
901+@inproceedings{oury2008power,
902+author = {Oury, N. and Swierstra, W.},
903+booktitle = {International Conference on Functional Programming},
904+file = {:home/edwin/Research/Papers/Mendeley/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
905+keywords = {Dependent Types},
906+mendeley-tags = {Dependent Types},
907+number = {9},
908+pages = {39--50},
909+publisher = {ACM},
910+title = {{The power of Pi}},
911+url = {http://dl.acm.org/citation.cfm?id=1411213},
912+volume = {43},
913+year = {2008}
914+}
915+@article{loh2010tutorial,
916+author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},
917+file = {:home/edwin/Research/Papers/Mendeley/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},
918+journal = {Fundamenta Informaticae},
919+number = {2},
920+pages = {177--207},
921+publisher = {IOS Press},
922+title = {{A tutorial implementation of a dependently typed lambda calculus}},
923+url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},
924+volume = {102},
925+year = {2010}
1217}
926}
1218@article{gordon2003authenticity,
927@article{gordon2003authenticity,
1219author = {Gordon, A.D. and Jeffrey, A.},
928author = {Gordon, A.D. and Jeffrey, A.},
@@ -1239,3 +948,294 @@ pmid = {22215642},
1239title = {{Security Engineering Chapter 18}},
948title = {{Security Engineering Chapter 18}},
1240volume = {34}
949volume = {34}
1241}
950}
951+@inproceedings{Sheard2005,
952+address = {New York, New York, USA},
953+author = {Sheard, Tim},
954+booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},
955+doi = {10.1145/1088348.1088356},
956+file = {:home/edwin/Research/Papers/Mendeley/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},
957+isbn = {159593071X},
958+keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},
959+month = sep,
960+pages = {74--85},
961+publisher = {ACM Press},
962+title = {{Putting curry-howard to work}},
963+url = {http://dl.acm.org/citation.cfm?id=1088348.1088356},
964+year = {2005}
965+}
966+@inproceedings{NanevskiAAMorrisett2008,
967+abstract = {We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions. The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which, abstracts the implementation details and ensures that the modules properly implement the finite map abstraction. Copyright 2008 ACM.},
968+author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},
969+booktitle = {International Conference on Functional Programming},
970+doi = {10.1145/1411204.1411237},
971+file = {:home/edwin/Research/Papers/Mendeley/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},
972+isbn = {9781595939197},
973+issn = {15232867},
974+keywords = {Dependent Types},
975+mendeley-tags = {Dependent Types},
976+number = {9},
977+pages = {229--240},
978+title = {{Ynot: Dependent types for imperative programs}},
979+url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},
980+volume = {43},
981+year = {2008}
982+}
983+@inproceedings{fisher2005pads,
984+author = {Fisher, K. and Gruber, R.},
985+booktitle = {ACM SIGPLAN Notices},
986+number = {6},
987+pages = {295--304},
988+publisher = {ACM},
989+title = {{PADS: a domain-specific language for processing ad hoc data}},
990+url = {http://dl.acm.org/citation.cfm?id=1065046},
991+volume = {40},
992+year = {2005}
993+}
994+@inproceedings{McBride2004b,
995+author = {McBride, Conor and McKinna, James},
996+booktitle = {Haskell Workshop},
997+file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},
998+title = {{I am not a number : I am a free variable}},
999+year = {2004}
1000+}
1001+@article{marlow2006making,
1002+author = {Marlow, S. and {Peyton Jones}, S.},
1003+file = {:home/edwin/Research/Papers/Mendeley/Marlow, Peyton Jones/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},
1004+journal = {Journal of Functional Programming},
1005+number = {4-5},
1006+pages = {415--449},
1007+publisher = {Cambridge University Press},
1008+title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}},
1009+url = {http://dl.acm.org/citation.cfm?id=1166018},
1010+volume = {16},
1011+year = {2006}
1012+}
1013+@article{landin1966next,
1014+author = {Landin, P.J.},
1015+file = {:home/edwin/Research/Papers/Mendeley/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
1016+journal = {Communications of the ACM},
1017+number = {3},
1018+pages = {157--166},
1019+publisher = {ACM},
1020+title = {{The next 700 programming languages}},
1021+url = {http://dl.acm.org/citation.cfm?id=365257 )},
1022+volume = {9},
1023+year = {1966}
1024+}
1025+@misc{Protocols2012a,
1026+author = {Anderson, Ross},
1027+doi = {10.1093/epirev/mxr031},
1028+file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
1029+isbn = {9780470068526},
1030+issn = {1478-6729},
1031+pmid = {22215642},
1032+title = {{Security Engineering Chapter 3}}
1033+}
1034+@inproceedings{Sculthorpe2009,
1035+author = {Sculthorpe, Neil and Nilsson, Henrik},
1036+booktitle = {International Conference on Functional Programming ({ICFP} '09)},
1037+file = {:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf;:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf},
1038+title = {{Safe functional reactive programming through dependent types}},
1039+url = {http://dl.acm.org/citation.cfm?id=1596558},
1040+year = {2009}
1041+}
1042+@book{Fowler,
1043+author = {Fowler, Martin},
1044+booktitle = {Language},
1045+file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
1046+isbn = {9780132107549},
1047+title = {{Domain Specific Languages Chapter 2}}
1048+}
1049+@article{Jones2003,
1050+abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},
1051+author = {Jones, Simon Peyton},
1052+editor = {Jones, Simon Peyton},
1053+isbn = {0521826144},
1054+journal = {Language},
1055+number = {1},
1056+publisher = {Cambridge University Press},
1057+title = {{Haskell 98 Language and Libraries The Revised Report}},
1058+url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},
1059+volume = {13},
1060+year = {2003}
1061+}
1062+@article{Brady2006a,
1063+author = {Brady, E and Hammond, K},
1064+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},
1065+journal = {\ldots of the 5th international conference on \ldots},
1066+keywords = {Dependent Types},
1067+mendeley-tags = {Dependent Types},
1068+title = {{A verified staged interpreter is a verified compiler}},
1069+url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},
1070+year = {2006}
1071+}
1072+@article{burrows1990,
1073+author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
1074+file = {:home/edwin/Research/Papers/Mendeley/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},
1075+journal = {ACM Transactions on Computer Systems},
1076+pages = {18----36},
1077+title = {{A logic of authentication}},
1078+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569},
1079+volume = {8},
1080+year = {1990}
1081+}
1082+@phdthesis{McBride1999,
1083+author = {McBride, Conor},
1084+file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
1085+keywords = {Dependent Types},
1086+mendeley-tags = {Dependent Types},
1087+school = {University of Edinburgh},
1088+title = {{Dependently typed functional programs and their proofs}},
1089+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
1090+year = {1999}
1091+}
1092+@article{mcbride2010ornamental,
1093+author = {McBride, Conor},
1094+file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
1095+journal = {Journal of Functional Programming},
1096+title = {{Ornamental algebras, algebraic ornaments}},
1097+url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},
1098+year = {2010}
1099+}
1100+@inproceedings{czarnecki2004dsl,
1101+author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},
1102+booktitle = {Domain-Specific Program Generation},
1103+file = {:home/edwin/Research/Papers/Mendeley/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},
1104+pages = {51--72},
1105+publisher = {Springer},
1106+title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},
1107+url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},
1108+year = {2004}
1109+}
1110+@article{Chapman2005epigram,
1111+author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},
1112+file = {:home/edwin/Research/Papers/Mendeley/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},
1113+journal = {Trends in Functional Programming},
1114+publisher = {Intellect Books},
1115+title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
1116+url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
1117+year = {2005}
1118+}
1119+@inproceedings{Levitation2010,
1120+author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},
1121+booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},
1122+doi = {10.1145/1932681.1863547},
1123+file = {:home/edwin/Research/Papers/Mendeley/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},
1124+isbn = {978-1-60558-794-3},
1125+issn = {03621340},
1126+keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},
1127+mendeley-tags = {Dependent Types},
1128+month = sep,
1129+number = {9},
1130+pages = {3},
1131+title = {{The gentle art of levitation}},
1132+url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},
1133+volume = {45},
1134+year = {2010}
1135+}
1136+@inproceedings{pj2006gadts,
1137+author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
1138+booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
1139+file = {:home/edwin/Research/Papers/Mendeley/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
1140+number = {9},
1141+pages = {50--61},
1142+publisher = {ACM},
1143+title = {{Simple unification-based type inference for GADTs}},
1144+url = {http://dl.acm.org/citation.cfm?id=1159811},
1145+volume = {41},
1146+year = {2006}
1147+}
1148+@article{McBride2004a,
1149+abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.},
1150+author = {McBride, Conor and McKinna, James},
1151+doi = {10.1017/S0956796803004829},
1152+file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
1153+issn = {09567968},
1154+journal = {Journal of Functional Programming},
1155+keywords = {Dependent Types},
1156+mendeley-tags = {Dependent Types},
1157+number = {1},
1158+pages = {69--111},
1159+publisher = {Cambridge University Press},
1160+title = {{The view from the left}},
1161+url = {http://www.journals.cambridge.org/abstract_S0956796803004829},
1162+volume = {14},
1163+year = {2004}
1164+}
1165+@article{Altenkirch2010a,
1166+abstract = {We begin by revisiting the idea of using a universe of types to write generic programs in a dependently typed setting by constructing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Positive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach presented here we are able to represent all of Epigrams datatypes within Epigram including the universe of datatypes itself.},
1167+author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},
1168+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
1169+journal = {Citeseer},
1170+publisher = {Citeseer},
1171+title = {{Generic Programming with Dependent Types}},
1172+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf},
1173+year = {2010}
1174+}
1175+@article{Steiner1988,
1176+author = {Steiner, JG},
1177+file = {:home/edwin/Research/Papers/Mendeley/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
1178+journal = {Proc. Winter USENIX Conference},
1179+title = {{Kerberos: An authentication service for open network systems}},
1180+url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},
1181+year = {1988}
1182+}
1183+@phdthesis{Okasaki1996,
1184+author = {Okasaki, Chris},
1185+file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
1186+school = {Carnegie Mellon University},
1187+title = {{Purely Functional Data Structures}},
1188+year = {1996}
1189+}
1190+@article{Abel2010,
1191+abstract = {Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.},
1192+author = {Abel, Andreas},
1193+file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
1194+journal = {EPTCS},
1195+pages = {1--15},
1196+title = {{MiniAgda: Integrating Sized and Dependent Types}},
1197+url = {http://arxiv.org/abs/1012.4896},
1198+volume = {43},
1199+year = {2010}
1200+}
1201+@inproceedings{Brady2006b,
1202+author = {Brady, Edwin},
1203+booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},
1204+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
1205+isbn = {978-3-540-74129-9},
1206+month = sep,
1207+pages = {145----162},
1208+title = {{Ivor, a proof engine}},
1209+url = {http://dl.acm.org/citation.cfm?id=1757028.1757037},
1210+year = {2006}
1211+}
1212+@article{Hughes1989,
1213+abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},
1214+author = {Hughes, J},
1215+chapter = {2},
1216+doi = {10.1093/comjnl/32.2.98},
1217+editor = {Turner, David A},
1218+file = {:home/edwin/Research/Papers/Mendeley/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
1219+institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},
1220+isbn = {0201172364},
1221+issn = {00104620},
1222+journal = {The Computer Journal},
1223+number = {2},
1224+pages = {98--107},
1225+publisher = {Br Computer Soc},
1226+title = {{Why Functional Programming Matters}},
1227+url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},
1228+volume = {32},
1229+year = {1989}
1230+}
1231+@article{mccann2000packet,
1232+author = {McCann, P.J. and Chandra, S.},
1233+journal = {ACM SIGCOMM Computer Communication Review},
1234+number = {4},
1235+pages = {321--333},
1236+publisher = {ACM},
1237+title = {{Packet types: abstract specification of network protocol messages}},
1238+url = {http://dl.acm.org/citation.cfm?id=347563},
1239+volume = {30},
1240+year = {2000}
1241+}
impl-paper/typechecking.tex+47−12
@@ -23,7 +23,7 @@ The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:
23\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.
23\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.
24\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.
24\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.
25\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the
25\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the
26−type of types.
26+type of types, and may be extended with other primitives.
27\end{itemize}
27\end{itemize}
28
28
29We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$,
29We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$,
@@ -106,7 +106,7 @@ is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\
106is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
106is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$
107then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
107then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of
108contractions and reversed contractions. Terms which are convertible are also said to
108contractions and reversed contractions. Terms which are convertible are also said to
109−be computationally equal.
109+be definitionally equal.
110The evaluator can also be extended by defining pattern matching functions, which
110The evaluator can also be extended by defining pattern matching functions, which
111will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
111will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern
112matching functions can be understood as extending the core language with high level
112matching functions can be understood as extending the core language with high level
@@ -151,6 +151,30 @@ be implemented in the usual way~\cite{loh2010tutorial}.
151\Rule{\Gamma\proves\RW{valid}}
151\Rule{\Gamma\proves\RW{valid}}
152{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
152{\Gamma\vdash\Type_n\Hab\Type_{n+1}}
153\\
153\\
154+\mathsf{Const}_1\:
155+\Rule{\Gamma\proves\RW{valid}}
156+{\Gamma\vdash\vi\Hab\TC{Int}}
157+\hg
158+\mathsf{Const}_2\:
159+\Rule{\Gamma\proves\RW{valid}}
160+{\Gamma\vdash\VV{str}\Hab\TC{String}}
161+\\
162+\mathsf{Const}_3\:
163+\Rule{\Gamma\proves\RW{valid}}
164+{\Gamma\vdash\TC{Int}\Hab\Type_0}
165+\hg
166+\mathsf{Const}_4\:
167+\Rule{\Gamma\proves\RW{valid}}
168+{\Gamma\vdash\TC{String}\Hab\Type_0}
169+\\
170+%\mathsf{Pat}_1\:
171+%\Rule{(\pat{\vx}{\vS})\in\Gamma}
172+%{\Gamma\vdash\vx\Hab\vS}
173+%\hg
174+%\mathsf{Pat}_2\:
175+%\Rule{(\pty{\vx}{\vS})\in\Gamma}
176+%{\Gamma\vdash\vx\Hab\vS}
177+\\
154\mathsf{Var}_1\:
178\mathsf{Var}_1\:
155\Rule{(\lam{\vx}{\vS})\in\Gamma}
179\Rule{(\lam{\vx}{\vS})\in\Gamma}
156{\Gamma\vdash\vx\Hab\vS}
180{\Gamma\vdash\vx\Hab\vS}
@@ -163,14 +187,6 @@ be implemented in the usual way~\cite{loh2010tutorial}.
163\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
187\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
164{\Gamma\vdash\vx\Hab\vS}
188{\Gamma\vdash\vx\Hab\vS}
165\\
189\\
166−%\mathsf{Pat}_1\:
167−%\Rule{(\pat{\vx}{\vS})\in\Gamma}
168−%{\Gamma\vdash\vx\Hab\vS}
169−%\hg
170−%\mathsf{Pat}_2\:
171−%\Rule{(\pty{\vx}{\vS})\in\Gamma}
172−%{\Gamma\vdash\vx\Hab\vS}
173−\\
174\mathsf{App}\:
190\mathsf{App}\:
175\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
191\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}
176{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
192{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}
@@ -230,7 +246,7 @@ defined collection of algebraic data types which can be parametrised over
230\remph{values} as well as types. An inductive family is declared
246\remph{values} as well as types. An inductive family is declared
231in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
247in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}
232as
248as
233−follows, using the de Bruijn telescope notation, $\tx$, to indicate a
249+follows, using vector notation, $\tx$, to indicate a
234sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
250sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
235
251
236\DM{
252\DM{
@@ -351,7 +367,7 @@ In order to implement pattern matching, we must separate the \remph{accessible}
351to match against it) if it is constructor headed, or a variable. Inaccessible patterns
367to match against it) if it is constructor headed, or a variable. Inaccessible patterns
352are converted to ``match anything'' patterns. We convert clauses to matchable pattern
368are converted to ``match anything'' patterns. We convert clauses to matchable pattern
353clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
369clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}.
354−We extend the telescope notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
370+We extend the vector notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the
355$\MO{Pat}$ operation across a list of arguments.
371$\MO{Pat}$ operation across a list of arguments.
356
372
357\FFIG{
373\FFIG{
@@ -444,6 +460,25 @@ to a telescope $\tx$ as $\vec{\MO{Op}}\:\tx$.
444In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
460In practice, for efficiency, pattern matching is implemented by compiling the match clauses to
445a tree of case expressions~\cite{Augustsson1985}.
461a tree of case expressions~\cite{Augustsson1985}.
446
462
463+\subsection{Totality checking}
464+
465+In order to ensure termination of type checking, and therefore its decidability,
466+we must distinguish terms for which evaluation definitely terminates, and
467+those which may diverge. \TT{} takes a simple but pragmatic and
468+effective approach to termination
469+checking: any functions which do not satisfy a syntactic constraint on recursive
470+calls are marked as \emph{partial}. Additionally, any function which calls a partial
471+function are uses a data type which is not strictly positive is also marked as
472+partial. The syntactic constraint we use is that a recursive call in a pattern
473+clause must have an argument which is structurally smaller than an input argument
474+in the same position. \TT{} also marks functions which do not cover all possible
475+inputs as partial. This totality checking is independent of the rest of the type
476+theory, and can be extended in future.
477+
478+This approach, separating the termination requirement from the type theory, means that
479+an \Idris{} programmer makes the decision about the importance of totality for each
480+function rather than having the totality requirement imposed by the type theory.
481+
447\subsection{From \Idris{} to \TT{}}
482\subsection{From \Idris{} to \TT{}}
448
483
449\TT{} is a very small language, consisting only of data declarations and pattern matching
484\TT{} is a very small language, consisting only of data declarations and pattern matching