a3569e5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some proofreading, filling in some gaps.

commita3569e57bb1a2a8c4cb7179dc797b2122ac4f8b9 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Apr 2012, 19:28 (15 years ago) parent2c5c768

8 files changed+993−900

compare with master

unifiedsplit

impl-paper/Makefile+1−1 impl-paper/conclusions.tex+14 impl-paper/elaboration.tex+52−33 impl-paper/hll.tex+39−16 impl-paper/impldtp.tex+8−8 impl-paper/intro.tex+4−2 impl-paper/library.bib+828−828 impl-paper/typechecking.tex+47−12

impl-paper/Makefile+1−1

@@ -3,7 +3,7 @@ PAPER = impldtp

33all: ${PAPER}.pdf .PHONY

55TEXFILES = ${PAPER}.tex intro.tex conclusions.tex hll.tex\

6− typechecking.tex elaboration.tex compiling.tex\

6+ typechecking.tex elaboration.tex \

77 syntax.tex

99DIAGS =

impl-paper/conclusions.tex+14

@@ -2,6 +2,13 @@

33\label{sect:discussion}

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.

9+Discuss performance (anecdotally, how big is the library and how long to check,

10+and relative to previous version).

11+

512\subsection{Related Work}

613

714Oleg~\cite{McBride1999} as inspiration. \Epigram{}~\cite{McBride2004a}.

@@ -17,4 +24,11 @@ type checks the high level language and produces a type correct core language.

1724Elaboration is effectively a type checker for the high level language, so we have

1825a hope of providing reasonable error messages related to the original code.]

1926

27+

2028\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

99high level declarations are translated into a \TT{} program consisting of

1010inductive families and pattern matching function definitions. We will need to

1111work at the \remph{declaration} level, and at the \remph{expression} level,

12−defining the following meta-operations which together constitute an algorithm

13−for elaborating \Idris{} programs to \TT{}.

12+defining the following meta-operations.

1413

1514\begin{itemize}

1615\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:

9089The \remph{hole queue} is a priority queue of names of hole and guess binders

9190$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$

9291in 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}

9493in the proof.

9594When 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

9796a new proof state, with an empty proof term, and using the high level definition

9897to direct the building of a final proof state, with a complete proof term.

9998

@@ -162,7 +161,8 @@ The system state is a tuple, $(\vC,\vA,\vI)$, containing:

162161\item Type class instances, $\vI$, containing dictionaries for type classes

163162\end{itemize}

164163

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

166166includes additional information such as syntax overloadings,

167167command line options, and optimisations, which do not concern us here. Elaboration

168168of 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$

226226if it cannot find such values. If successful, $\MO{Unify}$ will update the proof state.

227227\end{itemize}

228228

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

230230by the hole at the head of the hole queue in the proof state. They take the following form:

231231

232232\DM{

@@ -264,7 +264,8 @@ keeping $\vx$ at the head:

264264

265265An obvious difficulty is in ensuring that names are unique throughout a proof term.

266266In the implementation, we ensure that any hole created by the $\MO{Claim}$ tactic

267−has a unique name. In this paper, we will assume that all names are fresh.

267+has a unique name by checking against existing names in scope and modifying

268+the name if necessary. In this paper, we will assume that all created names are fresh.

268269

269270The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal

270271with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to

@@ -445,7 +446,8 @@ For example, consider the following simple

445446

446447We can build $\FN{id}$ either as a complete term, or by applying a sequence of tactics.

447448To 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:

449451

450452\DM{

451453\AR{

@@ -466,7 +468,9 @@ apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$:

466468}

467469

468470To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate

469−sequencing. Using this convention, we can build $\FN{id}$'s type and definition as shown

471+sequencing --- in the implementation we use wrapper functions for each tactic to

472+apply $\MO{RunTac}$.

473+Using this convention, we can build $\FN{id}$'s type and definition as shown

470474in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof

471475state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.

472476Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses,

@@ -566,8 +570,6 @@ a Coq proof script.

566570\va :: = & \ve & (\mbox{normal argument}) \\

567571\mid & \iarg{\vx}{\ve} & (\mbox{implicit argument with value}) \\

568572\mid & \carg{\ve} & (\mbox{explicit class instance})

569−\medskip\\

570−\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\

571573\end{array}

572574\medskip\\

573575\begin{array}{rll}

@@ -645,11 +647,11 @@ than one at a time.

645647%it's the global name after all and we do that by type).

646648

647649To 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

649651to update the proof state so that the hole in focus contains a representation

650652of the given expression, by applying tactics. We assume that the proof state

651653has 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

653655are building.

654656

655657\subsubsection{Elaborating variables and constants}

@@ -689,11 +691,13 @@ the current hole to the end of the queue with $\MO{Unfocus}$:

689691}

690692

691693On 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.

693697

694698\subsubsection{Elaborating bindings}

695699

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,

697701apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges

698702the $\MO{Attack}$:

699703

@@ -843,7 +847,8 @@ class instance arguments with the built-in $\MO{Instance}$ tactic (see Section

843847

844848The $\MO{Instance}$ tactic focuses on the given hole and searches the context for

845849a 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}.

847852

848853To elaborate a simple function application, of an arbitrary expression to an arbitrary

849854argument, we need not worry about implicit arguments or class constraints. Instead,

@@ -929,19 +934,20 @@ declaration.

929934

930935\subsubsection{Elaborating Pattern Matching}

931936

932−[Work clause by clause, $\MO{ElabClause}$ returns a left and right hand side, and

933−may have the side effect of adding things to the context, such as definitions in

934−$\iwhere$ clauses. Collect together in a full definition at the end.

935−

936−In the simplest case, no $\iwhere$ clause:]

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

940+to the global context, such as definitions in $\iwhere$ clauses.

941+First, let us consider the simplest case, with no $\iwhere$ clause:

937942

938943\DM{

939944\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?

940945}

941946

942947How 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

944−requires no change to the elaborator, is to define a type $\TC{Infer}$:

948+we do not know its type until after we have elaborated it?

949+We can achieve this without any change to the elaborator by defining

950+a type $\TC{Infer}$:

945951

946952\DM{

947953\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{}.

978984\MO{Elab}\:\vec{\VV{pclause}}\:\mq\:

979985\edo{

980986\tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\

981−\MO{TTDecl}\:\tc

987+\vec{\MO{TTDecl}}\:\tc

982988}

983989}

984990}

@@ -1189,6 +1195,7 @@ OrdEq (instanceOrd {{eq}} compare' max') = eq

11891195\end{SaveVerbatim}

11901196\useverb{ordparent}

11911197

1198+\noindent

11921199In general, we elaborate \texttt{class} declarations as follows:

11931200

11941201\DM{

@@ -1201,7 +1208,13 @@ In general, we elaborate \texttt{class} declarations as follows:

12011208\MO{Elab}\:

12021209\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Set\:\iwhere\\

12031210\hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)}

1204−\\

1211+}

1212+}

1213+}

1214+

1215+\DM{

1216+\AR{

1217+\AR{

12051218\vec{\MO{ElabMeth}}\:\vec{\VV{meth}}\:\td\\

12061219\vec{\MO{ElabParent}}\:\tc

12071220}

@@ -1220,6 +1233,7 @@ In general, we elaborate \texttt{class} declarations as follows:

12201233}

12211234}

12221235

1236+\noindent

12231237Then we elaborate \texttt{instance} declarations as follows:

12241238

12251239\DM{

@@ -1242,12 +1256,12 @@ Then we elaborate \texttt{instance} declarations as follows:

12421256Adding default definitions is straightforward: simply insert the default definition where

12431257there is a method missing in an \texttt{instance} declaration.

12441258

1245−[Key point: we've added a higher level language construct simply by elaborating in terms of

1246−a lower level language construct. In particular, we don't need to worry about type

1247−class \remph{resolution}, because we have a tactic to do that.

1248−We can build a lot of extensions this way because we

1249−have effectively built, bottom up, an Embedded Domain Specific Language for constructing

1250−programs in \TT{}.]

1259+\textbf{Remark:} Here, we have added a higher level language construct (type

1260+classes) simply by elaborating in terms of lower level language constructs

1261+(data types and functions). We achieve type class resolution by implementing a

1262+tactic, $\MO{Instance}$. We can build several extensions this way because we

1263+have effectively built, bottom up, an Embedded Domain Specific Language for

1264+constructing programs in \TT{}.

12511265

12521266\subsubsection{The $\MO{Instance}$ tactic}

12531267

@@ -1356,6 +1370,8 @@ and $\icase$ expressions:

13561370\ve ::= & \ldots \\

13571371\mid & \mvar{\vx} & (\mbox{metavariable}) &

13581372\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) \\

1373+\medskip\\

1374+\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\

13591375\end{array}

13601376}

13611377}

@@ -1412,7 +1428,7 @@ it to the current context:

14121428\edo{

14131429(\tv\Hab\ttt)\gets\MO{Context}\\

14141430\vT\gets\MO{Type}\\

1415−\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vt)\\

1431+\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vT)\\

14161432\ttinterp{\vx\:\tv}

14171433}

14181434}

@@ -1422,7 +1438,7 @@ it to the current context:

14221438A \texttt{case} expression allows pattern matching on intermediate values. The difficulty

14231439in elaborating \texttt{case} expressions is that \TT{} allows matching only on

14241440\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

14261442way to implement this is to use a metavariable. For example, we have already seen

14271443\texttt{lookup\_default}:

14281444

@@ -1466,6 +1482,9 @@ $\MO{Elab}$. Again, because of the way we have set up an Embedded Domain Specifi

14661482Language for describing elaboration, we have been able to implement a new higher

14671483level language feature in terms of elaboration of lower level language features.

14681484

1485+%\subsubsection{Tactic-implicit arguments}

1486+

1487+

14691488%\subsubsection{Pairs and Dependent Pairs}

14701489

14711490% Other extensions: do notation, idiom brackets, pairs, etc, are easily expressed

impl-paper/hll.tex+39−16

@@ -4,7 +4,7 @@

55\Idris{} is

66a 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

88library \cite{brady2011epic}.

99In this section, I will give a brief introduction to programming in \Idris{},

1010covering the most important features. A full tutorial is available elsewhere

@@ -75,7 +75,8 @@ infixr 10 ::

7575\end{SaveVerbatim}

7676\useverb{infixcons}

7777

78−\noindent

78+This declares that \texttt{::} is a right associative operator (\texttt{infixr})

79+with a precedence level of 10.

7980Functions, data constructors and type constuctors may all be given infix

8081operators as names. They may be used in prefix form if enclosed in brackets,

8182e.g. \tDC{(::)}.

@@ -105,10 +106,11 @@ mult (S k) y = plus y (mult k y)

105106The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded

106107for use by \texttt{Nat}, and are implemented

107108using 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−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

111−all part of the same namespace.

109+types and function names must begin with a capital letter or not.

110+%Function

111+%names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},

112+%\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are

113+%all part of the same namespace.

112114

113115\Idris{} has an interactive prompt, at which we can test these functions:

114116

@@ -160,7 +162,8 @@ further than the outer function.

160162\textbf{Scope:}

161163Any names which are visible in the outer scope are also visible in the \texttt{where}

162164clause (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,

164167in the above example, the \texttt{a} in the top level type and the \texttt{a} in the

165168auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required

166169behaviour, the \texttt{a} can be brought into scope as follows:

@@ -178,7 +181,8 @@ reverse {a} xs = revAcc [] xs where

178181\subsubsection{Dependent Types}

179182

180183A standard example of a dependent type is the type of ``lists with length'',

181−conventionally called ``vectors''. In \Idris{}, we declare vectors as follows:

184+conventionally called ``vectors'' in the dependently typed programming

185+literature. In \Idris{}, we declare vectors as follows:

182186

183187\begin{SaveVerbatim}{vect}

184188

@@ -196,7 +200,7 @@ are declared in different namespaces (in practice, normally in different modules

196200Ambiguous constructor names are resolved by type.

197201

198202This 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

200204declaration: we explicitly state the type

201205of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

202206argument, 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,

293297\texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit}

294298arguments to \texttt{index}. We could also write the type of \texttt{index} as:

295299

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+

296311\begin{SaveVerbatim}{vindeximpty}

297312

298313index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a

@@ -339,11 +354,14 @@ this constructors of \texttt{List} and \texttt{Vect}, names

339354can be overloaded in an ad-hoc manner and resolved according to the context in which

340355they are used. This is mostly for convenience, to eliminate the need to decorate

341356constructor 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}.

343360

344−Secondly, \Idris{} implements \remph{type classes}. This allows a more principled approach

345−to overloading --- a type class gives a collection of overloaded operations which describe

346−the interface for \remph{instances} of that class.

361+Secondly, \Idris{} implements \remph{type classes}, following Haskell. This

362+allows a more principled approach to overloading --- a type class gives a

363+collection of overloaded operations which describe the interface for

364+\remph{instances} of that class.

347365

348366A simple example

349367is the \texttt{Show} type class, which is defined in the library and

@@ -380,11 +398,16 @@ instance Show Nat where

380398 show O = "O"

381399 show (S k) = "s" ++ show k

382400

401+\end{SaveVerbatim}

402+\useverb{shownat}

403+

404+\begin{SaveVerbatim}{shownati}

405+

383406Idris> show (S (S (S O)))

384407"sssO" : String

385408

386409\end{SaveVerbatim}

387−\useverb{shownat}

410+\useverb{shownati}

388411

389412\noindent

390413Only 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

473496\useverb{letb}

474497

475498\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

477500fields from a record as follows, as well as by pattern matching at the top level:

478501

479502\begin{SaveVerbatim}{letp}

@@ -507,7 +530,7 @@ at the point where the given function returns true. We then deconstruct the

507530pair it returns, and remove the first character of the second string.

508531

509532A \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}

511534looks up an index in a list, returning \texttt{Nothing} if the index is out

512535of bounds. We can use this to write \texttt{lookup\_default}, which

513536looks 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}

6767

6868\begin{abstract}

6969Many 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

7171evaluation. 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

7373language implementations. In this paper, I describe the implementation of a

7474new dependently typed functional programming language, \Idris{}.

7575\Idris{} is intended to be a \emph{general purpose} programming language

@@ -127,14 +127,14 @@ implementation of new high level language constructs.

127127

128128\appendix

129129

130−\section{Elaboration meta-operations}

130+%\section{Elaboration meta-operations}

131131

132−It's possible that it would be useful to have a quick reference of meta-operations

133−used by the elaborator here.

132+%It's possible that it would be useful to have a quick reference of meta-operations

133+%used by the elaborator here.

134134

135−They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,

136−$\MO{NewProof}$, $\MO{NewTerm}$,

137−$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.

135+%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$,

136+%$\MO{NewProof}$, $\MO{NewTerm}$,

137+%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$.

138138

139139%\input{code}

140140

impl-paper/intro.tex+4−2

@@ -50,11 +50,13 @@ an EDSL based method for translating programs in a

5050high level dependently typed programming language to a small core type theory,

5151\TT{}, based on UTT \cite{luo1994}. The paper describes the structure of the

5252EDSL including proof and system state, and introduces a collection of \remph{tactics}

53−for manipulating incompete programs.

53+for manipulating incomplete programs.

5454Secondly, the paper gives a detailed description of the core type theory used

5555by \Idris{}, including a full description of the typing rules. Finally, through

5656describing the EDSL and the specific tactics, the paper shows how to extend

5757\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.

5860

5961The paper is structured as follows: In Section \ref{sect:hll} I give an overview of

6062programming in \Idris{}, introducing the high level constructs which will be

@@ -68,7 +70,7 @@ Section \ref{sect:discussion} we discuss related work and conclude.

6870

6971\subsection{Typographical conventions}

7072

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

7274language \Idris{} intended for programmers, and a low level language \TT{} to

7375which \Idris{} is elaborated. We distinguish these languages typographically as

7476follows:

impl-paper/library.bib+828−828

@@ -1,297 +1,276 @@

11Automatically generated by Mendeley 1.3.1

22Any changes to this file will be lost if it is regenerated by Mendeley.

4−@inproceedings{Sculthorpe2009,

5−author = {Sculthorpe, Neil and Nilsson, Henrik},

6−booktitle = {International Conference on Functional Programming ({ICFP} '09)},

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},

8−title = {{Safe functional reactive programming through dependent types}},

9−url = {http://dl.acm.org/citation.cfm?id=1596558},

10−year = {2009}

4+@inproceedings{ko2011modularising,

5+author = {Ko, H.S. and Gibbons, J.},

6+booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},

7+file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

8+pages = {13--24},

9+publisher = {ACM},

10+title = {{Modularising inductive families}},

11+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},

12+year = {2011}

1113}

12−@inproceedings{Augustsson1985,

13−address = {Berlin, Heidelberg},

14−author = {Augustsson, Lennart},

15−booktitle = {Functional Programming Languages and Computer Architecture},

16−doi = {10.1007/3-540-15975-4},

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}

14+@inproceedings{gibbons2011modularising,

15+author = {Gibbons, J. and Ko, H.S. and Others},

16+file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

17+title = {{Modularising inductive families}},

18+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},

19+year = {2011}

2720}

28−@inproceedings{NanevskiAAMorrisett2008,

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.},

30−author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},

31−booktitle = {International Conference on Functional Programming},

32−doi = {10.1145/1411204.1411237},

33−file = {:home/edwin/Research/Papers/Mendeley/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},

34−isbn = {9781595939197},

35−issn = {15232867},

21+@article{Okasaki1993,

22+author = {Okasaki, Chris},

23+file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

24+journal = {Journal of functional programming},

25+title = {{Red-Black Trees in A Functional Setting}},

26+year = {1993}

27+}

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},

3641keywords = {Dependent Types},

3742mendeley-tags = {Dependent Types},

38−number = {9},

39−pages = {229--240},

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}

43+title = {{Inductive families need not store their indices}},

44+url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},

45+year = {2003}

4446}

45−@inproceedings{McBride2004b,

46−author = {McBride, Conor and McKinna, James},

47−booktitle = {Haskell Workshop},

48−file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},

49−title = {{I am not a number : I am a free variable}},

50−year = {2004}

47+@misc{TheMendeleySupportTeam2011,

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.},

49+address = {London},

50+author = {{The Mendeley Support Team}},

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},

58+year = {2011}

5159}

52−@article{marlow2006making,

53−author = {Marlow, S. and {Peyton Jones}, S.},

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},

55−journal = {Journal of Functional Programming},

56−number = {4-5},

57−pages = {415--449},

58−publisher = {Cambridge University Press},

59−title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}},

60−url = {http://dl.acm.org/citation.cfm?id=1166018},

61−volume = {16},

60+@inproceedings{Wadler1989,

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.},

62+author = {Wadler, Philip},

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},

67+number = {June},

68+pages = {347--359},

69+publisher = {ACM},

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}},

94+url = {http://dl.acm.org/citation.cfm?id=640136.604179},

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},

62125year = {2006}

63126}

64−@book{Choosing2012,

65−author = {Fowler, Martin},

127+@book{Approach2012,

128+author = {Hunt, Andrew and Thomas, David},

66129booktitle = {Carcinogenesis},

67130doi = {10.1093/carcin/bgs054},

68−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},

69−isbn = {9780132107549},

131+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},

132+isbn = {020161622X},

70133issn = {1460-2180},

71134number = {3},

72135pmid = {22383472},

73−title = {{Domain Specific Languages Chapter 6}},

136+title = {{The Pragmatic Programmer Chapter 2}},

74137url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},

75138volume = {33}

76139}

77−@misc{Protocols2012a,

78−author = {Anderson, Ross},

140+@article{Miller1992,

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.},

79150doi = {10.1093/epirev/mxr031},

80−file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},

81−isbn = {9780470068526},

151+file = {:home/edwin/Research/Papers/Mendeley/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

152+isbn = {9781449394592},

82153issn = {1478-6729},

83154pmid = {22215642},

84−title = {{Security Engineering Chapter 3}}

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}

155+title = {{Using SQLite Chapter 7}}

95156}

96−@article{Steiner1988,

97−author = {Steiner, JG},

98−file = {:home/edwin/Research/Papers/Mendeley/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

99−journal = {Proc. Winter USENIX Conference},

100−title = {{Kerberos: An authentication service for open network systems}},

101−url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},

102−year = {1988}

157+@inproceedings{chlipala2010ur,

158+author = {Chlipala, Adam},

159+booktitle = {ACM SIGPLAN Notices},

160+file = {:home/edwin/Research/Papers/Mendeley/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

161+number = {6},

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},

167+year = {2010}

103168}

104−@book{Fowler,

105−author = {Fowler, Martin},

106−booktitle = {Language},

107−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},

108−isbn = {9780132107549},

109−title = {{Domain Specific Languages Chapter 2}}

169+@book{peyton1987implementation,

170+author = {{Peyton Jones}, S.L.},

171+publisher = {Prentice-Hall, Inc.},

172+title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}},

173+url = {http://dl.acm.org/citation.cfm?id=1096899},

174+year = {1987}

110175}

111−@article{Brady2006a,

112−author = {Brady, E and Hammond, K},

113−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

114−journal = {\ldots of the 5th international conference on \ldots},

115−keywords = {Dependent Types},

116−mendeley-tags = {Dependent Types},

117−title = {{A verified staged interpreter is a verified compiler}},

118−url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},

119−year = {2006}

176+@article{dybjer1994inductive,

177+author = {Dybjer, P.},

178+journal = {Formal aspects of computing},

179+number = {4},

180+pages = {440--465},

181+publisher = {Springer},

182+title = {{Inductive families}},

183+url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},

184+volume = {6},

185+year = {1994}

120186}

121−@inproceedings{oury2008power,

122−author = {Oury, N. and Swierstra, W.},

123−booktitle = {International Conference on Functional Programming},

124−file = {:home/edwin/Research/Papers/Mendeley/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

125−keywords = {Dependent Types},

126−mendeley-tags = {Dependent Types},

127−number = {9},

128−pages = {39--50},

187+@inproceedings{lempsink2009type,

188+author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},

189+booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},

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},

191+pages = {61--72},

129192publisher = {ACM},

130−title = {{The power of Pi}},

131−url = {http://dl.acm.org/citation.cfm?id=1411213},

132−volume = {43},

133−year = {2008}

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}

193+title = {{Type-safe diff for families of datatypes}},

194+url = {http://dl.acm.org/citation.cfm?id=1596624},

195+year = {2009}

211196}

212−@article{Abel2010,

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.},

214−author = {Abel, Andreas},

215−file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},

216−journal = {EPTCS},

217−pages = {1--15},

218−title = {{MiniAgda: Integrating Sized and Dependent Types}},

219−url = {http://arxiv.org/abs/1012.4896},

220−volume = {43},

221−year = {2010}

197+@misc{The2012b,

198+author = {Brooks, Fred},

199+doi = {10.1093/epirev/mxr031},

200+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},

201+isbn = {9780321702081},

202+issn = {1478-6729},

203+pmid = {22215642},

204+title = {{The Design of Design Chapter 1}}

222205}

223−@inproceedings{fisher2005pads,

224−author = {Fisher, K. and Gruber, R.},

225−booktitle = {ACM SIGPLAN Notices},

226−number = {6},

227−pages = {295--304},

228−publisher = {ACM},

229−title = {{PADS: a domain-specific language for processing ad hoc data}},

230−url = {http://dl.acm.org/citation.cfm?id=1065046},

231−volume = {40},

232−year = {2005}

206+@misc{The2012c,

207+author = {Robbins, A and Hannah, E and Lamb, L},

208+doi = {10.1093/epirev/mxr031},

209+file = {:home/edwin/Research/Papers/Mendeley/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

210+isbn = {9780596529833},

211+issn = {1478-6729},

212+pmid = {22215642},

213+title = {{Learning the vi and Vim Editors}}

233214}

234−@article{mccann2000packet,

235−author = {McCann, P.J. and Chandra, S.},

236−journal = {ACM SIGCOMM Computer Communication Review},

237−number = {4},

238−pages = {321--333},

239−publisher = {ACM},

240−title = {{Packet types: abstract specification of network protocol messages}},

241−url = {http://dl.acm.org/citation.cfm?id=347563},

242−volume = {30},

243−year = {2000}

215+@book{Brady2012,

216+author = {Hunt, Andrew and Thomas, David},

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},

222+number = {3},

223+pmid = {22383472},

224+title = {{The Pragmatic Programmer Chapter 5}},

225+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},

226+volume = {33}

244227}

245−@inproceedings{Brady2003,

246−author = {Brady, Edwin and McBride, Conor and McKinna, James},

247−booktitle = {Types for Proofs and Programs},

248−file = {:home/edwin/Research/Papers/Mendeley/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},

249−keywords = {Dependent Types},

250−mendeley-tags = {Dependent Types},

251−title = {{Inductive families need not store their indices}},

252−url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},

253−year = {2003}

228+@inproceedings{Pasalic2002,

229+author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},

230+booktitle = {International Conference on Functional Programming},

231+doi = {10.1145/583852.581499},

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},

233+isbn = {1-58113-487-8},

234+issn = {03621340},

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},

242+year = {2002}

254243}

255−@misc{TheMendeleySupportTeam2011,

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.},

257−address = {London},

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},

261−keywords = {Mendeley,how-to,user manual},

262−pages = {1--16},

263−publisher = {Mendeley Ltd.},

264−title = {{Getting Started with Mendeley}},

265−url = {http://www.mendeley.com},

266−year = {2011}

244+@misc{Nodes2012a,

245+author = {Brooks, Fred},

246+doi = {10.1093/epirev/mxr031},

247+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},

248+isbn = {9780321702081},

249+issn = {1478-6729},

250+pmid = {22215642},

251+title = {{The Design of Design Chapter 3}}

267252}

268−@inproceedings{Sheard2005,

269−address = {New York, New York, USA},

270−author = {Sheard, Tim},

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},

274−isbn = {159593071X},

275−keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},

276−month = sep,

277−pages = {74--85},

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}

253+@article{Haskell2012a,

254+author = {Biancuzzi, F and Warden, S},

255+doi = {10.1093/epirev/mxr031},

256+file = {:home/edwin/Research/Papers/Mendeley/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

257+isbn = {9780596801670},

258+issn = {1478-6729},

259+pmid = {22215642},

260+title = {{Masterminds of Programming Chapter 8}}

282261}

283−@article{Jones2003,

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.},

285−author = {Jones, Simon Peyton},

286−editor = {Jones, Simon Peyton},

287−isbn = {0521826144},

288−journal = {Language},

289−number = {1},

290−publisher = {Cambridge University Press},

291−title = {{Haskell 98 Language and Libraries The Revised Report}},

292−url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},

293−volume = {13},

294−year = {2003}

262+@book{An2012,

263+author = {Fowler, Martin},

264+booktitle = {Carcinogenesis},

265+doi = {10.1093/carcin/bgs054},

266+file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},

267+isbn = {9780132107549},

268+issn = {1460-2180},

269+number = {3},

270+pmid = {22383472},

271+title = {{Domain Specific Languages Chapter 1}},

272+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},

273+volume = {33}

295274}

296275@article{McBride2005,

297276author = {McBride, Conor},

@@ -308,18 +287,6 @@ url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},

308287volume = {3622},

309288year = {2005}

310289}

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−}

323290@misc{Resolution2012a,

324291author = {Fall, Kevin R and Stevens, W. Richard},

325292doi = {10.1093/epirev/mxr031},

@@ -328,225 +295,31 @@ issn = {1478-6729},

328295pmid = {22215642},

329296title = {{TCP/IP Illustrated Volume 1 Chapter 11}}

330297}

331−@inproceedings{gibbons2011modularising,

332−author = {Gibbons, J. and Ko, H.S. and Others},

333−file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.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},

298+@phdthesis{Brady2005,

299+author = {Brady, Edwin},

300+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},

419301keywords = {Dependent Types},

420302mendeley-tags = {Dependent Types},

421−organization = {Carnegie Mellon University},

422−pages = {214--227},

423−publisher = {ACM Press},

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}

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}}

303+school = {University of Durham},

304+title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},

305+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf},

306+year = {2005}

459307}

460−@inproceedings{Brady2006b,

308+@inproceedings{Brady2011a,

309+address = {New York, New York, USA},

461310author = {Brady, Edwin},

462−booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},

463−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

464−isbn = {978-3-540-74129-9},

465−month = sep,

466−pages = {145----162},

467−title = {{Ivor, a proof engine}},

468−url = {http://dl.acm.org/citation.cfm?id=1757028.1757037},

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},

311+booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},

312+doi = {10.1145/1929529.1929536},

313+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},

314+isbn = {9781450304870},

315+keywords = {Dependent Types,data description,dependent types},

316+mendeley-tags = {Dependent Types},

317+month = jan,

318+publisher = {ACM Press},

319+title = {{Idris --- Systems Programming Meets Full Dependent Types}},

320+url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},

482321year = {2011}

483322}

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−}

550323@misc{dagand2011transporting,

551324author = {Dagand, Pierre-Evariste and McBride, Conor},

552325file = {: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}},

554327url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},

555328year = {2011}

556329}

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−}

564330@inproceedings{taha2004gentle,

565331author = {Taha, W.},

566332booktitle = {Domain-Specific Program Generation},

@@ -570,42 +336,25 @@ title = {{A gentle introduction to multi-stage programming}},

570336url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},

571337year = {2004}

572338}

573−@inproceedings{pj2006gadts,

574−author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},

575−booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},

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},

339+@inproceedings{augustsson2008paradise,

340+author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},

341+booktitle = {International Conference on Functional Programming},

342+file = {:home/edwin/Research/Papers/Mendeley/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},

577343number = {9},

578−pages = {50--61},

344+pages = {225--228},

579345publisher = {ACM},

580−title = {{Simple unification-based type inference for GADTs}},

581−url = {http://dl.acm.org/citation.cfm?id=1159811},

582−volume = {41},

583−year = {2006}

346+title = {{Paradise: a two-stage DSL embedded in Haskell}},

347+url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},

348+volume = {43},

349+year = {2008}

584350}

585−@misc{altenkirch2008nσ,

586−author = {Altenkirch, T. and Oury, N.},

587−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},

588−title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},

589−url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},

590−year = {2008}

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}}

351+@misc{altenkirch2005dependent,

352+author = {Altenkirch, T. and McBride, C. and McKinna, J.},

353+booktitle = {Manuscript, available online},

354+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

355+title = {{Why dependent types matter}},

356+url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},

357+year = {2005}

609358}

610359@article{Xi1998,

611360abstract = {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},

626375volume = {33},

627376year = {1998}

628377}

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−}

705378@inproceedings{augustsson1999exercise,

706379author = {Augustsson, L. and Carlsson, M.},

707380booktitle = {In Workshop on Dependent Types in Programming, Gothenburg},

@@ -723,18 +396,6 @@ url = {http://journals.cambridge.org/abstract_S0956796811000207},

723396volume = {21},

724397year = {2011}

725398}

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−}

738399@inproceedings{norell2009dependently,

739400author = {Norell, Ulf},

740401booktitle = {Advanced Functional Programming},

@@ -781,14 +442,50 @@ title = {{Typing Haskell in Haskell}},

781442url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},

782443year = {1999}

783444}

784−@article{Epstein2011,

785−author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},

786−institution = {Microsoft Research},

787−journal = {researchmicrosoftcom},

788−number = {Section 8},

789−pages = {1--12},

790−title = {{Haskell for the cloud}},

791−url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf},

445+@article{Altenkirch2010,

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.},

447+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas},

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},

453+number = {Sheard 2005},

454+pages = {40--55},

455+publisher = {Springer Berlin Heidelberg},

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},

792489year = {2011}

793490}

794491@article{danielsson2011parsing,

@@ -828,28 +525,17 @@ title = {{Programming in Idris : a tutorial}},

828525url = {http://idris-lang.org/tutorial},

829526year = {2012}

830527}

831−@book{An2012,

832−author = {Fowler, Martin},

833−booktitle = {Carcinogenesis},

834−doi = {10.1093/carcin/bgs054},

835−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},

836−isbn = {9780132107549},

837−issn = {1460-2180},

528+@inproceedings{madhavapeddy2007melange,

529+author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},

530+booktitle = {ACM SIGOPS Operating Systems Review},

531+file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},

838532number = {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},

849534publisher = {ACM},

850−title = {{Modularising inductive families}},

851−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},

852−year = {2011}

535+title = {{Melange: creating a functional internet}},

536+url = {http://dl.acm.org/citation.cfm?id=1273009},

537+volume = {41},

538+year = {2007}

853539}

854540@inproceedings{Augustsson1998,

855541abstract = {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}},

877563url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},

878564year = {2011}

879565}

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+}

880583@inproceedings{swierstra2007beauty,

881584author = {Swierstra, W. and Altenkirch, T.},

882585booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},

@@ -887,42 +590,43 @@ title = {{Beauty in the beast}},

887590url = {http://dl.acm.org/citation.cfm?id=1291206},

888591year = {2007}

889592}

890−@inproceedings{Brady2010,

593+@inproceedings{bradyresource,

891594author = {Brady, Edwin and Hammond, Kevin},

892−booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},

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},

894−isbn = {9781605587943},

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},

896−mendeley-tags = {Dependent Types},

897−pages = {297--308},

595+booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},

596+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},

597+pages = {242----257},

598+title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},

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},

607+pages = {1--51},

898608publisher = {ACM},

899−title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},

900−url = {http://portal.acm.org/citation.cfm?id=1863587},

609+title = {{The next 700 data description languages}},

610+url = {http://dl.acm.org/citation.cfm?id=1111039},

611+volume = {15},

901612year = {2010}

902613}

903−@misc{The2012c,

904−author = {Robbins, A and Hannah, E and Lamb, L},

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},

907−isbn = {9780596529833},

908−issn = {1478-6729},

909−pmid = {22215642},

910−title = {{Learning the vi and Vim Editors}}

614+@book{Bird2010,

615+author = {Bird, Richard},

616+file = {:home/edwin/Research/Papers/Mendeley/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},

617+isbn = {9780521513388},

618+title = {{Pearls of Functional Algorithm Design}},

619+year = {2010}

911620}

912−@misc{altenkirch2005dependent,

913−author = {Altenkirch, T. and McBride, C. and McKinna, J.},

914−booktitle = {Manuscript, available online},

915−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

916−title = {{Why dependent types matter}},

917−url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},

918−year = {2005}

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}}

621+@inproceedings{stump2010resource,

622+author = {Stump, A. and Austin, E.},

623+booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},

624+file = {:home/edwin/Research/Papers/Mendeley/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

625+pages = {27--38},

626+publisher = {ACM},

627+title = {{Resource typing in Guru}},

628+url = {http://dl.acm.org/citation.cfm?id=1707796},

629+year = {2010}

926630}

927631@inproceedings{taha1997multi,

928632author = {Taha, W. and Sheard, T.},

@@ -935,66 +639,6 @@ url = {http://dl.acm.org/citation.cfm?id=259019},

935639volume = {32},

936640year = {1997}

937641}

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−}

998642@article{Wadler2001,

999643abstract = {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.},

1000644author = {Wadler, Philip},

@@ -1013,18 +657,6 @@ url = {http://www.springerlink.com/index/715264614rh13340.pdf},

1013657volume = {925},

1014658year = {2001}

1015659}

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−}

1028660@article{Hoare1978,

1029661abstract = {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.},

1030662author = {Hoare, C A R},

@@ -1044,16 +676,44 @@ url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},

1044676volume = {21},

1045677year = {1978}

1046678}

1047−@phdthesis{norell2007thesis,

1048−author = {Norell, Ulf},

1049−file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},

1050−keywords = {Dependent Types},

679+@book{Philosophy2012,

680+author = {Hunt, Andrew and Thomas, David},

681+booktitle = {Carcinogenesis},

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},

1051711mendeley-tags = {Dependent Types},

1052−publisher = {Citeseer},

1053−school = {Chalmers University of Technology},

1054−title = {{Towards a practical programming language based on dependent type theory}},

1055−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},

1056−year = {2007}

712+pages = {297--308},

713+publisher = {ACM},

714+title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},

715+url = {http://portal.acm.org/citation.cfm?id=1863587},

716+year = {2010}

1057717}

1058718@inproceedings{Visser2008,

1059719author = {Visser, E},

@@ -1062,6 +722,19 @@ title = {{WebDSL: A case study in domain-specific language engineering}},

1062722url = {http://www.springerlink.com/index/A3213003X6268032.pdf},

1063723year = {2008}

1064724}

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+}

1065738@inproceedings{Brady2005a,

1066739author = {Brady, E and Hammond, K},

1067740booktitle = {Implementation and Application of Functional \ldots},

@@ -1072,40 +745,6 @@ title = {{A dependently typed framework for static analysis of program execution

1072745url = {http://www.springerlink.com/index/P446P2HH70107759.pdf},

1073746year = {2005}

1074747}

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−}

1109748@inproceedings{madhavapeddy2010turning,

1110749author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},

1111750booktitle = {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}},

1115754url = {http://dl.acm.org/citation.cfm?id=1863114},

1116755year = {2010}

1117756}

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+}

1118765@inproceedings{bhargavan2010modular,

1119766author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},

1120767booktitle = {ACM Sigplan Notices},

@@ -1135,12 +782,21 @@ title = {{An analysis of Girard's paradox}},

1135782url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},

1136783year = {1986}

1137784}

1138−@misc{Abel1998,

1139−author = {Abel, Andreas},

1140−booktitle = {Language},

1141−file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

1142−title = {{foetus - Termination Checker for Simple Functional Programs}},

1143−year = {1998}

785+@inproceedings{Augustsson1985,

786+address = {Berlin, Heidelberg},

787+author = {Augustsson, Lennart},

788+booktitle = {Functional Programming Languages and Computer Architecture},

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},

799+year = {1985}

1144800}

1145801@misc{Bloat,

1146802author = {Brooks, Fred},

@@ -1148,6 +804,16 @@ file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Desig

1148804isbn = {9780321702081},

1149805title = {{The Design of Design Chapter 4}}

1150806}

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+}

1151817@misc{Brady2012c,

1152818author = {Brooks, Fred},

1153819doi = {10.1093/epirev/mxr031},

@@ -1160,31 +826,31 @@ pmid = {22215642},

1160826title = {{The Design of Design Chapter 5}},

1161827volume = {34}

1162828}

1163−@inproceedings{atkey2009unembedding,

1164−author = {Atkey, R. and Lindley, S. and Yallop, J.},

1165−booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},

1166−pages = {37--48},

1167−publisher = {ACM},

1168−title = {{Unembedding domain-specific languages}},

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},

829+@inproceedings{Fournet2011,

830+author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},

831+booktitle = {Foundations of security analysis and design {VI}},

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},

833+title = {{Cryptographic verification by typing for a sample protocol implementation}},

834+url = {http://www.springerlink.com/index/V168041M46658R73.pdf},

1182835year = {2010}

1183836}

1184−@article{mcbride2008functional,

1185−author = {McBride, C. and Paterson, R.},

1186−file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},

1187−journal = {Journal of functional programming},

837+@book{Choosing2012,

838+author = {Fowler, Martin},

839+booktitle = {Carcinogenesis},

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},

1188854number = {1},

1189855pages = {1--13},

1190856publisher = {Cambridge Univ Press},

@@ -1202,18 +868,61 @@ title = {{Implicit syntax}},

1202868url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},

1203869year = {1990}

1204870}

1205−@book{While2012,

1206−author = {Hunt, Andrew and Thomas, David},

1207−booktitle = {Carcinogenesis},

1208−doi = {10.1093/carcin/bgs054},

1209−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},

1210−isbn = {020161622X},

1211−issn = {1460-2180},

1212−number = {3},

1213−pmid = {22383472},

1214−title = {{The Pragmatic Programmer Chapter 6}},

1215−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},

1216−volume = {33}

871+@misc{altenkirch2008nσ,

872+author = {Altenkirch, T. and Oury, N.},

873+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},

874+title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},

875+url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},

876+year = {2008}

877+}

878+@misc{Abel1998,

879+author = {Abel, Andreas},

880+booktitle = {Language},

881+file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

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}

1217926}

1218927@article{gordon2003authenticity,

1219928author = {Gordon, A.D. and Jeffrey, A.},

@@ -1239,3 +948,294 @@ pmid = {22215642},

1239948title = {{Security Engineering Chapter 18}},

1240949volume = {34}

1241950}

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:

2323\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.

2424\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.

2525\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.

2727\end{itemize}

2828

2929We 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} ($\

106106is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$

107107then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of

108108contractions and reversed contractions. Terms which are convertible are also said to

109−be computationally equal.

109+be definitionally equal.

110110The evaluator can also be extended by defining pattern matching functions, which

111111will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern

112112matching functions can be understood as extending the core language with high level

@@ -151,6 +151,30 @@ be implemented in the usual way~\cite{loh2010tutorial}.

151151\Rule{\Gamma\proves\RW{valid}}

152152{\Gamma\vdash\Type_n\Hab\Type_{n+1}}

153153\\

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+\\

154178\mathsf{Var}_1\:

155179\Rule{(\lam{\vx}{\vS})\in\Gamma}

156180{\Gamma\vdash\vx\Hab\vS}

@@ -163,14 +187,6 @@ be implemented in the usual way~\cite{loh2010tutorial}.

163187\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}

164188{\Gamma\vdash\vx\Hab\vS}

165189\\

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−\\

174190\mathsf{App}\:

175191\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}

176192{\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

230246\remph{values} as well as types. An inductive family is declared

231247in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}

232248as

233−follows, using the de Bruijn telescope notation, $\tx$, to indicate a

249+follows, using vector notation, $\tx$, to indicate a

234250sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):

235251

236252\DM{

@@ -351,7 +367,7 @@ In order to implement pattern matching, we must separate the \remph{accessible}

351367to match against it) if it is constructor headed, or a variable. Inaccessible patterns

352368are converted to ``match anything'' patterns. We convert clauses to matchable pattern

353369clauses 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

355371$\MO{Pat}$ operation across a list of arguments.

356372

357373\FFIG{

@@ -444,6 +460,25 @@ to a telescope $\tx$ as $\vec{\MO{Op}}\:\tx$.

444460In practice, for efficiency, pattern matching is implemented by compiling the match clauses to

445461a tree of case expressions~\cite{Augustsson1985}.

446462

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+

447482\subsection{From \Idris{} to \TT{}}

448483

449484\TT{} is a very small language, consisting only of data declarations and pattern matching