75e7758 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some progress on implementation paper revisions

75e7758Edwin Brady14 years ago

papers/impl-paper/conclusions.tex+26−32

compare with master

unifiedsplit

@@ -7,6 +7,8 @@ years as tools for verifying software correctness, and several experimental

7languages are being developed, in particular Agda \cite{norell2007thesis}, Epigram

8\cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.

10+[Talk about~\cite{Asperti}, ~\cite{OutsideIn}, ~\cite{Sozeau2008}]

11+

10An earlier implementation of \Idris{} was built on the \Ivor{} proof engine

12An earlier implementation of \Idris{} was built on the \Ivor{} proof engine

11\cite{Brady2006b}. This implementation differed in one important way --- unlike

13\cite{Brady2006b}. This implementation differed in one important way --- unlike

12the present implementation, there was limited separation between the type theory

14the present implementation, there was limited separation between the type theory

@@ -61,16 +63,17 @@ in under 1000 lines of Haskell code. It is important that this kernel remains sm

61the correctness of the underlying type system, and keeping the implementation small

63the correctness of the underlying type system, and keeping the implementation small

62reduces the possibility of errors.

64reduces the possibility of errors.

64−The approach we have taken to implementing the high level language, implementing

66+The approach we have taken to implementing the high level language,

65−a tactic language as an embedded DSL, allows us to

67+implementing an elaboration monad with tactics for program construction, allows

66−build programs on top of a small and unchanging kernel, rather than extending

68+us to build programs on top of a small and unchanging kernel, rather than

67−the core language to deal with implicit syntax, unification and type classes.

69+extending the core language to deal with implicit syntax, unification and type

68−High level \Idris{} features are implemented by describing the corresponding

70+classes. High level \Idris{} features are implemented by describing the

69−sequence of tactics to build an equivalent program in \TT{}, via a development

71+corresponding sequence of tactics to build an equivalent program in \TT{}, via

70−calculus of incomplete terms, \TTdev{}. A significant advantage we have found with

72+a development calculus of incomplete terms, \TTdev{}. A significant advantage

71−this approach is that higher level features can easily be implemented in terms

73+we have found with this approach is that higher level features can easily be

72−of existing elaborator components. For example, once we have implemented elaboration

74+implemented in terms of existing elaborator components. For example, once we

73−for data types and functions, it is easy to add several features:

75+have implemented elaboration for data types and functions, it is easy to add

76+several features:

75\begin{itemize}

78\begin{itemize}

76\item \textbf{Type classes}: A dictionary is merely a record containing the

79\item \textbf{Type classes}: A dictionary is merely a record containing the

@@ -89,13 +92,13 @@ implement these high level features.

89Other high level features such as dependent records, tuples and monad comprehensions

92Other high level features such as dependent records, tuples and monad comprehensions

90can be added equally easily --- and indeed have been added in the full implementation.

93can be added equally easily --- and indeed have been added in the full implementation.

91Furthermore,

94Furthermore,

92−since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it is

95+since we have taken a tactic-based approach to elaborating \Idris{} to \TT{},

93−possible to expose the tactic language to the programmer. This opens up the

96+it is possible to expose tactics to the programmer. This opens up

94−possibility of implementing domain specific decision procedures, or implementing

97+the possibility of implementing domain specific decision procedures, or

95−user defined tactics in a style similar to Coq's \texttt{Ltac} language \cite{Delahaye2000}.

98+implementing user defined tactics in a style similar to Coq's \texttt{Ltac}

96−Although \TT{} is primarily intended as a core language for \Idris{},

99+language \cite{Delahaye2000}. Although \TT{} is primarily intended as a core

97−its rich type system also allows it to capture a number of high level languages, especially

100+language for \Idris{}, its rich type system also allows it to capture a number

98−when augmented with primitive operators.

101+of high level languages, especially when augmented with primitive operators.

102

100We have not discussed the performance of the elaboration

103We have not discussed the performance of the elaboration

101algorithm, or described how \Idris{} compiles to executable code. In practice,

104algorithm, or described how \Idris{} compiles to executable code. In practice,

@@ -118,19 +121,10 @@ theory.

118However, a programming language implementation is not an end in itself.

121However, a programming language implementation is not an end in itself.

119Programming languages exist to support research and practice in many different

122Programming languages exist to support research and practice in many different

120domains. In future work, therefore, I plan to apply domain specific

123domains. In future work, therefore, I plan to apply domain specific

121−language based techniques to realistic problems

124+language based techniques to realistic problems in important safety critical

122−in important safety critical domains such as security and network protocol

125+domains such as security and network protocol design and implementation. In

123−design and implementation. In order to be successful, this will require a language which

126+order to be successful, this will require a language which is expressive enough

124−is expressive enough to describe protocol specifications at a high level, and robust

127+to describe protocol specifications at a high level, and robust enough to

125−enough to guarantee correct implementation of those protocols. \Idris{}, I believe,

128+guarantee correct implementation of those protocols. \Idris{}, I believe, is

126−is the right tool for this work.

129+the right tool for this work.

127−

128−

129−

130−%\subsection{Further Work}

131

130

132−%[Would the EDSL approach work in other languages? Adding components of DTP

133−%to imperative languages, say, using \TT{} as a verified core.

134−%\Idris{} implementation as the beginning of a project to explore practical

135−%DTP --- systems, protocols, security especially. And just having full

136−%dependent types for lightweight correctness guarantees.]

papers/impl-paper/elaboration.tex+109−61

@@ -41,33 +41,42 @@ similar to a $\LET$ binding, but without any computational force,

41i.e. there are no reduction rules for guess bindings.

42Using binders to represent holes is useful in a dependently typed setting since

43one value may determine another. Attaching a guess to a binder ensures that

44−instantiating one such value also instantiates all of its dependencies. The

44+instantiating one such variable also instantiates all of its dependencies.

45+%The

45−typing rules for binders ensure that no $?$ bindings leak into types.

46+%typing rules for binders ensure that no $?$ bindings leak into types.

47\FFIG{

48\FFIG{

48−\AR{

49+\begin{array}{c}

49\vb ::= \ldots

50\vb ::= \ldots

50 \:\mid\: \hole{\vx}{\vt} \:\:(\mbox{hole binding}) \:\:

51 \:\mid\: \hole{\vx}{\vt} \:\:(\mbox{hole binding}) \:\:

51 \:\mid\: \guess{\vx}{\vt}{\vt} \:\:(\mbox{guess})

52 \:\mid\: \guess{\vx}{\vt}{\vt} \:\:(\mbox{guess})

52\medskip\\

53\medskip\\

54+\mathsf{HoleVar}\:

55+\Rule{(\hole{\vx}{\vS})\in\Gamma}

56+{\Gamma\vdash\vx\Hab\vS}

57+\hg

58+\mathsf{GuessVar}\:

59+\Rule{(\guess{\vx}{\vS}{\vs})\in\Gamma}

60+{\Gamma\vdash\vx\Hab\vS}

61+\\

62+\mathsf{Hole}\:

53\Rule{

63\Rule{

54\Gamma;\hole{\vx}{\vS}\proves\ve\Hab\vT

64\Gamma;\hole{\vx}{\vS}\proves\ve\Hab\vT

55}

65}

56{

66{

57\Gamma\proves\hole{\vx}{\vS}\SC\ve\Hab\vT

67\Gamma\proves\hole{\vx}{\vS}\SC\ve\Hab\vT

58}

68}

59−\hspace*{0.1cm}\vx\not\in\vT

69+%\hspace*{0.1cm}\vx\not\in\vT

60−\hspace*{0.1in}\mathsf{Hole}

61\hg

70\hg

71+\mathsf{Guess}\:

62\Rule{

72\Rule{

63\Gamma;\guess{\vx}{\vS}{\ve_1}\proves\ve_2\Hab\vT

73\Gamma;\guess{\vx}{\vS}{\ve_1}\proves\ve_2\Hab\vT

64}

74}

65{

75{

66\Gamma\proves\guess{\vx}{\vS}{\ve_1}\SC\ve_2\Hab\vT

76\Gamma\proves\guess{\vx}{\vS}{\ve_1}\SC\ve_2\Hab\vT

67}

77}

68−\hspace*{0.1cm}\vx\not\in\vT

78+%\hspace*{0.1cm}\vx\not\in\vT

69−\hspace*{0.1in}\mathsf{Guess}

79+\end{array}

70−}

71}

80}

72{\TTdev{} extensions}

81{\TTdev{} extensions}

73{ttdev}

82{ttdev}

@@ -77,12 +86,13 @@ typing rules for binders ensure that no $?$ bindings leak into types.

78\label{sect:prfstate}

87\label{sect:prfstate}

80−A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:

89+A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:

82\begin{itemize}

91\begin{itemize}

83\item A global context, $\vC$, containing pattern matching definitions and their types

92\item A global context, $\vC$, containing pattern matching definitions and their types

84\item A local context, $\Delta$, containing pattern bindings

93\item A local context, $\Delta$, containing pattern bindings

85\item A proof term, $\ve$, in \TTdev{}

94\item A proof term, $\ve$, in \TTdev{}

95+\item Unsolved unification problems, $\vP$

86\item A hole queue, $\vQ$

96\item A hole queue, $\vQ$

87%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables

97%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables

88\end{itemize}

98\end{itemize}

@@ -91,29 +101,36 @@ The \remph{hole queue} is a priority queue of names of hole and guess binders

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

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

92in the proof term ---

102in the proof term ---

93ensuring that each bound name is unique. Holes refer to \remph{sub goals}

103ensuring that each bound name is unique. Holes refer to \remph{sub goals}

94−in the proof.

104+in the proof. As a proof develops, unification problems arising from unsolved

105+holes may be introduced, and may be solved when those holes are instantiated.

106+When the hole queue is empty, and there are no remaining unification

95−When this queue is empty, the proof term is complete.

107+problems, the proof term is complete.

108+

96Creating a \TT{} expression from an \Idris{} expression involves creating

109Creating a \TT{} expression from an \Idris{} expression involves creating

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

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

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

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

112

100In the implementation, the proof state is captured in an elaboration monad,

113In the implementation, the proof state is captured in an elaboration monad,

114+\texttt{Elab}, which is simply a state monad with exceptions. This monad

101−\texttt{Elab}, which includes various operations for querying and updating

115+supports various operations for querying and updating the proof state,

102−the proof state, manipulating terms, generating fresh names, etc. However, we will

116+manipulating terms, generating fresh names, etc. However, we will describe

103−describe \Idris{} elaboration in terms of meta-operations on the proof state,

117+\Idris{} elaboration in terms of meta-operations on the proof state, in order

104−in order to capture the essence of the elaboration process without being distracted

118+to capture the essence of the elaboration process without being distracted by

105−by implementation details. These meta-operations include:

119+implementation details. These meta-operations include:

106

120

107\begin{itemize}

121\begin{itemize}

108\item \demph{Queries} which retrieve values from the proof state, without modifying

122\item \demph{Queries} which retrieve values from the proof state, without modifying

109the state. For example, we can:

123the state. For example, we can:

110\begin{itemize}

124\begin{itemize}

111−\item Get the type of the current sub goal ($\MO{Type}$)

125+\item Get the type of the current sub goal ($\MO{Type}$).

112−\item Retrieve the local context $\Gamma$ at the current sub goal ($\MO{Context}$)

126+\item Retrieve the local context $\Gamma$ at the current sub goal.

127+($\MO{Context}$)

113−\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative to $\Gamma$

128+\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative

129+to $\Gamma$.

114\end{itemize}

130\end{itemize}

115−\item \demph{Unification}, which unifies two terms (potentially solving sub goals)

131+\item \demph{Unification}, which unifies two terms (potentially solving sub

116−relative to $\Gamma$

132+goals) relative to $\Gamma$. This may introduce new unification problems

133+to the proof state.

117\item \demph{Tactics} which update the proof term. Tactics operate on the sub term

134\item \demph{Tactics} which update the proof term. Tactics operate on the sub term

118at the binder specified by the head of the hole queue $\vQ$.

135at the binder specified by the head of the hole queue $\vQ$.

119\item \demph{Focussing} on a specific sub goal, which brings a different sub goal to the

136\item \demph{Focussing} on a specific sub goal, which brings a different sub goal to the

@@ -122,18 +139,19 @@ head of the hole queue.

122%$\vC$ which solves the sub goal.

139%$\vC$ which solves the sub goal.

123\end{itemize}

140\end{itemize}

124

141

125−Elaboration of an \Idris{} expression involves creating a new proof state, running

142+Elaboration of an \Idris{} expression involves creating a new proof state,

126−a series of tactics to build a complete proof term, then retrieving and \remph{rechecking}

143+running a series of tactics to build a complete proof term, then retrieving and

127−the final proof term, which must be a \TT{} program (i.e. does not contain any of the

144+\remph{rechecking} the final proof term, which must be a \TT{} program (i.e.

128−\TTdev{} extensions). We call a sub-term which contains no hole or guess bindings

145+does not contain any of the \TTdev{} extensions). We call a sub-term which

129−\demph{pure}. Although a pure term does not contain hole or guess bindings, it may

146+contains no hole or guess bindings \demph{pure}. Although a pure term does not

147+contain hole or guess bindings, it may nevertheless \remph{refer} to hole- or

130−nevertheless \remph{refer} to hole- or guess-bound variables.

148+guess-bound variables.

131

149

132−The proof state is initialised with the $\MO{NewProof}$ operation. Given a global

150+The proof state is initialised with the $\MO{NewProof}$ operation. Given a

133−context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:

151+global context $\vC$, $\MO{NewProof}\:\vt$ sets up the proof state as:

134

152

135\DM{

153\DM{

136−(\vC, \cdot, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)

154+(\vC, \cdot, \hole{\vx}{\vt}\SC\vx, \langle\rangle, \langle\vx\rangle)

137}

155}

138

156

139The local context is initially empty, and the initial hole queue is the $\vx$ standing for

157The local context is initially empty, and the initial hole queue is the $\vx$ standing for

@@ -143,7 +161,7 @@ $\MO{NewTerm}\:\vt$ discards the proof term and hole queue, and

143updates the proof state to:

161updates the proof state to:

144

162

145\DM{

163\DM{

146−(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\vx\rangle)

164+(\vC, \Delta, \hole{\vx}{\vt}\SC\vx, \langle\rangle, \langle\vx\rangle)

147}

165}

148

166

149

167

@@ -201,6 +219,7 @@ are given explicitly, the application must be expanded.

201\newcommand{\Check}{\MO{Check}_\Gamma}

219\newcommand{\Check}{\MO{Check}_\Gamma}

202\newcommand{\Eval}{\MO{Normalise}_\Gamma}

220\newcommand{\Eval}{\MO{Normalise}_\Gamma}

203\newcommand{\Unify}{\MO{Unify}_\Gamma}

221\newcommand{\Unify}{\MO{Unify}_\Gamma}

222+\newcommand{\PrimUnify}{\MO{PrimUnify}_\Gamma}

204

223

205\subsection{Tactics}

224\subsection{Tactics}

206

225

@@ -211,6 +230,9 @@ may have side-effects including failure, or updating the proof state. We have th

211primitive meta-operations:

230primitive meta-operations:

212

231

213\begin{itemize}

232\begin{itemize}

233+\item $\MO{Get}$ and $\MO{Put}$ which allow direct access to the proof state.

234+% Focus and Unfocus don't need to be primitive, we could show in terms of

235+% Get and Put

214\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.

236\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.

215\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.

237\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.

216\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context

238\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context

@@ -220,13 +242,39 @@ if the expression is not well-typed.

220\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context

242\item $\Eval\:\ve$, which evaluates a well-typed expression $\ve$ relative to a context

221$\Gamma$, returning its normal form.

243$\Gamma$, returning its normal form.

222\item

244\item

223−$\Unify\:\ve_1\:\ve_2$,

245+$\PrimUnify\:\ve_1\:\ve_2$,

224−which unifies $\ve_1$ and $\ve_2$ by finding the values with which holes must be instantiated

246+which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which

225−for $\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$

247+holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative

226−(i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold). $\MO{Unify}$ will fail

248+to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).

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

249+\end{itemize}

250+

251+Unification is crucial to the success of elaboration --- it is unification

252+which finds values of implicit arguments, in particular. We do not require

253+unification to succeed immediately, in general, as instantiating a hole may

254+affect the solution to other unification problems. Instead,

255+$\MO{PrimUnify}$ may give one of the following results:

256+

257+\begin{itemize}

258+\item $\MO{Success}$, if there is a solution for $\ve_1$ and $\ve_2$.

259+\item $\MO{Failure}$, if no solution is found due to a failure to unify

260+sub-terms in normal form.

261+\item $\MO{Blocked}$, otherwise, in which case further elaboration may lead

262+to further refinement of the problem.

228\end{itemize}

263\end{itemize}

229

264

265+$\MO{Unify}$ attempts to solve the given unification problem using

266+$\MO{PrimUnify}$, then attempts to further refine existing problems in the proof

267+state. This operation is given in Figure \ref{unifyps}.

268+

269+\FFIG{

270+\mbox{\textbf{[UNIFY ALGORITHM GOES HERE] }}

271+%Show how it uses a PrimUnify

272+%operation to update

273+%the proof state with new problems, and solve the old ones

274+}

275+{The $\MO{Unify}$ meta-operation}

276+{unifyps}

277+

230\demph{Tactics} are meta-operations which operate on the sub-term given

278\demph{Tactics} are meta-operations which operate on the sub-term given

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

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

232

280

@@ -278,7 +326,7 @@ solve other holes by unifying the expected type of $\vx$ with the type of $\vv$:

278 \MoRet{\RW{do}\:\AR{

326 \MoRet{\RW{do}\:\AR{

279 \vT' \leftarrow \Check\:\vv\\

327 \vT' \leftarrow \Check\:\vv\\

280 \Unify\:\vT\:\vT'\\

328 \Unify\:\vT\:\vT'\\

281− \RW{return}\:\guess{\vx}{\vT}{\vv'}\SC\ve}

329+ \RW{return}\:\guess{\vx}{\vT}{\vv}\SC\ve}

282 } \\

330 } \\

283}

331}

284}

332}

@@ -288,7 +336,7 @@ For example, consider the following proof term:

288

336

289\DM{

337\DM{

290\AR{

338\AR{

291−\hole{\vA}{\Set}\SC\hole{\vk}{\Nat}\SC

339+\hole{\vA}{\Type}\SC\hole{\vk}{\Nat}\SC

292\hole{\vx}{\vA}\SC\hole{\vxs}{\Vect\:\vA\:\vk}\SC

340\hole{\vx}{\vA}\SC\hole{\vxs}{\Vect\:\vA\:\vk}\SC

293\\

341\\

294\hole{\vys}{\Vect\:\vA\:(\suc\:\vk)}\SC\vys

342\hole{\vys}{\Vect\:\vA\:(\suc\:\vk)}\SC\vys

@@ -335,7 +383,7 @@ computational force. Once a term is complete in a guess binding, it may be subst

335scope of the binding safely.

383scope of the binding safely.

336In each of these tactics, if any step fails, or the term in focus does not take

384In each of these tactics, if any step fails, or the term in focus does not take

337the correct form (e.g. is not a guess in the case of $\MO{Solve}$ or not a hole

385the correct form (e.g. is not a guess in the case of $\MO{Solve}$ or not a hole

338−in the case of $\MO{Claim}$ and $\MO{Fill}$, the entire tactic fails. We can

386+in the case of $\MO{Claim}$ and $\MO{Fill}$) the entire tactic fails. We can

339handle failure using the $\MO{Try}$ tactic combinator:

387handle failure using the $\MO{Try}$ tactic combinator:

340

388

341\DM{

389\DM{

@@ -367,14 +415,14 @@ binding requires that the goal normalises to a function type:

367}

415}

368

416

369\noindent

417\noindent

370−Creating a $\forall$ binding requires that the goal is a $\TC{Set}$:

418+Creating a $\forall$ binding requires that the goal is a $\TC{Type}$:

371

419

372\DM{

420\DM{

373\PA{\A\A}{

421\PA{\A\A}{

374−\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Set}\SC\vx) &

422+\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Type}\SC\vx) &

375 \MoRet{\RW{do}\:\AR{

423 \MoRet{\RW{do}\:\AR{

376− \Set\:\leftarrow\:\Check\:\vS\\

424+ \Type\:\leftarrow\:\Check\:\vS\\

377− \RW{return}\:\all{\vn}{\vS}\SC\hole{\vx}{\Set}\SC\vx

425+ \RW{return}\:\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx

378 }

426 }

379 }

427 }

380}

428}

@@ -387,7 +435,7 @@ Creating a $\LET$ binding requires a type and a value.

387\PA{\A\A}{

435\PA{\A\A}{

388\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &

436\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &

389 \MoRet{\RW{do}\:\AR{

437 \MoRet{\RW{do}\:\AR{

390− \Set\:\leftarrow\:\Check\:\vS\\

438+ \Type\:\leftarrow\:\Check\:\vS\\

391 \vS'\:\leftarrow\:\Check\:\vv\\

439 \vS'\:\leftarrow\:\Check\:\vv\\

392 \Unify\:\vS\:\vS'\\

440 \Unify\:\vS\:\vS'\\

393 \RW{return}\:\LET\:\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx

441 \RW{return}\:\LET\:\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx

@@ -420,7 +468,7 @@ with the pattern variable directly:

420\PA{\A\A}{

468\PA{\A\A}{

421\MO{Pat}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\ve) &

469\MO{Pat}_\Gamma & \vn & (\hole{\vx}{\vT}\SC\ve) &

422 \MoRet{\RW{do}\:\AR{

470 \MoRet{\RW{do}\:\AR{

423− \MO{PatBind}\:(\vx\Hab\vT)\\

471+ \MO{PatBind}\:(\vn\Hab\vT)\\

424 \RW{return}\:\ve[\vn/\vx]

472 \RW{return}\:\ve[\vn/\vx]

425 }}

473 }}

426}

474}

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

445

493

446\DM{

494\DM{

447\AR{

495\AR{

448−\FN{id}\Hab\all{\vA}{\Set}\SC\all{\va}{\vA}\SC\vA \\

496+\FN{id}\Hab\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\

449−\FN{id}\:=\:\lam{\vA}{\Set}\SC\lam{\va}{\vA}\SC\va

497+\FN{id}\:=\:\lam{\vA}{\Type}\SC\lam{\va}{\vA}\SC\va

450}

498}

451}

499}

452

500

@@ -459,7 +507,7 @@ Note that the types on each $\MO{Lambda}$ are solved by unification:

459\AR{

507\AR{

460\MO{MkId}\:\mq\:\RW{do}\:

508\MO{MkId}\:\mq\:\RW{do}\:

461 \AR{

509 \AR{

462− \MO{NewProof}\:\all{\vA}{\Set}\SC\all{\va}{\vA}\SC\vA \\

510+ \MO{NewProof}\:\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\

463 \MO{RunTac}\;\MO{Attack} \\

511 \MO{RunTac}\;\MO{Attack} \\

464 \MO{RunTac}\;(\MO{Lambda}\;\vA) \\

512 \MO{RunTac}\;(\MO{Lambda}\;\vA) \\

465 \MO{RunTac}\;\MO{Attack} \\

513 \MO{RunTac}\;\MO{Attack} \\

@@ -494,8 +542,8 @@ a Coq proof script.

494\AR{

542\AR{

495\MO{MkIdType}\:\mq\:\RW{do}\;

543\MO{MkIdType}\:\mq\:\RW{do}\;

496 \AR{

544 \AR{

497− \MO{NewProof}\:\Set\\

545+ \MO{NewProof}\:\Type\\

498− \MO{Attack} ; \MO{Pi}\:(\vA\Hab\Set) ;

546+ \MO{Attack} ; \MO{Pi}\:(\vA\Hab\Type) ;

499 \MO{Attack} ; \MO{Pi}\:(\va\Hab\vA) \\

547 \MO{Attack} ; \MO{Pi}\:(\va\Hab\vA) \\

500 \MO{Fill}\;\vA \\

548 \MO{Fill}\;\vA \\

501 \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\

549 \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\

@@ -741,7 +789,7 @@ scope of the binding.

741\ttinterp{\piexp{\vx}{\vt}\ve}\:\mq\:

789\ttinterp{\piexp{\vx}{\vt}\ve}\:\mq\:

742\RW{do}\:

790\RW{do}\:

743\AR{

791\AR{

744−\MO{Attack};\;\MO{Claim}\:(\vX\Hab\Set)\\

792+\MO{Attack};\;\MO{Claim}\:(\vX\Hab\Type)\\

745\MO{Pi}\:(\vx\Hab\vX)\\

793\MO{Pi}\:(\vx\Hab\vX)\\

746\MO{Focus}\:\vX\\

794\MO{Focus}\:\vX\\

747\ttinterp{\vt};\;

795\ttinterp{\vt};\;

@@ -767,7 +815,7 @@ $\vV$ and $\vX$.

767\ttinterp{\ilet{\vx}{\vv}\:{\ve}}\:\mq\:\RW{do}\:

815\ttinterp{\ilet{\vx}{\vv}\:{\ve}}\:\mq\:\RW{do}\:

768\AR{

816\AR{

769\MO{Attack};\;

817\MO{Attack};\;

770−\MO{Claim}\:(\vX\Hab\Set);\;

818+\MO{Claim}\:(\vX\Hab\Type);\;

771\MO{Claim}\:(\vV\Hab\vX)\\

819\MO{Claim}\:(\vV\Hab\vX)\\

772\MO{Let}\:(\vx\Hab\vX\defq\vV)\\

820\MO{Let}\:(\vx\Hab\vX\defq\vV)\\

773\MO{Focus}\:\vV\\

821\MO{Focus}\:\vV\\

@@ -872,7 +920,7 @@ the function or argument which helps with unification:

872\DM{

920\DM{

873\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:

921\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:

874\AR{

922\AR{

875−\MO{Claim}\:(\vA\Hab\Set);\;\MO{Claim}\:(\vB\Hab\Set)\\

923+\MO{Claim}\:(\vA\Hab\Type);\;\MO{Claim}\:(\vB\Hab\Type)\\

876\MO{Claim}\:(\vf\Hab\vA\to\vB);\;\MO{Claim}\:(\vs\Hab\vA)\\

924\MO{Claim}\:(\vf\Hab\vA\to\vB);\;\MO{Claim}\:(\vs\Hab\vA)\\

877\MO{Try}\:

925\MO{Try}\:

878\AR{

926\AR{

@@ -907,7 +955,7 @@ as a \TT{} declaration:

907

955

908\DM{

956\DM{

909\MO{Elab}\:(\vx\Hab\vt)\:\mq

957\MO{Elab}\:(\vx\Hab\vt)\:\mq

910−\:\edo{\MO{NewProof}\:\Set\\

958+\:\edo{\MO{NewProof}\:\Type\\

911 \ttinterp{\vt}\\

959 \ttinterp{\vt}\\

912 \vt'\gets\MO{Term}\\

960 \vt'\gets\MO{Term}\\

913 \MO{TTDecl}\:(\vx\Hab\vt')

961 \MO{TTDecl}\:(\vx\Hab\vt')

@@ -928,7 +976,7 @@ adds a \TT{} data declaration.

928\DM{

976\DM{

929\AR{

977\AR{

930\MO{Elab}\:(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\

978\MO{Elab}\:(\idata\;\ihab{\vx}{\vt}\;\iwhere\;\tc)\\

931−\hg\hg\mq\:\edo{\MO{NewProof}\:\Set\\

979+\hg\hg\mq\:\edo{\MO{NewProof}\:\Type\\

932 \ttinterp{\vt}\\

980 \ttinterp{\vt}\\

933 \vt'\gets\MO{Term}\\

981 \vt'\gets\MO{Term}\\

934 \MO{TTDecl}\:(\vx\Hab\vt')\\

982 \MO{TTDecl}\:(\vx\Hab\vt')\\

@@ -937,7 +985,7 @@ adds a \TT{} data declaration.

937}

985}

938\AR{

986\AR{

939\MO{ElabCon}\:(\vx\Hab\vt)\\

987\MO{ElabCon}\:(\vx\Hab\vt)\\

940−\hg\hg\mq\: \edo{\MO{NewProof}\:\Set\\

988+\hg\hg\mq\: \edo{\MO{NewProof}\:\Type\\

941 \ttinterp{\vt}\\

989 \ttinterp{\vt}\\

942 \vt'\gets\MO{Term}\\

990 \vt'\gets\MO{Term}\\

943 \RW{return}\:(\vx\Hab\vt')

991 \RW{return}\:(\vx\Hab\vt')

@@ -962,7 +1010,7 @@ This can be achieved without any change to the elaborator by defining

962a type $\TC{Infer}$:

1010a type $\TC{Infer}$:

963

1011

964\DM{

1012\DM{

965−\Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer}

1013+\Data\hg\TC{Infer}\Hab\Type\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Type}\SC\va\to\TC{Infer}

966}

1014}

967

1015

968Now elaboration of the left hand side proceeds by elaborating $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and

1016Now elaboration of the left hand side proceeds by elaborating $\DC{MkInfer}\:\_\:(\vx\:\ttt)$ and

@@ -1123,7 +1171,7 @@ declaration is translated to:

1123

1171

1124\begin{SaveVerbatim}{showdata}

1172\begin{SaveVerbatim}{showdata}

1125

1173

1126−data Show : Set -> Set where

1174+data Show : Type -> Type where

1127 instanceShow : (show : a -> String) -> Show a

1175 instanceShow : (show : a -> String) -> Show a

1128

1176

1129show : Show a -> a -> String

1177show : Show a -> a -> String

@@ -1182,7 +1230,7 @@ This translates to:

1182

1230

1183\begin{SaveVerbatim}{orddata}

1231\begin{SaveVerbatim}{orddata}

1184

1232

1185−data Ord : Set -> Set where

1233+data Ord : Type -> Type where

1186 instanceOrd : Eq a => (compare : a -> a -> Ordering) ->

1234 instanceOrd : Eq a => (compare : a -> a -> Ordering) ->

1187 (max : a -> a -> a) -> Ord a

1235 (max : a -> a -> a) -> Ord a

1188

1236

@@ -1223,7 +1271,7 @@ In general, \texttt{class} declarations are elaborated as follows:

1223\mq\:\RW{do}\:\AR{

1271\mq\:\RW{do}\:\AR{

1224(\vec{\VV{meth}}\Hab\ttt)\gets\td\\

1272(\vec{\VV{meth}}\Hab\ttt)\gets\td\\

1225\MO{Elab}\:

1273\MO{Elab}\:

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

1274+\AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Type\:\iwhere\\

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

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

1228}

1276}

1229}

1277}

@@ -1418,7 +1466,7 @@ We can inspect the type of \texttt{append\_rec} at the \Idris{} prompt:

1418\begin{SaveVerbatim}{appendrec}

1466\begin{SaveVerbatim}{appendrec}

1419

1467

1420*vec> :t append_rec

1468*vec> :t append_rec

1421−append_rec : (a : Set) -> (m : Nat) -> (n : Nat) -> a ->

1469+append_rec : (a : Type) -> (m : Nat) -> (n : Nat) -> a ->

1422 Vect a n -> Vect a m -> Vect a (n + m)

1470 Vect a n -> Vect a m -> Vect a (n + m)

1423

1471

1424\end{SaveVerbatim}

1472\end{SaveVerbatim}

papers/impl-paper/hll.tex+11−12

@@ -192,7 +192,7 @@ literature. In \Idris{}, vectors are declared as follows:

192

193\begin{SaveVerbatim}{vect}

194

195−data Vect : Set -> Nat -> Set where

195+data Vect : Type -> Nat -> Type where

196 Nil : Vect a O

197 (::) : a -> Vect a k -> Vect a (S k)

198

@@ -209,7 +209,7 @@ This declares a family of types, which requires a different form of declaration

209from the simple type declarations above. It resembles a Haskell GADT

210declaration: it explicitly states the type

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

212−argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}

212+argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}

213is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each

214constructor targets a different part of the family of types. \tDC{Nil} can only

215be used to construct vectors with zero length, and \tDC{::} to construct

@@ -239,7 +239,7 @@ They are declared as follows in the library:

239

240\begin{SaveVerbatim}{findecl}

241

242−data Fin : Nat -> Set where

242+data Fin : Nat -> Type where

243 fO : Fin (S k)

244 fS : Fin k -> Fin (S k)

245

@@ -316,19 +316,18 @@ their types, to be inferred by the machine. These types could also be given expl

316

317\begin{SaveVerbatim}{vindeximpty}

318

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

319+index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a

320

321\end{SaveVerbatim}

322\useverb{vindeximpty}

323

324\noindent

325−Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in

325+Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are

326−applications of \texttt{index}; their values can be inferred from the types of

326+not given in applications of \texttt{index}; their values can be inferred from

327−the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter

327+the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which

328−or index in a type declaration, but which is otherwise free, will be automatically

328+appears as a parameter or index in a type declaration, but which is otherwise

329−bound as an implicit argument. Indeed, binding arguments in this way is the essence

329+free, will be automatically bound as an implicit argument. Implicit arguments

330−of dependent types.

331−Implicit arguments can still be given explicitly in applications, using the syntax

330+can still be given explicitly in applications, using the syntax

332\texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:

331\texttt{\{a=value\}} and \texttt{\{n=value\}}, for example:

333

332

334\begin{SaveVerbatim}{vindexexp}

333\begin{SaveVerbatim}{vindexexp}

@@ -577,7 +576,7 @@ plus one:

577

576

578\begin{SaveVerbatim}{parity}

577\begin{SaveVerbatim}{parity}

579

578

580−data Parity : Nat -> Set where

579+data Parity : Nat -> Type where

581 even : Parity (n + n)

580 even : Parity (n + n)

582 odd : Parity (S (n + n))

581 odd : Parity (S (n + n))

583

582

papers/impl-paper/intro.tex+18−18

@@ -39,12 +39,12 @@ How can we achieve both of these goals?

40This paper describes a method for elaborating a high level dependently typed

41functional programming language to a low level core language based on dependent

42−type theory. The method involves building an Embedded Domain Specific Language

42+type theory. The method involves building an elaboration monad which captures

43−(EDSL) for constructing programs in the core language, using \emph{tactics}

43+the state of incomplete programs and a collection of \emph{tactics} for

44−directed by high level program syntax.

44+refining programs, directed by high level program syntax. As we shall see,

45−As we shall see, this method allows higher level language constructs to be

45+this method allows higher level language constructs to be constructed in a

46−constructed in a straightforward manner, without compromising the simplicity

46+straightforward manner, without compromising the simplicity of the underlying

47−of the underlying type theory.

47+type theory.

49\subsection{Contributions}

@@ -55,18 +55,18 @@ unification algorithm \cite{Miller1992} and an evaluator. However, it is less

55well understood how to combine these components effectively into a practical

56programming language.

58−The primary contribution of this paper is

58+The primary contribution of this paper is a tactic based method for translating

59−an EDSL based method for translating programs in a

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

59+programs in a high level dependently typed programming language to a small core

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

60+type theory, \TT{}, based on UTT \cite{luo1994}. The paper describes the

61+structure of an elaboration monad capturing proof and system state, and

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

62+introduces a collection of \remph{tactics} for manipulating incomplete

63−for manipulating incomplete programs.

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

63+programs. Secondly, the paper gives a detailed description of the core type

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

64+theory used by \Idris{}, including a full description of the typing rules.

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

65+Finally, through describing the specific tactics, the paper shows how to extend

67−\Idris{} with higher level features.

66+\Idris{} with higher level features. While we apply these ideas to \Idris{}

68−While we apply these ideas to \Idris{} specifically, the method for term construction

67+specifically, the method for term construction is equally applicable to other

69−is equally applicable to other typed programming languages.

68+typed programming languages, and indeed the tactics themselves are applicable

69+to any high level language which can be explained in terms of \TT{}.

71The paper is structured as follows: Section \ref{sect:hll} gives an overview of

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

papers/impl-paper/library.bib+1982−1036

@@ -1,126 +1,163 @@

1−Automatically generated by Mendeley 1.3.1

1+Automatically generated by Mendeley 1.6

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

4−@book{Chlipala2012,

4+@inproceedings{Sozeau2008,

5−author = {Chlipala, Adam},

5+author = {Sozeau, Matthieu and Oury, Nicolas},

6−file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/Unknown/Chlipala - 2012 - Certified Programming with Dependent Types.pdf:pdf},

6+booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs 2008})},

7−title = {{Certified Programming with Dependent Types}},

7+file = {:Users/edwin/Downloads/10.1.1.175.9556.pdf:pdf},

8+pages = {278----293},

9+title = {{First-Class Type Classes}},

8−year = {2012}

10+year = {2008}

11}

10−@inproceedings{czarnecki2004dsl,

12+@inproceedings{McBride2006,

11−author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},

13+author = {McBride, C and Goguen, H and McKinna, J},

12−booktitle = {Domain-Specific Program Generation},

14+booktitle = {Types for Proofs and Programs {(TYPES 2006)}},

13−file = {:Users/edwin/Documents/Mendeley Desktop/Czarnecki et al/Domain-Specific Program Generation/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},

15+title = {{A few constructions on constructors}},

14−pages = {51--72},

15−publisher = {Springer},

16−title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},

17−url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},

16+url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},

18−year = {2004}

17+year = {2006}

19}

18}

20−@phdthesis{Brady2005,

19+@article{McBride2005,

21−author = {Brady, Edwin},

20+author = {McBride, Conor},

22−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Unknown/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},

21+editor = {Vene, Varmo and Uustalu, Tarmo},

22+isbn = {3540285407},

23+journal = {Advanced Functional Programming},

23keywords = {Dependent Types},

24keywords = {Dependent Types},

24mendeley-tags = {Dependent Types},

25mendeley-tags = {Dependent Types},

25−school = {University of Durham},

26+pages = {130--170},

26−title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},

27+publisher = {Springer},

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

28+series = {Lecture Notes in Computer Science},

29+title = {{Epigram: Practical programming with dependent types}},

30+url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},

31+volume = {3622},

28year = {2005}

32year = {2005}

29}

33}

30−@inproceedings{Kimmell2012,

34+@article{Okasaki1993,

31−author = {Kimmell, G and Stump, A and {Eades III}, HD and Fu, Peng and Sheard, Tim and Weirich, S and Casinghino, C and Sj\"{o}berg, V and Collins, N and Ahn, KY},

35+author = {Okasaki, Chris},

32−booktitle = {Programming Languages meets Program Verification},

36+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

33−file = {:Users/edwin/Documents/Mendeley Desktop/Kimmell et al/Programming Languages meets Program Verification/Kimmell et al. - 2012 - Equational reasoning about programs with general recursion and call-by-value semantics.pdf:pdf},

37+journal = {Journal of functional programming},

34−title = {{Equational reasoning about programs with general recursion and call-by-value semantics}},

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

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

36−year = {2012}

37−}

38−@article{Epstein2011,

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

40−institution = {Microsoft Research},

41−journal = {researchmicrosoftcom},

42−number = {Section 8},

43−pages = {1--12},

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

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

46−year = {2011}

39+year = {1993}

47}

40}

48−@article{Altenkirch2010a,

41+@inproceedings{Hancock2000,

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

42+author = {Hancock, Peter and Setzer, Anton},

50−author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},

43+booktitle = {{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}},

51−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Mcbride, Morris/Citeseer/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},

44+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hancock, Setzer - 2000 - Interactive Programs in Dependent Type Theory.pdf:pdf},

52−journal = {Citeseer},

45+isbn = {3-540-67895-6},

53−publisher = {Citeseer},

46+month = aug,

54−title = {{Generic Programming with Dependent Types}},

47+pages = {317--331},

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

48+title = {{Interactive Programs in Dependent Type Theory}},

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

56−year = {2010}

50+year = {2000}

57}

51}

58−@article{fisher2006next,

52+@article{Turner2004,

59−author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},

53+author = {Turner, D A},

60−file = {:Users/edwin/Documents/Mendeley Desktop/Fisher, Mandelbaum, Walker/Journal of the ACM/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},

54+file = {:Users/edwin/Downloads/10.1.1.106.364.pdf:pdf},

61−journal = {Journal of the ACM},

55+journal = {Journal of Universal Computer Science},

56+keywords = {functional programming},

62−number = {2},

57+number = {7},

63−pages = {1--51},

58+pages = {751----768},

64−publisher = {ACM},

59+title = {{Total Functional Programming}},

65−title = {{The next 700 data description languages}},

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

67−volume = {15},

60+volume = {10},

68−year = {2010}

61+year = {2004}

69}

62}

70−@misc{The2012b,

63+@phdthesis{norell2007thesis,

71−author = {Brooks, Fred},

64+author = {Norell, Ulf},

72−doi = {10.1093/epirev/mxr031},

65+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},

73−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},

66+keywords = {Dependent Types},

74−isbn = {9780321702081},

67+mendeley-tags = {Dependent Types},

75−issn = {1478-6729},

68+publisher = {Citeseer},

76−pmid = {22215642},

69+school = {Chalmers University of Technology},

77−title = {{The Design of Design Chapter 1}}

70+title = {{Towards a practical programming language based on dependent type theory}},

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

72+year = {2007}

78}

73}

79−@article{Chapman2005epigram,

74+@article{Wu,

80−author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},

75+annote = {1,3

81−file = {:Users/edwin/Documents/Mendeley Desktop/Chapman, Altenkirch, McBride/Trends in Functional Programming/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},

76+

82−journal = {Trends in Functional Programming},

77+

83−publisher = {Intellect Books},

78+This paper describes a solution, in Haskell, of the 2012 ICFP Programming Contest task, explaining in particular how Haskell's laziness and higher order functions helped to build a solution in limited time. I enjoyed reading this paper as an experience report - it provides evidence for the importance of high level features such as purity and laziness (for example when describing the GameTrie), and shows that Haskell can handle more realistic, practical, problems such as concurrency and exceptions (for example when dealing gracefully with timeout and communication between solving threads).

84−title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},

79+

85−url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},

80+

86−year = {2005}

81+My main concern with the paper is that it reads as if the reader is already familiar with the contest task. It would be useful to be more precise about the task itself in the introduction, rather than by making it implicit from the code samples. Section 1.1 describes the problem, but only in general terms - I think it would be worth extending this, and correspondingly removing some of the code. In particular, 'stepRobot' and 'updRocks' would probably be fine just with their type signatures if the problem specification was more precise.

82+

83+ },

84+author = {Wu, Nicolas and Magalh\~{a}es, Jos\'{e} Pedro and Bransen, Jeroen and Swierstra, Wouter},

85+file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_14.pdf:pdf},

86+title = {{Pure and Lazy Lambda Mining}}

87}

88−@misc{TheMendeleySupportTeam2011,

88+@inproceedings{NanevskiAAMorrisett2008,

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

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

90−address = {London},

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

91−author = {{The Mendeley Support Team}},

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

92−booktitle = {Mendeley Desktop},

92+doi = {10.1145/1411204.1411237},

93−file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/Mendeley Desktop/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

93+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},

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

94+isbn = {9781595939197},

95+issn = {15232867},

96+keywords = {Dependent Types},

97+mendeley-tags = {Dependent Types},

98+number = {9},

95−pages = {1--16},

99+pages = {229--240},

96−publisher = {Mendeley Ltd.},

100+title = {{Ynot: Dependent types for imperative programs}},

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

101+url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},

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

102+volume = {43},

99−year = {2011}

103+year = {2008}

100}

104}

101−@phdthesis{Okasaki1996,

105+@article{Walt,

102−author = {Okasaki, Chris},

106+annote = {-1, 5

103−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Unknown/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},

107+

104−school = {Carnegie Mellon University},

108+

105−title = {{Purely Functional Data Structures}},

109+This paper describes the use of Agda's reflection mechanism to help with proof automation, and gives some simple examples, including proving evenness of natural numbers and proving that a boolean formula is a tautology.

106−year = {1996}

110+

111+

112+It seems that proof automation is important for a practical language with dependent types, and Agda's reflection mechanism as described is likely to help. However, this paper only really scratches the surface of what is possible - existing (unpublished, as far as I'm aware) examples such as the Ring solver go much further towards demonstrating its value.

113+

114+

115+The 'Evenness' example uses a lot of space for something pretty simple. An in practice, the number won't necessarily be known. What if you know "Even x" and need to prove "Even (x + 100)". Does it still work? Similarly for the tautology example - what if there is an unknown formula which is nevertheless known to be a tautology? It would be nice, therefore, to show how such proof obligations come up in practice and how the reflection techniques described help. Without this, it's not clear that the paper answers the given central question of whether Agda's reflective capabilities are sufficient and practically usable.

116+

117+

118+In summary: there's some nice tutorial material here describing reflection and its application, but I don't think there is enough depth for it to be really interesting.

119+

120+

121+Minor comments

122+

123+

124+The fonts and layout look wrong. Is this the proper LaTeX class? Also remember that the colour won't come out in print...

125+

126+

127+p2 "new" keywords seems wrong for a technique was has been aroundfor a couple of years. I know it hasn't been written up elsewhere, but I'd omit the word "new"

128+

129+

130+p3 "This is why we have decidable equality" - can you explain what you mean by this, for the non-Agda expert?

131+

132+

133+Vars are naturals - so they are de Bruijn indexed?

134+

135+

136+p5 "Other terms are rejected" - what does it mean for a term to be rejected? i.e. what is the effect? The text hints that this is a type error, since there is a suggestion that a proof is needed to show it is valid, but it would be good to be explicit.

137+

138+

139+p8 I'm not sure I'd go as far as to say it's "trivial" to show that (1) is a tautology, but I agree it should be easy, if tedious.},

140+author = {Walt, Paul Van Der and Swierstra, Wouter},

141+file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_22.pdf:pdf},

142+title = {{Engineering Proof by Reflection in Agda}}

107}

143}

108−@article{mcbride2008functional,

144+@article{Jones2003,

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

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

110−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Journal of functional programming/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},

146+author = {Jones, Simon Peyton},

111−journal = {Journal of functional programming},

147+editor = {Jones, Simon Peyton},

148+isbn = {0521826144},

149+journal = {Language},

112number = {1},

150number = {1},

113−pages = {1--13},

114−publisher = {Cambridge Univ Press},

151+publisher = {Cambridge University Press},

115−title = {{Functional pearl: Applicative programming with effects}},

152+title = {{Haskell 98 Language and Libraries The Revised Report}},

116−url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=1457860},

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

117−volume = {18},

154+volume = {13},

118−year = {2008}

155+year = {2003}

119}

156}

120@inproceedings{madhavapeddy2007melange,

157@inproceedings{madhavapeddy2007melange,

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

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

122booktitle = {ACM SIGOPS Operating Systems Review},

159booktitle = {ACM SIGOPS Operating Systems Review},

123−file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/ACM SIGOPS Operating Systems Review/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},

160+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},

124number = {3},

161number = {3},

125pages = {101--114},

162pages = {101--114},

126publisher = {ACM},

163publisher = {ACM},

@@ -129,243 +166,228 @@ url = {http://dl.acm.org/citation.cfm?id=1273009},

129volume = {41},

166volume = {41},

130year = {2007}

167year = {2007}

131}

168}

132−@inproceedings{lempsink2009type,

169+@inproceedings{czarnecki2004dsl,

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

170+author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},

134−booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},

171+booktitle = {Domain-Specific Program Generation},

135−file = {:Users/edwin/Documents/Mendeley Desktop/Lempsink, Leather, L\"{o}h/Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},

172+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},

136−pages = {61--72},

173+pages = {51--72},

137−publisher = {ACM},

174+publisher = {Springer},

138−title = {{Type-safe diff for families of datatypes}},

175+title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},

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

176+url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},

140−year = {2009}

177+year = {2004}

141}

178}

142−@book{Approach2012,

179+@article{Wadler2001,

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

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

144−booktitle = {Carcinogenesis},

181+author = {Wadler, Philip},

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

182+doi = {10.1007/3-540-59451-5_2},

146−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},

183+editor = {Jeuring, Johan and Meijer, Erik},

147−isbn = {020161622X},

184+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Wadler - 2001 - Monads for functional programming.pdf:pdf},

148−issn = {1460-2180},

185+isbn = {3540594515},

186+issn = {03029743},

187+journal = {Advanced Functional Programming},

149−number = {3},

188+number = {August 1992},

150−pmid = {22383472},

189+pages = {24--52},

151−title = {{The Pragmatic Programmer Chapter 2}},

190+publisher = {Springer},

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

191+series = {Lecture Notes in Computer Science},

192+title = {{Monads for functional programming}},

193+url = {http://www.springerlink.com/index/715264614rh13340.pdf},

153−volume = {33}

194+volume = {925},

195+year = {2001}

154}

196}

197+@phdthesis{Boquist1999,

198+author = {Boquist, Urban},

199+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Boquist - 1999 - Code optimisation techniques for lazy functional languages.pdf:pdf},

200+title = {{Code optimisation techniques for lazy functional languages}},

201+url = {http://mirror.seize.it/papers/Code Optimization Techniques for Lazy Functional Languages.pdf},

202+year = {1999}

203+}

155−@inproceedings{stump2010resource,

204+@inproceedings{Taha2003,

156−author = {Stump, A. and Austin, E.},

205+author = {Taha, Walid and Nielsson, Michael Florentin},

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

206+booktitle = {Principles of Programming Languages},

158−file = {:Users/edwin/Documents/Mendeley Desktop/Stump, Austin/Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

207+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Taha, Nielsson - 2003 - Environment Classifiers.pdf:pdf},

208+isbn = {1581136285},

209+keywords = {linear,modal logic,multi-stage programming,temporal logic,type safety,type systems},

210+title = {{Environment Classifiers}},

211+year = {2003}

212+}

213+@article{Brady2012a,

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

215+doi = {10.1093/geront/gns026},

216+file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter24BeautifulConcurre.pdf:pdf},

217+isbn = {9780596510046},

218+issn = {1758-5341},

219+journal = {The Gerontologist},

220+month = dec,

221+number = {6},

159−pages = {27--38},

222+pages = {NP},

160−publisher = {ACM},

223+pmid = {23150082},

161−title = {{Resource typing in Guru}},

224+title = {{Beautiful Code Chapter 24}},

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

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

226+volume = {52},

163−year = {2010}

227+year = {2012}

164}

228}

165@article{mcbride2010ornamental,

229@article{mcbride2010ornamental,

166author = {McBride, Conor},

230author = {McBride, Conor},

167−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Journal of Functional Programming/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},

231+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},

168journal = {Journal of Functional Programming},

232journal = {Journal of Functional Programming},

169title = {{Ornamental algebras, algebraic ornaments}},

233title = {{Ornamental algebras, algebraic ornaments}},

170url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},

234url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},

171year = {2010}

235year = {2010}

172}

236}

173−@article{Swierstra2011,

237+@inproceedings{Gall2012,

174−author = {Swierstra, W},

238+author = {Gall, Yann Le and Lee, Adam J and Kapdia, Apu},

175−file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra/Journal of Functional Programming/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},

239+booktitle = {SCMAT},

176−journal = {Journal of Functional Programming},

240+file = {:Users/edwin/Downloads/Papers/p219-legall.pdf:pdf},

177−number = {6},

241+isbn = {9781450312950},

242+keywords = {exposure,policy languages,privacy},

178−pages = {575----583},

243+pages = {219--228},

179−title = {{Sorted: Verifying the Problem of the {Dutch National} Flag in {Agda}}},

244+title = {{PlexC : A Policy Language for Exposure Control}},

180−url = {http://journals.cambridge.org/abstract_S0956796811000207},

181−volume = {21},

182−year = {2011}

245+year = {2012}

183}

246}

184−@article{McBride2002,

247+@article{Campbell-moore,

185−author = {McBride, C},

248+author = {Campbell-moore, Catrin},

186−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Types for proofs and programs ({TYPES 2000})/McBride - 2000 - Elimination with a Motive.pdf:pdf},

249+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Campbell-moore - Unknown - A Computable Infinitary Logic.pdf:pdf},

187−journal = {Types for proofs and programs ({TYPES 2000})},

250+pages = {1--10},

188−title = {{Elimination with a Motive}},

251+title = {{A Computable Infinitary Logic}}

189−url = {http://www.springerlink.com/index/vbpg19305t46f6dm.pdf},

190−year = {2000}

191}

252}

192−@article{Xi1998,

253+@misc{Resolution2012a,

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

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

194−author = {Xi, Hongwei and Pfenning, Frank},

195−doi = {10.1145/277652.277732},

196−file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/ACM Sigplan Notices/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},

197−isbn = {0897919874},

198−issn = {03621340},

199−journal = {ACM Sigplan Notices},

200−keywords = {Dependent Types},

201−mendeley-tags = {Dependent Types},

202−number = {5},

203−pages = {249--257},

204−publisher = {ACM},

205−series = {PLDI '98},

206−title = {{Eliminating array bound checking through dependent types}},

207−url = {http://portal.acm.org/citation.cfm?doid=277652.277732},

208−volume = {33},

209−year = {1998}

210−}

211−@misc{idristutorial,

212−author = {Brady, Edwin},

213−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Unknown/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},

214−title = {{Programming in Idris : a tutorial}},

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

216−year = {2012}

217−}

218−@book{Cryptography2012,

219−author = {Anderson, Ross},

220−doi = {10.1093/intimm/dxs023},

221−file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Unknown/Anderson - Unknown - Security Engineering Chapter 5.pdf:pdf},

222−isbn = {9780470068526},

223−issn = {1460-2377},

224−number = {4},

225−pmid = {22451589},

226−title = {{Security Engineering Chapter 5}},

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

228−volume = {24}

229−}

230−@inproceedings{NanevskiAAMorrisett2008,

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

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

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

234−doi = {10.1145/1411204.1411237},

235−file = {:Users/edwin/Documents/Mendeley Desktop/Nanevski A A Morrisett/International Conference on Functional Programming/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},

236−isbn = {9781595939197},

237−issn = {15232867},

238−keywords = {Dependent Types},

239−mendeley-tags = {Dependent Types},

240−number = {9},

241−pages = {229--240},

242−title = {{Ynot: Dependent types for imperative programs}},

243−url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},

244−volume = {43},

245−year = {2008}

246−}

247−@misc{Brady2012c,

248−author = {Brooks, Fred},

249doi = {10.1093/epirev/mxr031},

255doi = {10.1093/epirev/mxr031},

250−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},

256+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

251−isbn = {9780321702081},

252issn = {1478-6729},

257issn = {1478-6729},

253−number = {1},

254−pages = {NP},

255pmid = {22215642},

258pmid = {22215642},

256−title = {{The Design of Design Chapter 5}},

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

257−volume = {34}

258}

260}

259−@inproceedings{ko2011modularising,

261+@inproceedings{Pasalic2002,

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

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

261−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},

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

262−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Proceedings of the seventh ACM SIGPLAN workshop on Generic programming/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

264+doi = {10.1145/583852.581499},

265+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},

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

267+issn = {03621340},

268+keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},

269+month = sep,

270+number = {9},

263−pages = {13--24},

271+pages = {218--229},

264−publisher = {ACM},

272+title = {{Tagless staged interpreters for typed languages}},

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

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

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

274+volume = {37},

267−year = {2011}

275+year = {2002}

268}

276}

269−@book{Choosing2012,

277+@book{Projects,

270−author = {Fowler, Martin},

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

271−booktitle = {Carcinogenesis},

279+file = {:Users/edwin/Downloads/Safari/ThePragmaticProgrammerFromJourneymantoMasterChapter8PragmaticProjects.pdf:pdf},

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

280+isbn = {020161622X},

273−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Carcinogenesis/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},

281+title = {{The Pragmatic Programmer Chapter 8}}

274−isbn = {9780132107549},

275−issn = {1460-2180},

276−number = {3},

277−pmid = {22383472},

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

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

280−volume = {33}

281}

282}

282−@article{marlow2006making,

283+@inproceedings{Wadler1989,

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

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

284−file = {:Users/edwin/Documents/Mendeley Desktop/Marlow, Peyton Jones/Journal of Functional Programming/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},

285+author = {Wadler, Philip},

285−journal = {Journal of Functional Programming},

286+booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},

287+doi = {10.1145/99370.99404},

288+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Wadler - 1989 - Theorems for free!.pdf:pdf},

289+isbn = {0897913280},

286−number = {4-5},

290+number = {June},

287−pages = {415--449},

291+pages = {347--359},

288−publisher = {Cambridge University Press},

292+publisher = {ACM},

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

293+series = {FPCA '89},

294+title = {{Theorems for free!}},

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

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

291−volume = {16},

292−year = {2006}

296+year = {1989}

293}

297}

294−@article{Mandelbaum2007,

298+@inproceedings{swierstra2007beauty,

295−abstract = {Massive amounts of useful data are stored and processed in ad hoc formats for which common tools like parsers, printers, query engines and format converters are not readily available. In this paper, we explain the design and implementation of PADS/ML , a new language and system that facilitates the generation of data processing tools for ad hoc formats. The PADS/ML design includes features such as dependent, polymorphic and recursive datatypes, which allow programmers to describe the syntax and semantics of ad hoc data in a concise, easy-to-read notation. The PADS/ML implementation compiles these descriptions into ml structures and functors that include types for parsed data, functions for parsing and printing, and auxiliary support for user-specified, format-dependent and format-independent tool generation.},

299+author = {Swierstra, W. and Altenkirch, T.},

296−author = {Mandelbaum, Yitzhak and Fisher, Kathleen and Walker, David and Fernandez, Mary and Gleyzer, Artem},

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

297−doi = {10.1145/1190215.1190231},

301+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},

298−isbn = {1595935754},

299−issn = {03621340},

300−journal = {SIGPLAN Not},

301−number = {1},

302−pages = {77--83},

302+pages = {25--36},

303publisher = {ACM},

304−series = {POPL '07},

304+title = {{Beauty in the beast}},

305−title = {{PADS/ML: a functional data description language}},

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

306−url = {http://doi.acm.org/10.1145/1190216.1190231},

307−volume = {42},

308year = {2007}

306year = {2007}

309}

307}

310−@article{Abel2010,

308+@inproceedings{Xi1999,

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

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

312−author = {Abel, Andreas},

310+author = {Xi, Hongwei and Pfenning, Frank},

313−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/EPTCS/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},

311+booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},

314−journal = {EPTCS},

312+doi = {10.1145/292540.292560},

313+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},

314+isbn = {1581130953},

315+issn = {07439016},

316+keywords = {Dependent Types},

317+mendeley-tags = {Dependent Types},

318+organization = {Carnegie Mellon University},

315−pages = {1--15},

319+pages = {214--227},

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

320+publisher = {ACM Press},

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

321+series = {POPL '99},

322+title = {{Dependent types in practical programming}},

323+url = {http://portal.acm.org/citation.cfm?doid=292540.292560},

318−volume = {43},

324+volume = {26},

319−year = {2010}

325+year = {1999}

320}

326}

321−@article{Hoare1978,

327+@inproceedings{Kimmell2012,

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

328+author = {Kimmell, G and Stump, A and {Eades III}, HD and Fu, Peng and Sheard, Tim and Weirich, S and Casinghino, C and Sj\"{o}berg, V and Collins, N and Ahn, KY},

323−author = {Hoare, C A R},

329+booktitle = {Programming Languages meets Program Verification},

324−doi = {10.1016/0167-6423(87)90028-1},

330+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Kimmell et al. - 2012 - Equational reasoning about programs with general recursion and call-by-value semantics.pdf:pdf},

325−editor = {McKeag, R M and Macnaghten, A M},

331+title = {{Equational reasoning about programs with general recursion and call-by-value semantics}},

326−file = {:Users/edwin/Documents/Mendeley Desktop/Hoare/Communications of the ACM/Hoare - 1978 - Communicating sequential processes.pdf:pdf},

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

327−isbn = {0131532715},

333+year = {2012}

328−issn = {01676423},

334+}

329−journal = {Communications of the ACM},

335+@article{mccann2000packet,

336+author = {McCann, P.J. and Chandra, S.},

337+journal = {ACM SIGCOMM Computer Communication Review},

330−number = {8},

338+number = {4},

331−pages = {666--677},

339+pages = {321--333},

332−pmid = {2142694823583477576},

333publisher = {ACM},

340publisher = {ACM},

334−series = {International Series in Computer Science},

341+title = {{Packet types: abstract specification of network protocol messages}},

335−title = {{Communicating sequential processes}},

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

336−url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},

337−volume = {21},

343+volume = {30},

338−year = {1978}

344+year = {2000}

339}

345}

340−@book{Bird2010,

346+@article{McBride2007,

341−author = {Bird, Richard},

347+author = {McBride, Conor and Paterson, Ross},

342−file = {:Users/edwin/Documents/Mendeley Desktop/Bird/Unknown/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},

348+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},

343−isbn = {9780521513388},

349+journal = {Journal of functional programming},

344−title = {{Pearls of Functional Algorithm Design}},

350+title = {{Applicative programming with effects}},

351+url = {http://journals.cambridge.org/abstract_S0956796807006326},

345−year = {2010}

352+year = {2007}

346}

353}

347−@inproceedings{oury2008power,

354+@misc{Ferreira2012,

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

355+annote = {This paper explains how to compile Beluga, a programming language with higher order abstract syntax which is specifically designed to support data structures with binders. In particular, it aims to make it easy to reason about metatheory of programming languages by supporting name generation, alpha conversion and capture avoiding substitution.

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

356+

350−file = {:Users/edwin/Documents/Mendeley Desktop/Oury, Swierstra/International Conference on Functional Programming/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

357+

351−keywords = {Dependent Types},

358+In general, I liked this paper, primarily because it tackles an underrepresented problem - namely, taking a high level language with support for theorem proving and dependent types, and generating efficient executable code. This is clearly important if such high level languages are to be useful in practice, and even to demonstrate the usefulness and power of the language on anything other than small scale examples.

352−mendeley-tags = {Dependent Types},

359+

353−number = {9},

360+

354−pages = {39--50},

361+I think this paper can be accepted, though I have some small comments and suggestions for improvements:

355−publisher = {ACM},

362+

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

363+

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

364+The introductory example in section 2 provides a generally clear introduction to contextual objects, motivating the problem with a well-understood example. However, it would be nice to say more here about what the target of the compilation is (otherwise I'm not sure what you mean by using "simple names" here). You say: "The output is a fully annotated program using a representation close to the one presented by Cave and Pientka" - as well as the reference it would be very useful here to summarise what that representation is. There are a couple of instances of this, where some background is assumed, which would be good to explain in a couple of sentences in the early sections - e.g. it would also be useful to say what you mean by "Fresh-Style" earlier on.

358−volume = {43},

365+

366+

367+Section 4 - maybe give the informal description of fresh binders earlier?

368+

369+

370+p6-7 On dependency erasure - "The compiler keeps the simple types as a way of sanity check" - is this always true? It isn't true in general for dependent types (consider, for example, a function which computes a simple type) and certainly not with more aggressive dependency erasure such as forcing of constructor arguments which is implemented in Agda and Idris, for example.

371+

372+

373+p9 It seems that the type system is strong enough to support some optimisations on pattern match compilation - such as Epigram's detagging, where the result of a case split on one value informs what another value should be.

374+

375+

376+In related work, you don't mention any other compilers for dependently typed languages which have to tackle similar problems, though you do mention program extraction for Coq. There is also MAlonzo, which translates Agda to Haskell, and Epic (Trends in Functional Programming), used by Epigram, Agda and Idris, which deals with naming though in a much more limited way than this paper.},

377+author = {Ferreira, Francisco and Monnier, Stefan and Pientka, Brigitte},

378+file = {:Users/edwin/Downloads/Papers/plpv2013_submission_9.pdf:pdf},

379+keywords = {compilation,contextual objects,pattern matching},

380+title = {{Compiling Contextual Objects Bringing Higher-Order Abstract Syntax to Programmers}},

359−year = {2008}

381+year = {2012}

360}

382}

361−@inproceedings{madhavapeddy2010turning,

383+@misc{The2012b,

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

384+author = {Brooks, Fred},

363−booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},

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

364−file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Proceedings of the 2nd USENIX conference on Hot topics in cloud computing/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},

386+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},

365−publisher = {USENIX Association},

387+isbn = {9780321702081},

366−title = {{Turning down the LAMP: software specialisation for the cloud}},

388+issn = {1478-6729},

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

389+pmid = {22215642},

368−year = {2010}

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

369}

391}

370@book{peyton1987implementation,

392@book{peyton1987implementation,

371author = {{Peyton Jones}, S.L.},

393author = {{Peyton Jones}, S.L.},

@@ -374,390 +396,572 @@ title = {{The implementation of functional programming languages (prentice-hall

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

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

375year = {1987}

397year = {1987}

376}

398}

399+@article{Miller1992,

400+author = {Miller, Dale},

401+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},

402+journal = {Journal of Symbolic Computation},

403+title = {{Unification under a mixed prefix}},

404+url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},

405+year = {1992}

406+}

377−@inproceedings{Pasalic2002,

407+@inproceedings{Danielsson2010,

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

408+author = {Danielsson, Nils Anders},

379booktitle = {International Conference on Functional Programming},

409booktitle = {International Conference on Functional Programming},

380−doi = {10.1145/583852.581499},

410+doi = {10.1145/1932681.1863585},

381−file = {:Users/edwin/Documents/Mendeley Desktop/Pa\v{s}alic, Taha, Sheard/International Conference on Functional Programming/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},

411+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Danielsson - 2010 - Total parser combinators.pdf:pdf},

382−isbn = {1-58113-487-8},

412+isbn = {978-1-60558-794-3},

383issn = {03621340},

413issn = {03621340},

384−keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},

414+keywords = {dependent types,mixed induction and coinduction,parser combinators,productivity,termination},

385month = sep,

415month = sep,

386number = {9},

416number = {9},

387−pages = {218--229},

417+pages = {285},

388−title = {{Tagless staged interpreters for typed languages}},

418+title = {{Total parser combinators}},

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

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

390−volume = {37},

420+volume = {45},

391−year = {2002}

421+year = {2010}

392}

422}

393−@inproceedings{Brady2010,

423+@inproceedings{augustsson1999exercise,

394−author = {Brady, Edwin and Hammond, Kevin},

424+author = {Augustsson, L. and Carlsson, M.},

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

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

396−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Proceedings of the 15th ACM SIGPLAN international conference on Functional programming/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},

426+keywords = {Depe},

397−isbn = {9781605587943},

427+mendeley-tags = {Depe},

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

428+publisher = {Citeseer},

429+title = {{An exercise in dependent types: A well-typed interpreter}},

430+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2895},

431+year = {1999}

432+}

433+@inproceedings{Sheard2005,

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

435+author = {Sheard, Tim},

436+booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},

437+doi = {10.1145/1088348.1088356},

438+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},

439+isbn = {159593071X},

440+keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},

441+month = sep,

442+pages = {74--85},

443+publisher = {ACM Press},

444+title = {{Putting curry-howard to work}},

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

446+year = {2005}

447+}

448+@phdthesis{McBride1999,

449+author = {McBride, Conor},

450+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

451+keywords = {Dependent Types},

399mendeley-tags = {Dependent Types},

452mendeley-tags = {Dependent Types},

400−pages = {297--308},

453+school = {University of Edinburgh},

401−publisher = {ACM},

454+title = {{Dependently typed functional programs and their proofs}},

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

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

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

456+year = {1999}

457+}

458+@article{The2012a,

459+author = {Bentley, Jon},

460+doi = {10.1093/geront/gns026},

461+file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter3TheMostBeautiful.pdf:pdf},

462+isbn = {9780596510046},

463+issn = {1758-5341},

464+month = dec,

465+number = {6},

466+pages = {NP},

467+pmid = {23150082},

468+title = {{Beautiful Code Chapter 3}},

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

470+volume = {52},

404−year = {2010}

471+year = {2012}

405}

472}

406@inproceedings{Fournet2011,

473@inproceedings{Fournet2011,

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

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

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

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

409−file = {:Users/edwin/Documents/Mendeley Desktop/Fournet, Bhargavan, Gordon/Foundations of security analysis and design {VI}/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},

476+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},

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

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

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

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

412year = {2010}

479year = {2010}

413}

480}

414−@article{landin1966next,

481+@inproceedings{chlipala2010ur,

415−author = {Landin, P.J.},

482+author = {Chlipala, Adam},

416−file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Communications of the ACM/Landin - 1966 - The next 700 programming languages.pdf:pdf},

483+booktitle = {ACM SIGPLAN Notices},

417−journal = {Communications of the ACM},

484+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

418−number = {3},

485+number = {6},

419−pages = {157--166},

420−publisher = {ACM},

421−title = {{The next 700 programming languages}},

422−url = {http://dl.acm.org/citation.cfm?id=365257 )},

423−volume = {9},

424−year = {1966}

425−}

426−@inproceedings{bhargavan2010modular,

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

428−booktitle = {ACM Sigplan Notices},

429−number = {1},

430−pages = {445--456},

486+pages = {122--133},

431publisher = {ACM},

487publisher = {ACM},

432−title = {{Modular verification of security protocol code by typing}},

488+title = {{Ur: statically-typed metaprogramming with type-level record computation}},

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

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

434volume = {45},

490volume = {45},

435year = {2010}

491year = {2010}

436}

492}

437−@article{Haskell2012a,

493+@article{Fluet,

438−author = {Biancuzzi, F and Warden, S},

494+annote = {0,3

439−doi = {10.1093/epirev/mxr031},

495+

440−file = {:Users/edwin/Documents/Mendeley Desktop/Biancuzzi, Warden/Unknown/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

496+

441−isbn = {9780596801670},

497+This paper gives a control flow analysis for polymorphic functional programs (specifically System F with recursion). Surprisingly (to me at least) this appears not to have been done before, with previous analyses targetting dynamically typed or simply typed languages, or handling polymorphism by explicitly eliminating it. It seems to be a worthwhile exercise: richer static type systems should give more information to support static analysis.

442−issn = {1478-6729},

498+

443−pmid = {22215642},

499+

444−title = {{Masterminds of Programming Chapter 8}}

500+While I like what is achieved by this paper, I did find it rather hard going. The introduction feels laboured and then the paper covers a lot of detail (possibly too much) in quite a short space (though it still runs to 18 pages, two more than the limit!). I would suggest that the paper would be much improved, particularly to a non-expert reader, if it give one or more motivating examples in the introduction and showed how the analysis applied to these examples, when translated to ANF.

445−}

501+I think this would shorten the introduction and give a much better intuition for the rules.},

446−@book{Brady2012,

502+author = {Fluet, Matthew},

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

503+file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_6.pdf:pdf},

448−booktitle = {Carcinogenesis},

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

450−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},

451−isbn = {020161622X},

452−issn = {1460-2180},

453−number = {3},

454−pmid = {22383472},

455−title = {{The Pragmatic Programmer Chapter 5}},

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

457−volume = {33}

458−}

459−@article{McBride2007,

460−author = {McBride, Conor and Paterson, Ross},

461−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Journal of functional programming/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},

462−journal = {Journal of functional programming},

463−title = {{Applicative programming with effects}},

464−url = {http://journals.cambridge.org/abstract_S0956796807006326},

465−year = {2007}

466−}

467−@inproceedings{Altenkirch2010,

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

469−author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},

470−booktitle = {{FLOPS 2010}},

471−doi = {10.1007/978-3-642-12251-4_5},

472−editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},

473−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch et al/{FLOPS 2010}/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},

474−isbn = {9783642122507},

475−pages = {40----55},

476−publisher = {Springer Berlin Heidelberg},

477−series = {Lecture Notes in Computer Science},

478−title = {{Dependent Types without the Sugar}},

479−url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},

480−year = {2010}

481−}

482−@article{McBride2005,

483−author = {McBride, Conor},

484−editor = {Vene, Varmo and Uustalu, Tarmo},

485−isbn = {3540285407},

486−journal = {Advanced Functional Programming},

487−keywords = {Dependent Types},

488−mendeley-tags = {Dependent Types},

489−pages = {130--170},

504+pages = {1--18},

490−publisher = {Springer},

505+title = {{A Type- and Control-Flow Analysis for System F}}

491−series = {Lecture Notes in Computer Science},

492−title = {{Epigram: Practical programming with dependent types}},

493−url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},

494−volume = {3622},

495−year = {2005}

496}

506}

497−@article{Huet1997,

507+@article{Vytiniotis2011,

498−author = {Huet, G},

508+author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},

499−file = {:Users/edwin/Documents/Mendeley Desktop/Huet/{Journal of Functional Programming}/Huet - 1997 - The zipper.pdf:pdf},

509+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions.pdf:pdf;:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions(2).pdf:pdf},

500journal = {{Journal of Functional Programming}},

510journal = {{Journal of Functional Programming}},

501−number = {5},

511+number = {4--5},

502−pages = {549----554},

512+pages = {333----412},

503−title = {{The zipper}},

513+title = {{\textsc{OutsideIn}(X) Modular type inference with local assumptions}},

504−url = {http://journals.cambridge.org/abstract_S0956796897002864},

514+url = {http://journals.cambridge.org/abstract_S0956796811000098},

505−volume = {7},

515+volume = {21},

506−year = {1997}

516+year = {2011}

507}

517}

508@inproceedings{Gregoire2005,

518@inproceedings{Gregoire2005,

509author = {Gregoire, Benjamin and Mahboubi, Assia},

519author = {Gregoire, Benjamin and Mahboubi, Assia},

510booktitle = {{Theorem Proving in Higher Order Logics (TPHOLS 2005)}},

520booktitle = {{Theorem Proving in Higher Order Logics (TPHOLS 2005)}},

511−file = {:Users/edwin/Documents/Mendeley Desktop/Gregoire, Mahboubi/{Theorem Proving in Higher Order Logics (TPHOLS 2005)}/Gregoire, Mahboubi - 2005 - Proving Equalities in a Commutative Ring Done Right in Coq.pdf:pdf},

521+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Gregoire, Mahboubi - 2005 - Proving Equalities in a Commutative Ring Done Right in Coq.pdf:pdf},

512pages = {98----113},

522pages = {98----113},

513title = {{Proving Equalities in a Commutative Ring Done Right in Coq}},

523title = {{Proving Equalities in a Commutative Ring Done Right in Coq}},

514url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.61.3041},

524url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.61.3041},

515year = {2005}

525year = {2005}

516}

526}

517−@misc{Bloat,

527+@book{Cryptography2012,

518−author = {Brooks, Fred},

519−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},

520−isbn = {9780321702081},

521−title = {{The Design of Design Chapter 4}}

522−}

523−@misc{Protocols2012a,

524author = {Anderson, Ross},

528author = {Anderson, Ross},

525−doi = {10.1093/epirev/mxr031},

529+doi = {10.1093/intimm/dxs023},

526−file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Unknown/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},

530+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 5.pdf:pdf},

527isbn = {9780470068526},

531isbn = {9780470068526},

528−issn = {1478-6729},

532+issn = {1460-2377},

529−pmid = {22215642},

533+number = {4},

534+pmid = {22451589},

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

535+title = {{Security Engineering Chapter 5}},

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

537+volume = {24}

531}

538}

539+@article{Brady,

540+author = {Butenhof, David R.},

541+file = {:Users/edwin/Downloads/Safari/ProgrammingwithPOSIXThreadsChapter8Hintstoavoiddebu.pdf:pdf},

542+isbn = {0201633922},

543+title = {{Programming with POSIX Threads Chapter 8}}

544+}

532−@inproceedings{Augustsson1998,

545+@inproceedings{oury2008power,

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

546+author = {Oury, N. and Swierstra, W.},

534−author = {Augustsson, Lennart},

535booktitle = {International Conference on Functional Programming},

547booktitle = {International Conference on Functional Programming},

536−doi = {10.1097/MEG.0b013e328342f213},

548+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

537−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/International Conference on Functional Programming/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

549+keywords = {Dependent Types},

538−issn = {14735687},

550+mendeley-tags = {Dependent Types},

551+number = {9},

552+pages = {39--50},

553+publisher = {ACM},

554+title = {{The power of Pi}},

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

556+volume = {43},

557+year = {2008}

558+}

559+@article{McBride2004a,

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

561+author = {McBride, Conor and McKinna, James},

562+doi = {10.1017/S0956796803004829},

563+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

564+issn = {09567968},

565+journal = {Journal of Functional Programming},

539−keywords = {Depe,Dependent Types},

566+keywords = {Dependent Types},

540−mendeley-tags = {Depe,Dependent Types},

567+mendeley-tags = {Dependent Types},

541number = {1},

568number = {1},

542−pages = {239--250},

569+pages = {69--111},

543−pmid = {21139473},

544−publisher = {ACM Press},

570+publisher = {Cambridge University Press},

545−title = {{Cayenne - a language with dependent types}},

571+title = {{The view from the left}},

546−url = {http://www.cs.chalmers.se/$\sim$augustss/cayenne/paper.ps},

572+url = {http://www.journals.cambridge.org/abstract_S0956796803004829},

547−volume = {23},

573+volume = {14},

548−year = {1998}

574+year = {2004}

549}

575}

550−@book{Hunt,

576+@book{Cryptography2012a,

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

577+author = {Pfleeger, Charles P and Pfleeger, S. L.},

552−booktitle = {Design},

578+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

553−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Design/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},

579+doi = {10.1093/ntr/nts035},

554−isbn = {020161622X},

580+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 2.pdf:pdf},

555−title = {{The Pragmatic Programmer Chapter 4}}

581+isbn = {0132390779},

582+issn = {1469-994X},

583+month = oct,

584+number = {10},

585+pages = {NP},

586+pmid = {23012339},

587+title = {{Security in Computing Chapter 2}},

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

589+volume = {14},

590+year = {2012}

556}

591}

557−@article{burrows1990,

592+@phdthesis{Pretnar2010,

558−author = {Burrows, Michael and Abadi, Martin and Needham, Roger},

593+author = {Pretnar, Matija},

559−file = {:Users/edwin/Documents/Mendeley Desktop/Burrows, Abadi, Needham/ACM Transactions on Computer Systems/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

594+file = {:Users/edwin/Downloads/the-logic-and-handling-of-algebraic-effects.pdf:pdf},

560−journal = {ACM Transactions on Computer Systems},

595+school = {University of Edinburgh},

561−pages = {18----36},

596+title = {{The Logic and Handling of Algebraic Effects}},

562−title = {{A logic of authentication}},

563−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569},

564−volume = {8},

565−year = {1990}

597+year = {2010}

566}

598}

567−@inproceedings{atkey2009unembedding,

599+@inproceedings{Brady2010,

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

600+author = {Brady, Edwin and Hammond, Kevin},

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

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

602+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},

603+isbn = {9781605587943},

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

605+mendeley-tags = {Dependent Types},

570−pages = {37--48},

606+pages = {297--308},

571publisher = {ACM},

607publisher = {ACM},

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

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

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

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

574−year = {2009}

610+year = {2010}

575}

611}

576−@inproceedings{Brady2011a,

612+@misc{Danielsson2002,

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

613+author = {Danielsson, Nils Anders and Altenkirch, Thorsten},

578−author = {Brady, Edwin},

614+file = {:Users/edwin/Downloads/Papers/danielsson-altenkirch-subtyping.pdf:pdf},

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

615+title = {{Subtyping, Declaratively}},

580−doi = {10.1145/1929529.1929536},

581−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},

582−isbn = {9781450304870},

583−keywords = {Dependent Types,data description,dependent types},

584−mendeley-tags = {Dependent Types},

585−month = jan,

586−publisher = {ACM Press},

587−title = {{Idris --- Systems Programming Meets Full Dependent Types}},

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

589−year = {2011}

616+year = {2002}

590}

617}

591−@inproceedings{gibbons2011modularising,

618+@book{Strings2012,

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

619+author = {Sedgewick, Robert and Wayne, Kevin},

593−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Proceedings of the seventh ACM SIGPLAN workshop on Generic programming/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

620+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

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

621+doi = {10.1093/ntr/nts035},

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

622+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sedgewick, Wayne - 2012 - Algorithms Chapter 5.pdf:pdf},

623+isbn = {9780132762571},

624+issn = {1469-994X},

625+month = oct,

626+number = {10},

627+pages = {NP},

628+pmid = {23012339},

629+title = {{Algorithms Chapter 5}},

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

631+volume = {14},

596−year = {2011}

632+year = {2012}

597}

633}

598−@book{An2012,

634+@inproceedings{Augustsson1985,

599−author = {Fowler, Martin},

635+address = {Berlin, Heidelberg},

600−booktitle = {Carcinogenesis},

636+author = {Augustsson, Lennart},

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

638+doi = {10.1007/3-540-15975-4},

639+editor = {Jouannaud, Jean-Pierre},

640+isbn = {978-3-540-15975-9},

641+keywords = {Computer Science},

642+pages = {368----381},

643+publisher = {Springer Berlin Heidelberg},

644+series = {Lecture Notes in Computer Science},

645+title = {{Compiling Pattern Matching}},

646+url = {http://www.springerlink.com/content/y647423656557505/},

647+volume = {201},

648+year = {1985}

649+}

650+@misc{Abel1998,

651+author = {Abel, Andreas},

652+booktitle = {Language},

653+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

654+title = {{foetus - Termination Checker for Simple Functional Programs}},

655+year = {1998}

656+}

657+@article{Silkensen,

658+author = {Silkensen, Erik and Siek, Jeremy},

659+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Silkensen, Siek - Unknown - Well-typed Islands Parse Faster.pdf:pdf},

660+title = {{Well-typed Islands Parse Faster}}

661+}

662+@misc{Svenningsson,

663+author = {Svenningsson, Josef and Axelsson, Emil},

664+booktitle = {Writing},

665+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Svenningsson, Axelsson - Unknown - Combining Deep and Shallow Embedding for EDSL.pdf:pdf},

666+title = {{Combining Deep and Shallow Embedding for EDSL}}

667+}

668+@misc{Bauer,

669+archivePrefix = {arXiv},

670+arxivId = {arXiv:1203.1539v1},

671+author = {Bauer, Andrej and Pretnar, Matija},

672+eprint = {arXiv:1203.1539v1},

673+file = {:Users/edwin/Downloads/1203.1539v1.pdf:pdf},

674+keywords = {()},

675+title = {{Programming with Algebraic Effects and Handlers}}

676+}

677+@misc{Krustev,

678+author = {Krustev, Dimitur},

679+booktitle = {Language},

680+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Krustev - Unknown - Towards a Framework for Building Formally Verified Supercompilers in Coq.pdf:pdf},

681+title = {{Towards a Framework for Building Formally Verified Supercompilers in Coq}}

682+}

683+@book{Graphs2012,

684+author = {Sedgewick, Robert and Wayne, Kevin},

685+booktitle = {The Gerontologist},

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

686+doi = {10.1093/geront/gns026},

602−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Carcinogenesis/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},

687+file = {:Users/edwin/Downloads/Safari/AlgorithmsFourthEditionChapterFourGraphs.pdf:pdf},

603−isbn = {9780132107549},

688+isbn = {9780132762571},

604−issn = {1460-2180},

689+issn = {1758-5341},

690+month = dec,

605−number = {3},

691+number = {6},

606−pmid = {22383472},

692+pages = {NP},

693+pmid = {23150082},

607−title = {{Domain Specific Languages Chapter 1}},

694+title = {{Algorithms Chapter 4}},

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

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

696+volume = {52},

697+year = {2012}

698+}

699+@misc{Brady2012c,

700+author = {Brooks, Fred},

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

702+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},

703+isbn = {9780321702081},

704+issn = {1478-6729},

705+number = {1},

706+pages = {NP},

707+pmid = {22215642},

708+title = {{The Design of Design Chapter 5}},

609−volume = {33}

709+volume = {34}

610}

710}

611@inproceedings{coquand1986analysis,

711@inproceedings{coquand1986analysis,

612author = {Coquand, T.},

712author = {Coquand, T.},

613booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},

713booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},

614−file = {:Users/edwin/Documents/Mendeley Desktop/Coquand/{Proceedings of the First IEEE Symposium on Logic in Computer Science}/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},

714+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},

615pages = {227----246},

715pages = {227----246},

616title = {{An analysis of Girard's paradox}},

716title = {{An analysis of Girard's paradox}},

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

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

618year = {1986}

718year = {1986}

619}

719}

620−@misc{altenkirch2008nσ,

720+@book{Harper2012,

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

721+author = {Harper, Robert},

622−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Oury/Unknown/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},

722+file = {:Users/edwin/Downloads/pfpl.pdf:pdf},

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

723+title = {{Practical Foundations for Programming Languages}},

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

625−year = {2008}

626−}

627−@inproceedings{barras2008implicit,

628−author = {Barras, B. and Bernardo, B.},

629−booktitle = {Foundations of Software Science and Computational Structures},

630−file = {:Users/edwin/Documents/Mendeley Desktop/Barras, Bernardo/Foundations of Software Science and Computational Structures/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},

631−pages = {365--379},

632−publisher = {Springer},

633−title = {{The implicit calculus of constructions as a programming language with dependent types}},

634−url = {http://www.springerlink.com/index/m84h82904546l265.pdf},

635−year = {2008}

636−}

637−@book{While2012,

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

639−booktitle = {Carcinogenesis},

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

641−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},

642−isbn = {020161622X},

643−issn = {1460-2180},

644−number = {3},

645−pmid = {22383472},

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

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

648−volume = {33}

649−}

650−@inproceedings{bradyresource,

651−author = {Brady, Edwin and Hammond, Kevin},

652−booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},

653−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Practical Applications of Declarative Languages ({PADL} 2012)/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},

654−pages = {242----257},

655−title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},

656−url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},

657year = {2012}

724year = {2012}

658}

725}

659−@book{luo1994,

726+@misc{dagand2011transporting,

660−author = {Luo, Z.},

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

661−publisher = {Oxford University Press, Inc.},

728+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

662−title = {{Computation and reasoning: a type theory for computer science}},

729+title = {{Transporting Functions across Ornaments}},

663−url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},

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

664−year = {1994}

731+year = {2011}

665}

732}

666−@phdthesis{norell2007thesis,

733+@article{Abel2010,

667−author = {Norell, Ulf},

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

668−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Unknown/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},

735+author = {Abel, Andreas},

669−keywords = {Dependent Types},

736+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},

670−mendeley-tags = {Dependent Types},

737+journal = {EPTCS},

671−publisher = {Citeseer},

738+pages = {1--15},

672−school = {Chalmers University of Technology},

739+title = {{MiniAgda: Integrating Sized and Dependent Types}},

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

740+url = {http://arxiv.org/abs/1012.4896},

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

741+volume = {43},

675−year = {2007}

742+year = {2010}

676}

743}

677−@inproceedings{Brady2006b,

744+@article{burrows1990,

678−author = {Brady, Edwin},

745+author = {Burrows, Michael and Abadi, Martin and Needham, Roger},

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

746+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

680−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Implementation and Application of Functional Languages ({IFL}'06)/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

747+journal = {ACM Transactions on Computer Systems},

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

682−month = sep,

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

748+pages = {18----36},

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

749+title = {{A logic of authentication}},

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

750+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569},

751+volume = {8},

686−year = {2006}

752+year = {1990}

687}

753}

688−@inproceedings{chlipala2010ur,

754+@article{loh2010tutorial,

689−author = {Chlipala, Adam},

755+author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},

690−booktitle = {ACM SIGPLAN Notices},

756+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},

691−file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/ACM SIGPLAN Notices/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

757+journal = {Fundamenta Informaticae},

692−number = {6},

758+number = {2},

693−pages = {122--133},

759+pages = {177--207},

694−publisher = {ACM},

760+publisher = {IOS Press},

695−title = {{Ur: statically-typed metaprogramming with type-level record computation}},

761+title = {{A tutorial implementation of a dependently typed lambda calculus}},

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

762+url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},

697−volume = {45},

763+volume = {102},

698year = {2010}

764year = {2010}

699}

765}

766+@article{mcbride2008functional,

767+author = {McBride, C. and Paterson, R.},

768+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},

769+journal = {Journal of functional programming},

770+number = {1},

771+pages = {1--13},

772+publisher = {Cambridge Univ Press},

773+title = {{Functional pearl: Applicative programming with effects}},

774+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=1457860},

775+volume = {18},

776+year = {2008}

777+}

778+@techreport{Cardelli1988,

779+author = {Cardelli, L},

780+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Cardelli - 1988 - Phase distinctions in type theory.pdf:pdf},

781+title = {{Phase distinctions in type theory}},

782+year = {1988}

783+}

700@misc{Abadi1997,

784@misc{Abadi1997,

701author = {Abadi, Martin and Gordon, Andrew D},

785author = {Abadi, Martin and Gordon, Andrew D},

702booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},

786booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},

703−file = {:Users/edwin/Documents/Mendeley Desktop/Abadi, Gordon/4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},

787+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},

704pages = {36 -- 47},

788pages = {36 -- 47},

705title = {{A calculus for cryptographic protocols: The spi calculus}},

789title = {{A calculus for cryptographic protocols: The spi calculus}},

706url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},

790url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},

707year = {1997}

791year = {1997}

708}

792}

709−@inproceedings{McBride2006,

793+@article{Haskell2012a,

710−author = {McBride, C and Goguen, H and McKinna, J},

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

711−booktitle = {Types for Proofs and Programs {(TYPES 2006)}},

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

712−title = {{A few constructions on constructors}},

796+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

713−url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},

797+isbn = {9780596801670},

714−year = {2006}

798+issn = {1478-6729},

799+pmid = {22215642},

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

715}

801}

716−@article{Jones2003,

802+@inproceedings{madhavapeddy2010turning,

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

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

718−author = {Jones, Simon Peyton},

804+booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},

719−editor = {Jones, Simon Peyton},

805+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},

720−isbn = {0521826144},

806+publisher = {USENIX Association},

721−journal = {Language},

807+title = {{Turning down the LAMP: software specialisation for the cloud}},

722−number = {1},

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

723−publisher = {Cambridge University Press},

809+year = {2010}

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

810+}

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

811+@misc{Braßel,

726−volume = {13},

812+annote = {New compilation system for Curry, a Haskell like language with equational constraints, making it a functional logic language.

813+

814+

815+What is the contribution of this paper? i.e. what is new about the compiler? Seems to be efficient implementation of equational constraints.

816+

817+

818+Nice introduction to the language, easy for a Haskell programmer to follow, and nice explanation of how it works motivating the problem. But I find it hard to tell what in the paper is already known and what is a specific contribution.

819+

820+

821+Functional patterns look nice, if hard to implement. Related to views? Limitations?

822+Could these techniques improve (compile-time) unification in dependently typed languages?

823+

824+

825+Not many results. Encouraging, but only 7 of various forms isn't conclusive. },

826+author = {Bra\ss el, Bernd and Hanus, Michael and Peem\"{o}ller, Bj\"{o}rn and Reck, Fabian},

827+file = {:Users/edwin/Downloads/Papers/padl2013_submission_17.pdf:pdf},

828+keywords = {func-,functional logic programming,implementation,unification},

829+title = {{Implementing Equational Constraints in a Functional Language}}

830+}

831+@inproceedings{Brady2003,

832+author = {Brady, Edwin and McBride, Conor and McKinna, James},

833+booktitle = {Types for Proofs and Programs {(TYPES 2003)}},

834+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},

835+keywords = {Dependent Types},

836+mendeley-tags = {Dependent Types},

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

727year = {2003}

838year = {2003}

728}

839}

729−@inproceedings{Visser2008,

840+@book{An2012,

730−author = {Visser, E},

841+author = {Fowler, Martin},

731−booktitle = {Generative and Transformational Techniques in Software Engineering},

842+booktitle = {Carcinogenesis},

732−title = {{WebDSL: A case study in domain-specific language engineering}},

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

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

844+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},

845+isbn = {9780132107549},

846+issn = {1460-2180},

847+number = {3},

848+pmid = {22383472},

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

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

851+volume = {33}

852+}

853+@book{Choosing2012,

854+author = {Fowler, Martin},

855+booktitle = {Carcinogenesis},

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

857+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},

858+isbn = {9780132107549},

859+issn = {1460-2180},

860+number = {3},

861+pmid = {22383472},

862+title = {{Domain Specific Languages Chapter 6}},

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

864+volume = {33}

865+}

866+@misc{altenkirch2008nσ,

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

868+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},

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

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

734year = {2008}

871year = {2008}

735}

872}

736−@inproceedings{ko2011modularising,

873+@misc{Silkensen2012,

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

874+annote = {This paper tackles an interesting problem, namely that of building DSLs independently which are nevertheless composable (at least as far as parsing goes). The claim is that the approach taken - using type based disambiguation - can combine the good features of internal and external DSLs - namely, that they become easier to implement, and have a nice syntax.

738−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},

875+

876+

877+I found the paper interesting to read, the contribution worthwhile and the results convincing, though I have a few suggestions for preparing the paper for TFP submission, since it wouldn't be possible to accept it in its current form.

878+

879+

880+Perhaps most importantly, the draft submission is in the SIGPLAN format, which means you've used a lot more space than you have available. I find that 1 SIGPLAN page becomes at least 2 in Springer format because of font size and margins, so you'll need to think carefully about what you consider the most important contribution of the paper, how much detail you can go into, and how many examples to give.

881+If it helps, I think you could reduce section 5 to just a short sketch of Typed Racket and there'd be enough of a contribution to justify a TFP paper (though of course I can't speak for other potential referees!)

882+

883+

884+I found the paper a bit difficult to read at first since I don't have a detailed understand of parsing algorithms, and I suspect I won't be alone in this among the TFP readership. It would be useful to say more in the introduction about island parsing, and what a chart parsing strategy is. An intuitive explanation of the various parsing algorithms you give formally (Example 2.3, say) would be very useful for this (possibly even more useful than the formal descriptions...).

885+

886+

887+Another advantage of internal DSLs that I didn't see mentioned explicitly in the paper is that many features of the host language - syntax, code generation, type checking - are available for free, but have to be implemented explicitly for an external DSL. Maybe this is part of what you mean by interoperability. There is more than parsing needed for this though.

888+

889+

890+A question on contribution 1: how realistic is it to assume that nonterminals are largely disjoint? I could imagine, say, function calls or arithmetic being part of multiple DSLs if not factored out. Or have I misunderstood what you mean?

891+

892+

893+Some modern languages with dependent types have systems for syntax extension, e.g. Agda has mixfix declarations, Idris has syntax rules, type-directed elaboration and overloaded variable bindings. I wonder, therefore, if your approach to parsing could be better integrated into this kind of language, where embedded verifiable DSLs seem to be an obvious application. The Typed Racket example suggests to me that this would be an interesting thing to explore.},

894+author = {Silkensen, Erik and Siek, Jeremy},

895+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Silkensen, Siek - 2012 - Well-typed Islands Parse Faster.pdf:pdf},

739−pages = {13--24},

896+pages = {1--12},

740−publisher = {ACM},

897+title = {{Well-typed Islands Parse Faster}},

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

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

743−year = {2011}

898+year = {2012}

744}

899}

745−@misc{Attacks2012a,

900+@misc{The2012c,

746−author = {Anderson, Ross},

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

747doi = {10.1093/epirev/mxr031},

902doi = {10.1093/epirev/mxr031},

748−file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Unknown/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},

903+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

749−isbn = {9780470068526},

904+isbn = {9780596529833},

750issn = {1478-6729},

905issn = {1478-6729},

751−number = {1},

752−pages = {NP},

753pmid = {22215642},

906pmid = {22215642},

754−title = {{Security Engineering Chapter 18}},

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

908+}

909+@misc{idristutorial,

910+author = {Brady, Edwin},

911+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},

912+title = {{Programming in Idris : a tutorial}},

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

914+year = {2012}

915+}

916+@book{Simon2012,

917+author = {Seibel, Peter},

918+booktitle = {The Gerontologist},

919+doi = {10.1093/geront/gns026},

920+file = {:Users/edwin/Downloads/Safari/CodersatWorkReflectionsontheCraftofProgrammingChapter7SimonPeytonJones.pdf:pdf},

921+isbn = {9781430219484},

922+issn = {1758-5341},

923+month = dec,

924+number = {6},

925+pages = {NP},

926+pmid = {23150082},

927+title = {{Coders at Work Chapter 7}},

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

755−volume = {34}

929+volume = {52},

930+year = {2012}

931+}

932+@misc{TheMendeleySupportTeam2011,

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

934+address = {London},

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

936+booktitle = {Mendeley Desktop},

937+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

938+keywords = {Mendeley,how-to,user manual},

939+pages = {1--16},

940+publisher = {Mendeley Ltd.},

941+title = {{Getting Started with Mendeley}},

942+url = {http://www.mendeley.com},

943+year = {2011}

944+}

945+@book{Brady2012d,

946+author = {Seibel, Peter},

947+booktitle = {The Gerontologist},

948+doi = {10.1093/geront/gns026},

949+file = {:Users/edwin/Downloads/Safari/CodersatWorkReflectionsontheCraftofProgrammingChapter6JoeArmstrong.pdf:pdf},

950+isbn = {9781430219484},

951+issn = {1758-5341},

952+month = dec,

953+number = {6},

954+pages = {NP},

955+pmid = {23150082},

956+title = {{Coders at Work Chapter 6}},

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

958+volume = {52},

959+year = {2012}

756}

960}

757@inproceedings{l,

961@inproceedings{l,

758author = {L\"{a}mmel, R. and Jones, S.P.},

962author = {L\"{a}mmel, R. and Jones, S.P.},

759booktitle = {ACM SIGPLAN Notices},

963booktitle = {ACM SIGPLAN Notices},

760−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{a}mmel, Jones/ACM SIGPLAN Notices/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},

964+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},

761number = {3},

965number = {3},

762pages = {26--37},

966pages = {26--37},

763publisher = {ACM},

967publisher = {ACM},

@@ -766,213 +970,303 @@ url = {http://dl.acm.org/citation.cfm?id=640136.604179},

766volume = {38},

970volume = {38},

767year = {2003}

971year = {2003}

768}

972}

769−@inproceedings{Delahaye2000,

973+@phdthesis{Okasaki1996,

770−author = {Delahaye, D},

974+author = {Okasaki, Chris},

771−booktitle = {Logic for Programming and Automated Reasoning},

975+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},

772−file = {:Users/edwin/Documents/Mendeley Desktop/Delahaye/Logic for Programming and Automated Reasoning/Delahaye - 2000 - A tactic language for the system Coq.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Delahaye/Logic for Programming and Automated Reasoning/Delahaye - 2000 - A tactic language for the system Coq(2).pdf:pdf},

976+school = {Carnegie Mellon University},

773−pages = {85----95},

977+title = {{Purely Functional Data Structures}},

774−publisher = {Springer},

775−title = {{A tactic language for the system Coq}},

776−url = {http://www.springerlink.com/index/EFQAH8J88K42VN8T.pdf},

777−year = {2000}

978+year = {1996}

778}

979}

779−@misc{pollack1997believe,

980+@inproceedings{McBride2004b,

780−author = {Pollack, R.},

981+author = {McBride, Conor and McKinna, James},

781−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Unknown/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},

982+booktitle = {Haskell Workshop},

782−title = {{How to believe a machine-checked proof}},

983+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},

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

984+title = {{I am not a number : I am a free variable}},

784−year = {1997}

985+year = {2004}

785}

986}

786−@book{Bertot2004,

987+@inproceedings{Brady2005a,

787−author = {Bertot, Yves and Cast\'{e}ran, Pierre},

988+author = {Brady, E and Hammond, K},

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

990+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},

991+keywords = {Dependent Types},

992+mendeley-tags = {Dependent Types},

993+title = {{A dependently typed framework for static analysis of program execution costs}},

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

995+year = {2005}

996+}

997+@misc{TMR13,

998+author = {Eidhof, Chris and Elkins, Derek and Hicks, Stephen},

999+file = {:Users/edwin/Downloads/Papers/TMR-Issue13.pdf:pdf},

1000+number = {13},

1001+title = {{The Monad . Reader Issue 13}},

1002+year = {2009}

1003+}

1004+@inproceedings{taha2004gentle,

1005+author = {Taha, W.},

1006+booktitle = {Domain-Specific Program Generation},

1007+pages = {30--50},

788publisher = {Springer},

1008publisher = {Springer},

789−title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},

1009+title = {{A gentle introduction to multi-stage programming}},

790−url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},

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

791year = {2004}

1011year = {2004}

792}

1012}

793−@inproceedings{brady2011epic,

1013+@article{Rose,

1014+annote = {This paper describes a language, Jeeves, for describing privacy policies and ensuring that they are automatically enforced. It gives the semantics of Jeeves in terms of a translation to a target language $\lambda_J$ and shows how to implement the privacy rules in a monadic style in Haskell which captures the constraint propagation.

1015+

1016+

1017+Capturing policy rules in this way is an interesting idea and the monadic definition of constraint propagation is natural, but unfortunately the paper itself only seems half-written. I found the website (https://sites.google.com/site/jeevesprogramming/) and the tutorial there much more enlightening! Perhaps relating the implementation to some more extensive examples would be helpful, illustrating how the Haskell code relates to Jeeves programs. This would be particularly valuable in sections 3 and 5, and there is plenty of space available for this.

1018+

1019+

1020+The paper could use a thorough proof read and spell check. For example:

1021+

1022+

1023+end of sec 1 - references for the report and web site would be useful here.

1024+End of sec 2: privacy politics? This is the only place this phrase is used.

1025+

1026+

1027+p2 etal => et al

1028+

1029+

1030+"The program read" => "The program reads"

1031+"Depending on what" => comma before this

1032+"bottem" => "bottom"

1033+

1034+

1035+p4 "Eventhough" => "Even though"

1036+"The program body, consist" => "The program body consists"

1037+

1038+

1039+"but without any substantial..." - there is a missing word here

1040+

1041+

1042+The presentation of Sec 5 is untidy - for example a section heading at the end of the page and bad spacing between subsections.

1043+

1044+

1045+Reference 1 is blank

1046+

1047+

1048+

1049+ },

794−author = {Brady, Edwin},

1050+author = {Rose, Eva},

795−booktitle = {Trends in Functional Programming ({TFP}’11)},

1051+file = {:Users/edwin/Downloads/Papers/padl2013_submission_33.pdf:pdf},

796−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Trends in Functional Programming ({TFP}’11)/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},

1052+keywords = {constraints,language design,mon-,privacy policy,semantics},

797−title = {{Epic --- A Library for Generating Compilers}},

1053+title = {{Declarative implementation aspects of privacy policy effects}}

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

799−year = {2011}

800}

1054}

801−@article{dybjer1994inductive,

1055+@inproceedings{morris2006exploring,

802−author = {Dybjer, P.},

1056+author = {Morris, P. and Altenkirch, T. and McBride, C.},

803−journal = {Formal aspects of computing},

1057+booktitle = {Types for Proofs and Programs},

804−number = {4},

1058+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

805−pages = {440--465},

1059+pages = {252--267},

806publisher = {Springer},

1060publisher = {Springer},

807−title = {{Inductive families}},

1061+title = {{Exploring the regular tree types}},

808−url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},

1062+url = {http://www.springerlink.com/index/f9p1317716614834.pdf},

1063+year = {2006}

1064+}

1065+@inproceedings{pj2006gadts,

1066+author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},

1067+booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},

1068+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},

1069+number = {9},

1070+pages = {50--61},

1071+publisher = {ACM},

1072+title = {{Simple unification-based type inference for GADTs}},

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

809−volume = {6},

1074+volume = {41},

1075+year = {2006}

1076+}

1077+@book{luo1994,

1078+author = {Luo, Z.},

1079+publisher = {Oxford University Press, Inc.},

1080+title = {{Computation and reasoning: a type theory for computer science}},

1081+url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},

810year = {1994}

1082year = {1994}

811}

1083}

812−@inproceedings{McBride2004b,

1084+@misc{Hancock,

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

1085+author = {Hancock, Peter and Setzer, Anton},

814−booktitle = {Haskell Workshop},

1086+file = {:Users/edwin/Downloads/10.1.1.25.9367.pdf:pdf},

815−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/Haskell Workshop/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},

1087+keywords = {dependent types,functional programming,interac-,monadic i,o,reactive programming,refinement,repetition constructs,tion},

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

1088+title = {{Interactive Programs in Dependent Type Theory}},

817−year = {2004}

1089+year = {2000}

818}

1090}

819−@article{Wadler2001,

1091+@book{Chlipala2012,

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

1092+author = {Chlipala, Adam},

821−author = {Wadler, Philip},

1093+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chlipala - 2012 - Certified Programming with Dependent Types.pdf:pdf},

822−doi = {10.1007/3-540-59451-5_2},

1094+title = {{Certified Programming with Dependent Types}},

823−editor = {Jeuring, Johan and Meijer, Erik},

824−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Advanced Functional Programming/Wadler - 2001 - Monads for functional programming.pdf:pdf},

825−isbn = {3540594515},

826−issn = {03029743},

827−journal = {Advanced Functional Programming},

828−number = {August 1992},

829−pages = {24--52},

830−publisher = {Springer},

831−series = {Lecture Notes in Computer Science},

832−title = {{Monads for functional programming}},

833−url = {http://www.springerlink.com/index/715264614rh13340.pdf},

834−volume = {925},

835−year = {2001}

1095+year = {2012}

836}

1096}

837−@inproceedings{taha1997multi,

1097+@article{Mandelbaum2007,

838−author = {Taha, W. and Sheard, T.},

1098+abstract = {Massive amounts of useful data are stored and processed in ad hoc formats for which common tools like parsers, printers, query engines and format converters are not readily available. In this paper, we explain the design and implementation of PADS/ML , a new language and system that facilitates the generation of data processing tools for ad hoc formats. The PADS/ML design includes features such as dependent, polymorphic and recursive datatypes, which allow programmers to describe the syntax and semantics of ad hoc data in a concise, easy-to-read notation. The PADS/ML implementation compiles these descriptions into ml structures and functors that include types for parsed data, functions for parsing and printing, and auxiliary support for user-specified, format-dependent and format-independent tool generation.},

839−booktitle = {ACM SIGPLAN Notices},

1099+author = {Mandelbaum, Yitzhak and Fisher, Kathleen and Walker, David and Fernandez, Mary and Gleyzer, Artem},

1100+doi = {10.1145/1190215.1190231},

1101+isbn = {1595935754},

1102+issn = {03621340},

1103+journal = {SIGPLAN Not},

840−number = {12},

1104+number = {1},

841−pages = {203--217},

1105+pages = {77--83},

842publisher = {ACM},

1106publisher = {ACM},

843−title = {{Multi-stage programming with explicit annotations}},

1107+series = {POPL '07},

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

1108+title = {{PADS/ML: a functional data description language}},

1109+url = {http://doi.acm.org/10.1145/1190216.1190231},

845−volume = {32},

1110+volume = {42},

846−year = {1997}

1111+year = {2007}

847}

1112}

848−@article{loh2010tutorial,

1113+@article{Nabais2008,

849−author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},

1114+author = {Nabais, Davide},

850−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{o}h, McBride, Swierstra/Fundamenta Informaticae/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},

1115+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Nabais - 2008 - DesCo a Web Based Information System for Descriptional Complexity of Formal Languages.pdf:pdf},

851−journal = {Fundamenta Informaticae},

1116+journal = {Most},

852−number = {2},

853−pages = {177--207},

1117+pages = {1--5},

854−publisher = {IOS Press},

1118+title = {{DesCo : a Web Based Information System for Descriptional Complexity of Formal Languages}},

855−title = {{A tutorial implementation of a dependently typed lambda calculus}},

856−url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},

857−volume = {102},

858−year = {2010}

1119+year = {2008}

859}

1120}

860−@book{Philosophy2012,

1121+@book{Edition2012,

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

1122+author = {Pfleeger, Charles P and Pfleeger, S. L.},

862−booktitle = {Carcinogenesis},

1123+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

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

1124+doi = {10.1093/ntr/nts035},

864−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},

1125+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 1.pdf:pdf},

865−isbn = {020161622X},

1126+isbn = {0132390779},

866−issn = {1460-2180},

1127+issn = {1469-994X},

1128+month = oct,

867−number = {3},

1129+number = {10},

868−pmid = {22383472},

1130+pages = {NP},

869−title = {{The Pragmatic Programmer Chapter 1}},

1131+pmid = {23012339},

1132+title = {{Security in Computing Chapter 1}},

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

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

871−volume = {33}

1134+volume = {14},

1135+year = {2012}

872}

1136}

873−@inproceedings{pollack1990implicit,

1137+@book{Eap,

874−author = {Pollack, R.},

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

875−booktitle = {{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}},

1139+file = {:Users/edwin/Downloads/Safari/TCPIPIllustratedVolume1TheProtocolsSecondEditionChapter18SecurityEAPIPs.pdf:pdf},

876−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}/Pollack - 1990 - Implicit syntax.pdf:pdf},

1140+isbn = {9780132808200},

877−publisher = {Citeseer},

1141+title = {{TCP/IP Illustrated Chapter 18}}

878−title = {{Implicit syntax}},

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

880−year = {1990}

881}

1142}

882−@article{gordon2003authenticity,

1143+@book{Fowler,

883−author = {Gordon, A.D. and Jeffrey, A.},

1144+author = {Fowler, Martin},

884−file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Journal of computer security/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

1145+booktitle = {Language},

885−journal = {Journal of computer security},

1146+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},

886−number = {4},

1147+isbn = {9780132107549},

887−pages = {451--520},

1148+title = {{Domain Specific Languages Chapter 2}}

888−publisher = {IOS Press},

889−title = {{Authenticity by typing for security protocols}},

890−url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},

891−volume = {11},

892−year = {2003}

893}

1149}

894−@inproceedings{Wadler1989,

1150+@book{Brady2012e,

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

1151+author = {Seibel, Peter},

896−author = {Wadler, Philip},

1152+booktitle = {The Gerontologist},

897−booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},

1153+doi = {10.1093/geront/gns026},

898−doi = {10.1145/99370.99404},

1154+file = {:Users/edwin/Downloads/Safari/CodersatWorkReflectionsontheCraftofProgrammingChapter9GuySteele.pdf:pdf},

899−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Proceedings of the fourth international conference on Functional programming languages and computer architecture/Wadler - 1989 - Theorems for free!.pdf:pdf},

1155+isbn = {9781430219484},

900−isbn = {0897913280},

1156+issn = {1758-5341},

1157+month = dec,

901−number = {June},

1158+number = {6},

902−pages = {347--359},

1159+pages = {NP},

903−publisher = {ACM},

1160+pmid = {23150082},

904−series = {FPCA '89},

1161+title = {{Coders at Work Chapter 9}},

905−title = {{Theorems for free!}},

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

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

1163+volume = {52},

907−year = {1989}

1164+year = {2012}

908}

1165}

909−@inproceedings{Augustsson1985,

1166+@article{Regular2012,

910−address = {Berlin, Heidelberg},

1167+author = {Kernighan, Brian},

911−author = {Augustsson, Lennart},

1168+doi = {10.1093/geront/gns026},

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

1169+file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter1ARegularExpressio.pdf:pdf},

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

1170+isbn = {9780596510046},

914−editor = {Jouannaud, Jean-Pierre},

1171+issn = {1758-5341},

915−isbn = {978-3-540-15975-9},

1172+month = dec,

916−keywords = {Computer Science},

1173+number = {6},

917−pages = {368----381},

1174+pages = {NP},

918−publisher = {Springer Berlin Heidelberg},

1175+pmid = {23150082},

919−series = {Lecture Notes in Computer Science},

1176+title = {{Beautiful Code Chapter 1}},

920−title = {{Compiling Pattern Matching}},

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

921−url = {http://www.springerlink.com/content/y647423656557505/},

922−volume = {201},

1178+volume = {52},

923−year = {1985}

1179+year = {2012}

924}

1180}

925−@inproceedings{Brady2005a,

1181+@inproceedings{norell2009dependently,

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

1182+author = {Norell, Ulf},

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

1183+booktitle = {Advanced Functional Programming},

928−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Implementation and Application of Functional \ldots/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},

1184+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

929keywords = {Dependent Types},

1185keywords = {Dependent Types},

930mendeley-tags = {Dependent Types},

1186mendeley-tags = {Dependent Types},

931−title = {{A dependently typed framework for static analysis of program execution costs}},

1187+pages = {230--266},

1188+publisher = {Springer},

1189+title = {{Dependently typed programming in Agda}},

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

1190+url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

933−year = {2005}

1191+year = {2009}

934}

1192}

935−@article{Vytiniotis2011,

1193+@misc{Interface2012a,

1194+author = {Kreibich, Jay A.},

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

1196+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

1197+isbn = {9781449394592},

1198+issn = {1478-6729},

1199+pmid = {22215642},

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

1201+}

1202+@inproceedings{Augustsson1998,

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

1204+author = {Augustsson, Lennart},

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

1206+doi = {10.1097/MEG.0b013e328342f213},

1207+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

1208+issn = {14735687},

1209+keywords = {Depe,Dependent Types},

1210+mendeley-tags = {Depe,Dependent Types},

1211+number = {1},

1212+pages = {239--250},

1213+pmid = {21139473},

1214+publisher = {ACM Press},

1215+title = {{Cayenne - a language with dependent types}},

1216+url = {http://www.cs.chalmers.se/$\sim$augustss/cayenne/paper.ps},

1217+volume = {23},

1218+year = {1998}

1219+}

1220+@article{OutsideIn,

936−author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},

1221+author = {Vytiniotis, D and {Peyton Jones}, Simon and Shrijvers, Tom and Sulzmann, Martin},

937−file = {:Users/edwin/Documents/Mendeley Desktop/Vytiniotis et al/{Journal of Functional Programming}/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions(2).pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Vytiniotis et al/{Journal of Functional Programming}/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions.pdf:pdf},

1222+file = {:Users/edwin/Downloads/jfp-outsidein.pdf:pdf},

938−journal = {{Journal of Functional Programming}},

1223+journal = {Journal of Functional Programming},

939number = {4--5},

1224number = {4--5},

940pages = {333----412},

1225pages = {333----412},

941−title = {{\textsc{OutsideIn}(X) Modular type inference with local assumptions}},

1226+title = {{OutsideIn (X) Modular type inference with local assumptions}},

942−url = {http://journals.cambridge.org/abstract_S0956796811000098},

1227+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},

943volume = {21},

1228volume = {21},

944year = {2011}

1229year = {2011}

945}

1230}

946−@article{mccann2000packet,

1231+@inproceedings{fisher2005pads,

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

1232+author = {Fisher, K. and Gruber, R.},

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

1233+booktitle = {ACM SIGPLAN Notices},

949−number = {4},

1234+number = {6},

950−pages = {321--333},

1235+pages = {295--304},

951publisher = {ACM},

1236publisher = {ACM},

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

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

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

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

954−volume = {30},

1239+volume = {40},

955−year = {2000}

956−}

957−@article{Miller1992,

958−author = {Miller, Dale},

959−file = {:Users/edwin/Documents/Mendeley Desktop/Miller/Journal of Symbolic Computation/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},

960−journal = {Journal of Symbolic Computation},

961−title = {{Unification under a mixed prefix}},

962−url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},

963−year = {1992}

1240+year = {2005}

964}

1241}

965−@inproceedings{norell2009dependently,

1242+@inproceedings{Levitation2010,

966−author = {Norell, Ulf},

1243+author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

967−booktitle = {Advanced Functional Programming},

1244+booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},

968−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Advanced Functional Programming/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

1245+doi = {10.1145/1932681.1863547},

1246+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},

1247+isbn = {978-1-60558-794-3},

1248+issn = {03621340},

969−keywords = {Dependent Types},

1249+keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

970mendeley-tags = {Dependent Types},

1250mendeley-tags = {Dependent Types},

971−pages = {230--266},

1251+month = sep,

972−publisher = {Springer},

1252+number = {9},

973−title = {{Dependently typed programming in Agda}},

1253+title = {{The gentle art of levitation}},

974−url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

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

975−year = {2009}

1255+volume = {45},

1256+year = {2010}

1257+}

1258+@book{While2012,

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

1260+booktitle = {Carcinogenesis},

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

1262+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},

1263+isbn = {020161622X},

1264+issn = {1460-2180},

1265+number = {3},

1266+pmid = {22383472},

1267+title = {{The Pragmatic Programmer Chapter 6}},

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

1269+volume = {33}

976}

1270}

977@article{Hughes1989,

1271@article{Hughes1989,

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

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

@@ -980,7 +1274,7 @@ author = {Hughes, J},

980chapter = {2},

1274chapter = {2},

981doi = {10.1093/comjnl/32.2.98},

1275doi = {10.1093/comjnl/32.2.98},

982editor = {Turner, David A},

1276editor = {Turner, David A},

983−file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/The Computer Journal/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},

1277+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},

984institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},

1278institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},

985isbn = {0201172364},

1279isbn = {0201172364},

986issn = {00104620},

1280issn = {00104620},

@@ -993,57 +1287,393 @@ url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},

993volume = {32},

1287volume = {32},

994year = {1989}

1288year = {1989}

995}

1289}

996−@article{Steiner1988,

1290+@article{Brady2006a,

997−author = {Steiner, JG},

1291+author = {Brady, E and Hammond, K},

998−file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Proc. Winter USENIX Conference/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

1292+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

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

1293+journal = {\ldots of the 5th international conference on \ldots},

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

1294+keywords = {Dependent Types},

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

1295+mendeley-tags = {Dependent Types},

1296+title = {{A verified staged interpreter is a verified compiler}},

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

1002−year = {1988}

1298+year = {2006}

1003}

1299}

1004−@phdthesis{McBride1999,

1300+@article{Xi1998,

1005−author = {McBride, Conor},

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

1006−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Unknown/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

1302+author = {Xi, Hongwei and Pfenning, Frank},

1303+doi = {10.1145/277652.277732},

1304+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},

1305+isbn = {0897919874},

1306+issn = {03621340},

1307+journal = {ACM Sigplan Notices},

1007keywords = {Dependent Types},

1308keywords = {Dependent Types},

1008mendeley-tags = {Dependent Types},

1309mendeley-tags = {Dependent Types},

1009−school = {University of Edinburgh},

1310+number = {5},

1010−title = {{Dependently typed functional programs and their proofs}},

1311+pages = {249--257},

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

1312+publisher = {ACM},

1313+series = {PLDI '98},

1314+title = {{Eliminating array bound checking through dependent types}},

1315+url = {http://portal.acm.org/citation.cfm?doid=277652.277732},

1316+volume = {33},

1012−year = {1999}

1317+year = {1998}

1013}

1318}

1014−@inproceedings{augustsson1999exercise,

1319+@inproceedings{Abel2013,

1015−author = {Augustsson, L. and Carlsson, M.},

1320+author = {Abel, Andreas and Pientka, Brigitte and Thibodeau, David and Setzer, Anton},

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

1321+booktitle = {Principles of Programming Languages},

1017−keywords = {Depe},

1322+file = {:Users/edwin/Downloads/popl13.pdf:pdf},

1018−mendeley-tags = {Depe},

1323+isbn = {9781450318327},

1019−publisher = {Citeseer},

1324+keywords = {2008,by the graduiertenkol-,coinduction,elimination,functional programming,introduction,leg programm und modellanalyse,message passing,of the deutsche,pattern matching,puma,thibodeau acknowledges financial support,vs},

1020−title = {{An exercise in dependent types: A well-typed interpreter}},

1325+title = {{Copatterns: Programming Infinite Structures by Observations}},

1021−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2895},

1022−year = {1999}

1326+year = {2013}

1023}

1327}

1024−@inproceedings{taha2004gentle,

1328+@misc{pollack1997believe,

1025−author = {Taha, W.},

1329+author = {Pollack, R.},

1026−booktitle = {Domain-Specific Program Generation},

1330+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},

1331+title = {{How to believe a machine-checked proof}},

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

1333+year = {1997}

1334+}

1335+@book{Searching2012,

1336+author = {Sedgewick, Robert and Wayne, Kevin},

1337+booktitle = {The Gerontologist},

1338+doi = {10.1093/geront/gns026},

1339+file = {:Users/edwin/Downloads/Safari/AlgorithmsFourthEditionChapterThreeSearching.pdf:pdf},

1340+isbn = {9780132762571},

1341+issn = {1758-5341},

1342+month = dec,

1343+number = {6},

1027−pages = {30--50},

1344+pages = {NP},

1028−publisher = {Springer},

1345+pmid = {23150082},

1029−title = {{A gentle introduction to multi-stage programming}},

1346+title = {{Algorithms Chapter 3}},

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

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

1348+volume = {52},

1349+year = {2012}

1350+}

1351+@book{Philosophy2012,

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

1353+booktitle = {Carcinogenesis},

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

1355+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},

1356+isbn = {020161622X},

1357+issn = {1460-2180},

1358+number = {3},

1359+pmid = {22383472},

1360+title = {{The Pragmatic Programmer Chapter 1}},

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

1362+volume = {33}

1363+}

1364+@article{Servers,

1365+author = {Totty, Brian and Gourley, David},

1366+file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter5WebServers.pdf:pdf},

1367+isbn = {1565925092},

1368+title = {{HTTP: The Definitive Guide Chapter 5}}

1369+}

1370+@article{Bird2012a,

1371+annote = {This new version of the paper is, I think, very clear and an entertaining read. It presents a neat example of program calculation and reasoning with each step in the calculation explained precisely - indeed the interesting thing to me is the calculation, rather than the problem itself, and it is nice that this works for an algorithm which requires in-place update (even if it does involve pretending // is in-place!).

1372+

1373+

1374+I'm not totally convinced about the condition of the algorithm being "discovered in a disciplined manner" since many of the steps in the calculation required some insight, but others will disagree and I don't think it really matters for the main point of this paper in any case - the point is the calculational development, which is sufficiently detailed that a careful reader should be able to develop that insight, with practice. I would recommend this paper for acceptance in its current form. },

1375+author = {Bird, Richard S},

1376+file = {:Users/edwin/Downloads/Papers/s1-ln13057035-302779530-1939656818Hwf-543670216IdV208531454713057035PDF_HI0001.pdf:pdf},

1377+keywords = {a href,journal of functional programming},

1378+title = {{An in-situ algorithm for expanding a graph}},

1031−year = {2004}

1379+year = {2012}

1032}

1380}

1033@inproceedings{Sculthorpe2009,

1381@inproceedings{Sculthorpe2009,

1034author = {Sculthorpe, Neil and Nilsson, Henrik},

1382author = {Sculthorpe, Neil and Nilsson, Henrik},

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

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

1036−file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/International Conference on Functional Programming ({ICFP} '09)/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/International Conference on Functional Programming ({ICFP} '09)/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},

1384+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},

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

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

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

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

1039year = {2009}

1387year = {2009}

1040}

1388}

1389+@article{landin1966next,

1390+author = {Landin, P.J.},

1391+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Landin - 1966 - The next 700 programming languages.pdf:pdf},

1392+journal = {Communications of the ACM},

1393+number = {3},

1394+pages = {157--166},

1395+publisher = {ACM},

1396+title = {{The next 700 programming languages}},

1397+url = {http://dl.acm.org/citation.cfm?id=365257 )},

1398+volume = {9},

1399+year = {1966}

1400+}

1401+@inproceedings{Delahaye2000,

1402+author = {Delahaye, D},

1403+booktitle = {Logic for Programming and Automated Reasoning},

1404+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Delahaye - 2000 - A tactic language for the system Coq.pdf:pdf;:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Delahaye - 2000 - A tactic language for the system Coq(2).pdf:pdf},

1405+pages = {85----95},

1406+publisher = {Springer},

1407+title = {{A tactic language for the system Coq}},

1408+url = {http://www.springerlink.com/index/EFQAH8J88K42VN8T.pdf},

1409+year = {2000}

1410+}

1411+@book{Messages,

1412+author = {Totty, Brian and Gourley, David},

1413+file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter3HTTPMessages.pdf:pdf},

1414+isbn = {1565925092},

1415+title = {{HTTP: The Definitive Guide Chapter 3}}

1416+}

1417+@article{Asperti,

1418+author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

1419+doi = {10.2168/LMCS-},

1420+file = {:Users/edwin/Downloads/lmcs_types_2010.pdf:pdf},

1421+journal = {Logical Methods in Computer Science},

1422+keywords = {and phrases,calculus of inductive construc-,interactive theorem prover,refiner,type inference},

1423+pages = {1----49},

1424+title = {{A bi-directional refinement algorithm for the calculus of (co)inductive constructions}},

1425+volume = {8},

1426+year = {2012}

1427+}

1428+@inproceedings{Altenkirch2010,

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

1430+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},

1431+booktitle = {{FLOPS 2010}},

1432+doi = {10.1007/978-3-642-12251-4_5},

1433+editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},

1434+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},

1435+isbn = {9783642122507},

1436+pages = {40----55},

1437+publisher = {Springer Berlin Heidelberg},

1438+series = {Lecture Notes in Computer Science},

1439+title = {{Dependent Types without the Sugar}},

1440+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},

1441+year = {2010}

1442+}

1443+@misc{Gobi2010,

1444+author = {Gobi, Attila and Shkaravska, Olha and {Van Eekelen}, Marko},

1445+booktitle = {Syntax},

1446+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Gobi, Shkaravska, Van Eekelen - 2010 - Higher-Order Size Checking Without Subtyping.pdf:pdf},

1447+number = {100039},

1448+title = {{Higher-Order Size Checking Without Subtyping}},

1449+year = {2010}

1450+}

1451+@book{Context2012,

1452+author = {Sedgewick, Robert and Wayne, Kevin},

1453+booktitle = {The Gerontologist},

1454+doi = {10.1093/geront/gns026},

1455+file = {:Users/edwin/Downloads/Safari/AlgorithmsFourthEditionChapterSixContext.pdf:pdf},

1456+isbn = {9780132762571},

1457+issn = {1758-5341},

1458+month = dec,

1459+number = {6},

1460+pages = {NP},

1461+pmid = {23150082},

1462+title = {{Algorithms Chapter 6}},

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

1464+volume = {52},

1465+year = {2012}

1466+}

1467+@misc{Protocols2012a,

1468+author = {Anderson, Ross},

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

1470+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},

1471+isbn = {9780470068526},

1472+issn = {1478-6729},

1473+pmid = {22215642},

1474+title = {{Security Engineering Chapter 3}}

1475+}

1476+@inproceedings{Visser2008,

1477+author = {Visser, E},

1478+booktitle = {Generative and Transformational Techniques in Software Engineering},

1479+title = {{WebDSL: A case study in domain-specific language engineering}},

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

1481+year = {2008}

1482+}

1483+@inproceedings{gibbons2011modularising,

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

1485+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

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

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

1488+year = {2011}

1489+}

1490+@book{Synchronization2012,

1491+author = {Butenhof, David R.},

1492+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

1493+doi = {10.1093/ntr/nts035},

1494+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Butenhof - Unknown - Programming with POSIX Threads Chapter 3.pdf:pdf},

1495+isbn = {0201633922},

1496+issn = {1469-994X},

1497+number = {10},

1498+pmid = {23012339},

1499+title = {{Programming with POSIX Threads Chapter 3}},

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

1501+volume = {14}

1502+}

1503+@article{Pl,

1504+annote = {-2, 3

1505+

1506+

1507+This paper gives a type inference algorithm for Java extended with lambdas, extending earlier work on type inference for a small functional language with subtyping. It is interesting to see how this could work, and I'm sure this would be a welcome addition to Java. However, I didn't find the paper very well organised or presented so it was difficult to get very much from it. There is too much unnecessary detail (such as fragments of the parser or complete sets of coercions and substitutions) and not enough useful context such as syntax of Java_lambda with its typing rules.

1508+

1509+

1510+If there is an implementation, it would also be good to give a url to download it so that the reader can try out some of the ideas given in the paper, and try to reproduce your results!

1511+

1512+

1513+Other comments:

1514+

1515+

1516+p1 The opening sentences don't seem to make sense on their own. It would be useful to know what your language in [7] is.

1517+

1518+

1519+There are several typos which suggest that the paper could use a proof read and spell check. For example:

1520+p2 "The improvement is that, that" => remove a "that"

1521+"not necessary" => "not necessarily"

1522+"can also consists" => "can also consist"

1523+"remainig" => "remaining"

1524+

1525+

1526+p3 What does "The concrete syntax [...] is oriented at [3]" mean? Is the syntax defined in this reference? It would be better to give it explicitly to make the paper more self contained.

1527+

1528+

1529+p4 Is there some reason that you use tuples in the representation of classes, functions and expressions?

1530+

1531+

1532+p9 "Decomposition: ..." I don't understand this sentence.

1533+

1534+

1535+p10 "corecions" => "coercions" (several times)

1536+also "coersions" => "coercions"

1537+

1538+

1539+p14 (and other places similarly) I don't think it helps much to give the full set of substitutions here. A representative selection at most should be fine.

1540+

1541+

1542+

1543+ },

1544+author = {Pl\"{u}micke, Martin},

1545+file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_13.pdf:pdf},

1546+title = {{Functional implementation of well-typings in}}

1547+}

1548+@article{gordon2003authenticity,

1549+author = {Gordon, A.D. and Jeffrey, A.},

1550+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

1551+journal = {Journal of computer security},

1552+number = {4},

1553+pages = {451--520},

1554+publisher = {IOS Press},

1555+title = {{Authenticity by typing for security protocols}},

1556+url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},

1557+volume = {11},

1558+year = {2003}

1559+}

1560+@book{Approach2012,

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

1562+booktitle = {Carcinogenesis},

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

1564+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},

1565+isbn = {020161622X},

1566+issn = {1460-2180},

1567+number = {3},

1568+pmid = {22383472},

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

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

1571+volume = {33}

1572+}

1573+@inproceedings{barras2008implicit,

1574+author = {Barras, B. and Bernardo, B.},

1575+booktitle = {Foundations of Software Science and Computational Structures},

1576+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},

1577+pages = {365--379},

1578+publisher = {Springer},

1579+title = {{The implicit calculus of constructions as a programming language with dependent types}},

1580+url = {http://www.springerlink.com/index/m84h82904546l265.pdf},

1581+year = {2008}

1582+}

1583+@article{Zanasi,

1584+author = {Zanasi, Fabio},

1585+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Zanasi - Unknown - On the Expressive Power of MSO and WMSO on Trees of Arbitrary Degree ( Extended abstract ).pdf:pdf},

1586+pages = {1--6},

1587+title = {{On the Expressive Power of MSO and WMSO on Trees of Arbitrary Degree ( Extended abstract )}}

1588+}

1589+@article{Thiemann,

1590+annote = {1, 4

1591+

1592+

1593+This paper is a case study in dependently typed programming, investigating how an existing Haskell library (Accelerate) could benefit from dependent types by implementing a version of the library in Agda. The Haskell version is a generative library, meaning that programs are constructed as Haskell ADTs, then compiled to code which will run on a GPU. The authos observe that type correctness of Accelerate programs is checked statically, as far as possible, by using advanced features of the Haskell type system such as GADTs, and hypothesise that a language with a stronger type system such as Agda would increase the static guarantees which are expressible.

1594+

1595+

1596+This is an interesting question, well worth asking, and the paper presents mixed results. The presentation of the Agda version is clear, and the relationship with the Haskell version is easy to see. However, some properties which one might hope to express turn out to be difficult in the current form. One conclusion I would draw from this is that to use dependent types well involves more than simply annotating an existing program. The difficulties with filter and fold in particular show that care must be taken to preserve information required for checking later.

1597+

1598+

1599+I wonder if the work has become too constrained by porting directly from the Haskell implementation. Perhaps a question to ask in future work would be - what would a dependently typed API to GPUs look like? What properties do we want to capture, and how can we do so with minimal work for the programmer?

1600+

1601+

1602+Nevertheless, I enjoyed reading the paper and I think this is a good first step towards data parallel programming with dependent types.

1603+

1604+

1605+Minor comments:

1606+

1607+

1608+p3 Given that proceedings are in black and white, maybe it'd be more distinctive to put the Haskell code in a box rather than just a vertical bar?

1609+

1610+

1611+p8 It would be useful to see the type of the zipWith function which corresponds to the Haskell version, if not the implementation (which I suspect is a little tricky).

1612+

1613+

1614+p9 Probably not relevant to this paper, but this comment about properties of floating point arithmetic makes me wonder if it'd be possible to represent floating point error bounds in the type to recover these properties.

1615+

1616+

1617+p10 Another alternative for the type of filter could be a type level function to calculate the length. However, this would probably make proofs even harder. I think this is evidence that dependently typed programming is more than Haskell plus extra type annotations!

1618+

1619+

1620+p14 "We have build" => "We have built"},

1621+author = {Thiemann, Peter and Chakravarty, Manuel M T},

1622+file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_30.pdf:pdf},

1623+keywords = {data parallelism,programming with dependent types},

1624+pages = {1--16},

1625+title = {{Agda Meets Accelerate}}

1626+}

1627+@inproceedings{atkey2009unembedding,

1628+author = {Atkey, R. and Lindley, S. and Yallop, J.},

1629+booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},

1630+pages = {37--48},

1631+publisher = {ACM},

1632+title = {{Unembedding domain-specific languages}},

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

1634+year = {2009}

1635+}

1636+@inproceedings{ko2011modularising,

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

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

1639+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

1640+pages = {13--24},

1641+publisher = {ACM},

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

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

1644+year = {2011}

1645+}

1646+@article{Chapman2005epigram,

1647+author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},

1648+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},

1649+journal = {Trends in Functional Programming},

1650+publisher = {Intellect Books},

1651+title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},

1652+url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},

1653+year = {2005}

1654+}

1655+@article{Hutton,

1656+author = {Hutton, Graham and Fulger, Diana},

1657+file = {:Users/edwin/Downloads/effects.pdf:pdf},

1658+title = {{Reasoning About Effects : Seeing the Wood Through the Trees}}

1659+}

1660+@article{dybjer1994inductive,

1661+author = {Dybjer, P.},

1662+journal = {Formal aspects of computing},

1663+number = {4},

1664+pages = {440--465},

1665+publisher = {Springer},

1666+title = {{Inductive families}},

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

1668+volume = {6},

1669+year = {1994}

1670+}

1041@misc{TheMendeleySupportTeam2011a,

1671@misc{TheMendeleySupportTeam2011a,

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

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

1043address = {London},

1673address = {London},

1044author = {{The Mendeley Support Team}},

1674author = {{The Mendeley Support Team}},

1045booktitle = {Mendeley Desktop},

1675booktitle = {Mendeley Desktop},

1046−file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/Mendeley Desktop/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

1676+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

1047keywords = {Mendeley,how-to,user manual},

1677keywords = {Mendeley,how-to,user manual},

1048pages = {1--16},

1678pages = {1--16},

1049publisher = {Mendeley Ltd.},

1679publisher = {Mendeley Ltd.},

@@ -1051,35 +1681,21 @@ title = {{Getting Started with Mendeley}},

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

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

1052year = {2011}

1682year = {2011}

1053}

1683}

1054−@article{danielsson2011parsing,

1684+@misc{Brady2012b,

1055−author = {Danielsson, N. and Norell, U.},

1685+author = {Brooks, Fred},

1056−journal = {Implementation and Application of Functional Languages},

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

1057−pages = {80--99},

1058−publisher = {Springer},

1059−title = {{Parsing mixfix operators}},

1060−url = {http://www.springerlink.com/index/386243257W504252.pdf},

1061−year = {2011}

1062−}

1063−@misc{dagand2011transporting,

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

1065−file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Unknown/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

1066−title = {{Transporting Functions across Ornaments}},

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

1068−year = {2011}

1069−}

1070−@book{Fowler,

1071−author = {Fowler, Martin},

1072−booktitle = {Language},

1073−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Language/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},

1687+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},

1074−isbn = {9780132107549},

1688+isbn = {9780321702081},

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

1689+issn = {1478-6729},

1690+pmid = {22215642},

1691+title = {{The Design of Design Chapter 2}}

1076}

1692}

1077@misc{Bove2008,

1693@misc{Bove2008,

1078abstract = {In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is based on ideas in Martin-L\"{o}f type theory and Martin-L\"{o}fs logical framework. We begin by showing how to do simply typed functional programming, and discuss the differences between Agdas type system and the Hindley-Milner type system, which underlies mainstream typed functional programming languages like Haskell and ML. We then show how to employ dependent types for programming with functional data structures such as vectors and binary search trees. We go on to explain the Curry-Howard identification of propositions and types, and how it makes Agda not only a programming language but also a programming logic. According to Curry-Howard, we also identify programs and proofs, something which is possible only by requiring that all program terminate. However, we show in the final section a method for encoding general and possibly partial recursive functions as total functions using dependent types.},

1694abstract = {In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is based on ideas in Martin-L\"{o}f type theory and Martin-L\"{o}fs logical framework. We begin by showing how to do simply typed functional programming, and discuss the differences between Agdas type system and the Hindley-Milner type system, which underlies mainstream typed functional programming languages like Haskell and ML. We then show how to employ dependent types for programming with functional data structures such as vectors and binary search trees. We go on to explain the Curry-Howard identification of propositions and types, and how it makes Agda not only a programming language but also a programming logic. According to Curry-Howard, we also identify programs and proofs, something which is possible only by requiring that all program terminate. However, we show in the final section a method for encoding general and possibly partial recursive functions as total functions using dependent types.},

1079author = {Bove, Ana and Dybjer, Peter},

1695author = {Bove, Ana and Dybjer, Peter},

1080booktitle = {Notes},

1696booktitle = {Notes},

1081doi = {10.1007/978-3-642-03153-3_2},

1697doi = {10.1007/978-3-642-03153-3_2},

1082−file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Notes/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},

1698+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},

1083number = {February},

1699number = {February},

1084pages = {57--99},

1700pages = {57--99},

1085publisher = {Springer},

1701publisher = {Springer},

@@ -1088,111 +1704,367 @@ url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},

1088volume = {5520},

1704volume = {5520},

1089year = {2008}

1705year = {2008}

1090}

1706}

1091−@article{Okasaki1993,

1707+@article{In2012,

1092−author = {Okasaki, Chris},

1708+author = {Gulhati, Ashish},

1093−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Journal of functional programming/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

1709+doi = {10.1093/geront/gns026},

1094−journal = {Journal of functional programming},

1710+file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter11SecureCommunicati.pdf:pdf},

1095−title = {{Red-Black Trees in A Functional Setting}},

1711+isbn = {9780596510046},

1712+issn = {1758-5341},

1713+month = dec,

1714+number = {6},

1715+pages = {NP},

1716+pmid = {23150082},

1717+title = {{Beautiful Code Chapter 11}},

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

1719+volume = {52},

1096−year = {1993}

1720+year = {2012}

1097}

1721}

1722+@article{McBride2002,

1723+author = {McBride, C},

1724+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 2000 - Elimination with a Motive.pdf:pdf},

1725+journal = {Types for proofs and programs ({TYPES 2000})},

1726+title = {{Elimination with a Motive}},

1727+url = {http://www.springerlink.com/index/vbpg19305t46f6dm.pdf},

1728+year = {2000}

1729+}

1098−@inproceedings{pj2006gadts,

1730+@inproceedings{lempsink2009type,

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

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

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

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

1101−file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/{International Conference on Functional Programming} ({ICFP} '06)/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},

1733+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},

1102−number = {9},

1103−pages = {50--61},

1734+pages = {61--72},

1104publisher = {ACM},

1735publisher = {ACM},

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

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

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

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

1107−volume = {41},

1738+year = {2009}

1739+}

1740+@inproceedings{Brady2011a,

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

1742+author = {Brady, Edwin},

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

1744+doi = {10.1145/1929529.1929536},

1745+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},

1746+isbn = {9781450304870},

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

1748+mendeley-tags = {Dependent Types},

1749+month = jan,

1750+publisher = {ACM Press},

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

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

1108−year = {2006}

1753+year = {2011}

1109}

1754}

1110@misc{altenkirch2005dependent,

1755@misc{altenkirch2005dependent,

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

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

1112booktitle = {Manuscript, available online},

1757booktitle = {Manuscript, available online},

1113−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Manuscript, available online/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

1758+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

1114title = {{Why dependent types matter}},

1759title = {{Why dependent types matter}},

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

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

1116year = {2005}

1761year = {2005}

1117}

1762}

1118−@misc{The2012c,

1763+@misc{Nodes2012a,

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

1764+author = {Brooks, Fred},

1120doi = {10.1093/epirev/mxr031},

1765doi = {10.1093/epirev/mxr031},

1121−file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Unknown/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

1766+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},

1122−isbn = {9780596529833},

1767+isbn = {9780321702081},

1123issn = {1478-6729},

1768issn = {1478-6729},

1124pmid = {22215642},

1769pmid = {22215642},

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

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

1126}

1771}

1127−@misc{Resolution2012a,

1772+@article{danielsson2011parsing,

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

1773+author = {Danielsson, N. and Norell, U.},

1129−doi = {10.1093/epirev/mxr031},

1774+journal = {Implementation and Application of Functional Languages},

1130−file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Unknown/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

1775+pages = {80--99},

1131−issn = {1478-6729},

1776+publisher = {Springer},

1132−pmid = {22215642},

1777+title = {{Parsing mixfix operators}},

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

1778+url = {http://www.springerlink.com/index/386243257W504252.pdf},

1779+year = {2011}

1134}

1780}

1135−@article{Brady2006a,

1781+@book{Bird2010,

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

1782+author = {Bird, Richard},

1137−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/\ldots of the 5th international conference on \ldots/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

1783+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},

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

1784+isbn = {9780521513388},

1139−keywords = {Dependent Types},

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

1140−mendeley-tags = {Dependent Types},

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

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

1143−year = {2006}

1786+year = {2010}

1144}

1787}

1788+@article{Jones1999,

1789+abstract = {Haskell benefits from a sophisticated type system, but implementors, programmers, and researchers suffer because it has no formal description. To remedy this shortcoming, we present a Haskell program that implements a Haskell typechecker, thus providing a mathematically rigorous specification in a notation that is familiar to Haskell users. We expect this program to fill a serious gap in current descriptions of Haskell, both as a starting point for discussions about existing features of the type system, and as a platform from which to explore new proposals.},

1790+author = {Jones, Mark P},

1791+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Jones - 1999 - Typing Haskell in Haskell.pdf:pdf},

1792+journal = {October},

1793+publisher = {Citeseer},

1794+title = {{Typing Haskell in Haskell}},

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

1796+year = {1999}

1797+}

1798+@book{Security2012,

1799+author = {Pfleeger, Charles P and Pfleeger, S. L.},

1800+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

1801+doi = {10.1093/ntr/nts035},

1802+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 3.pdf:pdf},

1803+isbn = {0132390779},

1804+issn = {1469-994X},

1805+month = oct,

1806+number = {10},

1807+pages = {NP},

1808+pmid = {23012339},

1809+title = {{Security in Computing Chapter 3}},

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

1811+volume = {14},

1812+year = {2012}

1813+}

1814+@article{Steiner1988,

1815+author = {Steiner, JG},

1816+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

1817+journal = {Proc. Winter USENIX Conference},

1818+title = {{Kerberos: An authentication service for open network systems}},

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

1820+year = {1988}

1821+}

1145−@inproceedings{swierstra2007beauty,

1822+@inproceedings{stump2010resource,

1146−author = {Swierstra, W. and Altenkirch, T.},

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

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

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

1148−file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra, Altenkirch/Proceedings of the ACM SIGPLAN workshop on Haskell workshop/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},

1825+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

1149−pages = {25--36},

1826+pages = {27--38},

1150publisher = {ACM},

1827publisher = {ACM},

1151−title = {{Beauty in the beast}},

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

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

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

1153−year = {2007}

1830+year = {2010}

1154}

1831}

1155−@article{McBride2004a,

1832+@article{fisher2006next,

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

1833+author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},

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

1834+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},

1158−doi = {10.1017/S0956796803004829},

1835+journal = {Journal of the ACM},

1159−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/Journal of Functional Programming/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

1836+number = {2},

1160−issn = {09567968},

1837+pages = {1--51},

1838+publisher = {ACM},

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

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

1841+volume = {15},

1842+year = {2010}

1843+}

1844+@inproceedings{brady2011epic,

1845+author = {Brady, Edwin},

1846+booktitle = {Trends in Functional Programming ({TFP}’11)},

1847+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},

1848+title = {{Epic --- A Library for Generating Compilers}},

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

1850+year = {2011}

1851+}

1852+@inproceedings{Brady2006b,

1853+author = {Brady, Edwin},

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

1855+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

1856+isbn = {978-3-540-74129-9},

1857+month = sep,

1858+pages = {145----162},

1859+title = {{Ivor, a proof engine}},

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

1861+year = {2006}

1862+}

1863+@article{Reynolds1972,

1864+abstract = {Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters which are themselves written in a programming language based on the lambda calculus (i.e., an applicative language such as pure LISP). Examples include McCarthy's definition of LISP, Landin's SECD machine, the Vienna definition of PL/I, Reynolds' definitions of GEDANKEN, and recent unpublished work by L. Morris and C. Wadsworth. Such definitions can be classified according to whether the interpreter contains higher-order functions, and whether the order of application (i.e., call-by-value versus call-by-name) in the defined language depends upon the order of application in the defining language. As an example, we consider the definition of a simple applicative programming language by means of an interpreter written in a similar language. Definitions in each of the above classifications are derived from one another by informal but constructive methods. The treatment of imperative features such as jumps and assignment is also discussed.},

1865+author = {Reynolds, John C},

1866+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Reynolds - 1972 - Definitional interpreters for higher-order programming languages.pdf:pdf},

1867+journal = {Proceedings of the ACM annual conference on ACM 72},

1868+keywords = {applicative language,closure,continuation,gedanken,higher order function,interpreter,j operator,lambda calculus,language definition,lisp,order application,pal,programming language,reference,secd machine},

1869+number = {30602},

1870+pages = {717--740},

1871+publisher = {ACM Press},

1872+title = {{Definitional interpreters for higher-order programming languages}},

1873+volume = {2},

1874+year = {1972}

1875+}

1876+@book{Hunt,

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

1878+booktitle = {Design},

1879+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},

1880+isbn = {020161622X},

1881+title = {{The Pragmatic Programmer Chapter 4}}

1882+}

1883+@article{Epstein2011,

1884+author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},

1885+institution = {Microsoft Research},

1886+journal = {researchmicrosoftcom},

1887+number = {Section 8},

1888+pages = {1--12},

1889+title = {{Haskell for the cloud}},

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

1891+year = {2011}

1892+}

1893+@book{Bertot2004,

1894+author = {Bertot, Yves and Cast\'{e}ran, Pierre},

1895+publisher = {Springer},

1896+title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},

1897+url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},

1898+year = {2004}

1899+}

1900+@article{Swierstra2011,

1901+author = {Swierstra, W},

1902+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},

1161journal = {Journal of Functional Programming},

1903journal = {Journal of Functional Programming},

1904+number = {6},

1905+pages = {575----583},

1906+title = {{Sorted: Verifying the Problem of the {Dutch National} Flag in {Agda}}},

1907+url = {http://journals.cambridge.org/abstract_S0956796811000207},

1908+volume = {21},

1909+year = {2011}

1910+}

1911+@misc{Casinghino2012,

1912+author = {Casinghino, Chris and Sj\"{o}berg, Vilhelm and Weirich, Stephanie},

1913+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Casinghino, Sj{o}berg, Weirich - 2012 - Combining Proofs and Programs in a Dependently Typed Language.pdf:pdf},

1914+keywords = {dependent types,general recursion,termination},

1915+pages = {1--12},

1916+title = {{Combining Proofs and Programs in a Dependently Typed Language}},

1917+year = {2012}

1918+}

1919+@article{Huet1997,

1920+author = {Huet, G},

1921+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Huet - 1997 - The zipper.pdf:pdf},

1922+journal = {{Journal of Functional Programming}},

1923+number = {5},

1924+pages = {549----554},

1925+title = {{The zipper}},

1926+url = {http://journals.cambridge.org/abstract_S0956796897002864},

1927+volume = {7},

1928+year = {1997}

1929+}

1930+@inproceedings{bradyresource,

1931+author = {Brady, Edwin and Hammond, Kevin},

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

1933+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},

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

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

1936+url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},

1937+year = {2012}

1938+}

1939+@book{Management,

1940+author = {Totty, Brian and Gourley, David},

1941+file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter4ConnectionManageme.pdf:pdf},

1942+isbn = {1565925092},

1943+title = {{HTTP: The Definitive Guide Chapter 4}}

1944+}

1945+@phdthesis{Brady2005,

1946+author = {Brady, Edwin},

1947+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},

1162keywords = {Dependent Types},

1948keywords = {Dependent Types},

1163mendeley-tags = {Dependent Types},

1949mendeley-tags = {Dependent Types},

1164−number = {1},

1950+school = {University of Durham},

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

1952+year = {2005}

1953+}

1954+@article{Lee2001,

1955+author = {Lee, Chin Soon and Jones, Neil D. and Ben-Amram, Amir M.},

1956+doi = {10.1145/373243.360210},

1957+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Lee, Jones, Ben-Amram - 2001 - The size-change principle for program termination.pdf:pdf},

1958+isbn = {1-58113-336-7},

1959+issn = {03621340},

1960+journal = {ACM SIGPLAN Notices},

1961+keywords = {PSPACE-completeness,omega automaton,partial evaluation,program analysis,termination},

1962+month = mar,

1963+number = {3},

1165−pages = {69--111},

1964+pages = {81--92},

1166−publisher = {Cambridge University Press},

1965+title = {{The size-change principle for program termination}},

1167−title = {{The view from the left}},

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

1168−url = {http://www.journals.cambridge.org/abstract_S0956796803004829},

1169−volume = {14},

1967+volume = {36},

1170−year = {2004}

1968+year = {2001}

1969+}

1970+@misc{Bloat,

1971+author = {Brooks, Fred},

1972+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},

1973+isbn = {9780321702081},

1974+title = {{The Design of Design Chapter 4}}

1171}

1975}

1172−@misc{Nodes2012a,

1976+@misc{Caldwell,

1173−author = {Brooks, Fred},

1977+author = {Caldwell, James and Roan, Ryan},

1978+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Caldwell, Roan - Unknown - Type Checking SQL for Secure Database Access.pdf:pdf},

1979+title = {{Type Checking SQL for Secure Database Access}}

1980+}

1981+@inproceedings{Peterson1993,

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

1983+author = {Peterson, John and Jones, Mark},

1984+booktitle = {Proceedings of the ACM SIGPLAN 1993 conference on Programming Language Design and Implementation - PLDI '93},

1985+doi = {10.1145/155090.155112},

1986+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Peterson, Jones - 1993 - Implementing type classes.pdf:pdf},

1987+isbn = {0897915984},

1988+issn = {0362-1340},

1989+month = aug,

1990+number = {6},

1991+pages = {227--236},

1992+publisher = {ACM Press},

1993+title = {{Implementing type classes}},

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

1995+volume = {28},

1996+year = {1993}

1997+}

1998+@misc{Attacks2012a,

1999+author = {Anderson, Ross},

1174doi = {10.1093/epirev/mxr031},

2000doi = {10.1093/epirev/mxr031},

1175−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},

2001+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},

1176−isbn = {9780321702081},

2002+isbn = {9780470068526},

1177issn = {1478-6729},

2003issn = {1478-6729},

2004+number = {1},

2005+pages = {NP},

1178pmid = {22215642},

2006pmid = {22215642},

1179−title = {{The Design of Design Chapter 3}}

2007+title = {{Security Engineering Chapter 18}},

2008+volume = {34}

1180}

2009}

1181−@inproceedings{Hancock2000,

2010+@inproceedings{bhargavan2010modular,

1182−author = {Hancock, Peter and Setzer, Anton},

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

1183−booktitle = {{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}},

2012+booktitle = {ACM Sigplan Notices},

1184−file = {:Users/edwin/Documents/Mendeley Desktop/Hancock, Setzer/{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}/Hancock, Setzer - 2000 - Interactive Programs in Dependent Type Theory.pdf:pdf},

2013+number = {1},

1185−isbn = {3-540-67895-6},

2014+pages = {445--456},

1186−month = aug,

2015+publisher = {ACM},

1187−pages = {317--331},

2016+title = {{Modular verification of security protocol code by typing}},

1188−title = {{Interactive Programs in Dependent Type Theory}},

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

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

2018+volume = {45},

1190−year = {2000}

2019+year = {2010}

2020+}

2021+@article{Hoare1978,

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

2023+author = {Hoare, C A R},

2024+doi = {10.1016/0167-6423(87)90028-1},

2025+editor = {McKeag, R M and Macnaghten, A M},

2026+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hoare - 1978 - Communicating sequential processes.pdf:pdf},

2027+isbn = {0131532715},

2028+issn = {01676423},

2029+journal = {Communications of the ACM},

2030+number = {8},

2031+pages = {666--677},

2032+pmid = {2142694823583477576},

2033+publisher = {ACM},

2034+series = {International Series in Computer Science},

2035+title = {{Communicating sequential processes}},

2036+url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},

2037+volume = {21},

2038+year = {1978}

2039+}

2040+@article{Overview,

2041+author = {Totty, Brian and Gourley, David},

2042+file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter1OverviewofHTTP.pdf:pdf},

2043+isbn = {1565925092},

2044+title = {{HTTP: The Definitive Guide Chapter 1}}

2045+}

2046+@book{Fogel,

2047+author = {Fogel, Karl},

2048+file = {:Users/edwin/Downloads/Books/producingoss.pdf:pdf},

2049+title = {{Producing Open Source Software: How to Run a Successful Free Software Project}}

2050+}

2051+@book{Brady2012,

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

2053+booktitle = {Carcinogenesis},

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

2055+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},

2056+isbn = {020161622X},

2057+issn = {1460-2180},

2058+number = {3},

2059+pmid = {22383472},

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

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

2062+volume = {33}

1191}

2063}

1192@inproceedings{augustsson2008paradise,

2064@inproceedings{augustsson2008paradise,

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

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

1194booktitle = {International Conference on Functional Programming},

2066booktitle = {International Conference on Functional Programming},

1195−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson, Mansell, Sittampalam/International Conference on Functional Programming/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},

2067+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},

1196number = {9},

2068number = {9},

1197pages = {225--228},

2069pages = {225--228},

1198publisher = {ACM},

2070publisher = {ACM},

@@ -1201,61 +2073,185 @@ url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},

1201volume = {43},

2073volume = {43},

1202year = {2008}

2074year = {2008}

1203}

2075}

1204−@misc{Abel1998,

2076+@article{marlow2006making,

1205−author = {Abel, Andreas},

2077+author = {Marlow, S. and {Peyton Jones}, S.},

1206−booktitle = {Language},

2078+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},

1207−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Language/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

2079+journal = {Journal of Functional Programming},

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

2080+number = {4-5},

2081+pages = {415--449},

2082+publisher = {Cambridge University Press},

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

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

2085+volume = {16},

1209−year = {1998}

2086+year = {2006}

1210}

2087}

1211−@article{Jones1999,

2088+@misc{TheMendeleySupportTeam2011b,

1212−abstract = {Haskell benefits from a sophisticated type system, but implementors, programmers, and researchers suffer because it has no formal description. To remedy this shortcoming, we present a Haskell program that implements a Haskell typechecker, thus providing a mathematically rigorous specification in a notation that is familiar to Haskell users. We expect this program to fill a serious gap in current descriptions of Haskell, both as a starting point for discussions about existing features of the type system, and as a platform from which to explore new proposals.},

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

1213−author = {Jones, Mark P},

2090+address = {London},

1214−journal = {October},

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

1215−publisher = {Citeseer},

2092+booktitle = {Mendeley Desktop},

1216−title = {{Typing Haskell in Haskell}},

2093+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

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

2094+keywords = {Mendeley,how-to,user manual},

2095+pages = {1--16},

2096+publisher = {Mendeley Ltd.},

2097+title = {{Getting Started with Mendeley}},

2098+url = {http://www.mendeley.com},

2099+year = {2011}

2100+}

2101+@inproceedings{ko2011modularising,

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

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

2104+pages = {13--24},

2105+publisher = {ACM},

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

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

2108+year = {2011}

2109+}

2110+@book{Fry1985,

2111+author = {Abelson, Harold and Sussman, Gerald and Sussman, Julie},

2112+booktitle = {Computer Music Journal},

2113+doi = {10.2307/3679579},

2114+file = {:Users/edwin/Downloads/sicp.pdf:pdf},

2115+isbn = {0262011530},

2116+issn = {01489267},

2117+month = jan,

2118+number = {3},

2119+title = {{Structure and Interpretation of Computer Programs}},

2120+url = {http://www.jstor.org/stable/3679579?origin=crossref},

2121+volume = {9},

2122+year = {1985}

2123+}

2124+@article{Bird2012,

2125+annote = {I enjoyed reading this pearl. It describes, clearly and concisely, the calculation of a program for changing the way of representing a graph in response to a challenge of Donald Knuth's, who asked whether such an algorithm could be discovered in a "disciplined manner". The paper describes that disciplined manner.

2126+

2127+

2128+

2129+

2130+In general, I found the paper easy to follow. Section 2 sets up the problem, giving a purely functional representation of graphs and the definitions of some basic, important functions, in particular encode and decode. Section 3 gives a first example of program calculation, assuming the existence of a function 'lengthen' corresponding to 'shorten' and deriving an implementation from its required properties. Later, we see a definition using arrays rather than lists in order to improve the complexity to linear time. Section 4 addresses a condition Knuth imposes, namely that update must be in place and gives an imperative translation.

2131+

2132+

2133+I think this paper gives a nice example of program calculation leading from a functional specification to an imperative program. I do have a few suggestions though which I think would improve the paper:

2134+

2135+

2136+In the introduction, you say there is a reason why the code cannot be purely functional, but I don't see an explicit explanation of why this is. In place update perhaps? Can this be clarified?

2137+

2138+

2139+The equation numbering, e.g. (1) at the bottom of p1 - some equations are clearly important and referred to elsewhere, such as this one. Is it possible to make these stand out more? e.g. with an explicit heading "Equation 1"?

2140+

2141+

2142+p3 In the first examples of program calculation, it is easy to follow the reasoning of why the calculation is correct, but it is not so obvious what the insight was that led to the calculation. Is this simply a matter of experience?

2143+

2144+

2145+p6 I'm surprised to read that // updates an array in place. Is this really what is happening or is there a clever representation of Data.Array.Diff? It appears to use IO operations internally. So it might be nice to say a little more about what is really going on.

2146+

2147+

2148+p7 "...an observation that could have been made earlier" seems an odd thing to say. Why not either make it earlier, or just make it here where it is used?

2149+

2150+

2151+p9 There is no need to give the translation rules to the imperative code in detail, but it would still be useful to sketch what is going on. It seems that the foldr becomes the outer for loop, and apply the inner for loop. It would also be useful, in Figs 1-4 to give the functional code alongside the imperative versions. It is interesting to examine how the mapping works and I think an important point made by the paper (as indeed you say in the conclusion).

2152+

2153+

2154+p14 The last paragraph appears to be largely a comment to the present referees!

2155+

2156+ },

2157+author = {Bird, Richard S},

2158+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bird - 2012 - An in-situ algorithm for expanding a graph.pdf:pdf},

2159+journal = {Journal of Functional Programming},

2160+keywords = {a href,journal of functional programming},

2161+title = {{An in-situ algorithm for expanding a graph}},

2162+year = {2012}

2163+}

2164+@article{Ahn,

2165+annote = {-1,5

2166+

2167+

2168+The paper describes Nax, a new functional programming language with term indices which supports logical consistency and Hindley-Milner style type inference. The authors give four key features of Nax (1: strong normalization, 2: type inference, 3: expressivity and 4: support for term indices) and give several examples to demonstrate the simplicity of programming in Nax as compared with Haskell and Agda. Three examples are given, in each language: a type preserving evaluator for an expression language, a generic Path datatype which describes a path through an index type, and a stack safe compiler for the expression language.

2169+

2170+

2171+Presenting examples in this way gives a nice introduction to Nax, in that they are well understood examples already and it is easy to relate them to implementations with which the reader is already familiar. On the other hand, this leads to my main problem with this paper: it doesn't really tell us anything we don't already know, and the promising things about Nax which *would* be an interesting contribution are left out of the paper.

2172+

2173+

2174+Of the four features of Nax given above, 1 and 2 are described as "beyond the scope of this paper" which is a shame because these are the things I'm most interested in hearing about! Existing dependently typed languages lack type inference, and whlie I would argue that it is usually best to write types first in any case, there are still many situations where recovering type inference would be useful - typically small or simply typed helper functions. So this would have been a very nice technical contribution.

2175+

2176+

2177+The third feature (expressivity) is one that the authors claim as a contribution of the paper. They claim that programming in Nax is as "simple" as programming in Haskell or Agda. However, I think this is a strong claim to make given the available evidence - it is quite subjective. I agree that the programs are quite easy to read, but to say that *programming* is as simple really requires some externally verified evidence from other programmers! It seems to me that programming with Mendler-style combinators may take some practice, for example.

2178+

2179+

2180+In summary, I do like the idea behind Nax and some of its features sound as if they could be interesting, and I think this latest contribution to the design space of dependently typed functional programming is welcome. But this paper does not really provide any new insights as it stands.

2181+

2182+

2183+Minor comments:

2184+

2185+

2186+Fig 1,2 and 3 - I'm not sure I would like the rotation of these in print (it's pretty awkward on screen too).},

2187+author = {Ahn, Ki Yung and Sheard, Tim and Fiore, Marcelo and Pitts, Andrew M},

2188+file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_28.pdf:pdf},

2189+keywords = {gadts,indexed datatypes,lightweight dependent types,term-indexed types,universe polymorphism,universe subtyping},

2190+title = {{Programming with Term-Indexed Types in Nax}}

2191+}

2192+@article{Morrisett1999,

2193+author = {Morrisett, G and Walker, D},

2194+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Morrisett, Walker - 1999 - From System F to typed assembly language.pdf:pdf},

2195+journal = {ACM Transactions on \ldots},

2196+title = {{From System F to typed assembly language}},

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

1218year = {1999}

2198year = {1999}

1219}

2199}

1220−@inproceedings{morris2006exploring,

2200+@article{Altenkirch2010a,

1221−author = {Morris, P. and Altenkirch, T. and McBride, C.},

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

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

2202+author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},

1223−file = {:Users/edwin/Documents/Mendeley Desktop/Morris, Altenkirch, McBride/Types for Proofs and Programs/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

2203+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},

1224−pages = {252--267},

2204+journal = {Citeseer},

1225−publisher = {Springer},

2205+publisher = {Citeseer},

1226−title = {{Exploring the regular tree types}},

2206+title = {{Generic Programming with Dependent Types}},

1227−url = {http://www.springerlink.com/index/f9p1317716614834.pdf},

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

1228−year = {2006}

2208+year = {2010}

1229}

2209}

1230−@inproceedings{Sheard2005,

2210+@book{Edition2012a,

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

2211+author = {Pfleeger, Charles P and Pfleeger, S. L.},

1232−author = {Sheard, Tim},

2212+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

1233−booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},

2213+doi = {10.1093/ntr/nts035},

1234−doi = {10.1145/1088348.1088356},

2214+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computer Chapter 12.pdf:pdf},

1235−file = {:Users/edwin/Documents/Mendeley Desktop/Sheard/Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},

2215+isbn = {0132390779},

1236−isbn = {159593071X},

2216+issn = {1469-994X},

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

1238−month = sep,

2217+month = oct,

2218+number = {10},

1239−pages = {74--85},

2219+pages = {NP},

1240−publisher = {ACM Press},

2220+pmid = {23012339},

1241−title = {{Putting curry-howard to work}},

2221+title = {{Security in Computer Chapter 12}},

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

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

2223+volume = {14},

1243−year = {2005}

2224+year = {2012}

1244}

2225}

1245−@misc{Interface2012a,

2226+@book{Pierce2004,

1246−author = {Kreibich, Jay A.},

2227+author = {Pierce, Benjamin},

1247−doi = {10.1093/epirev/mxr031},

2228+editor = {Pierce, Benjamin},

1248−file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Unknown/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

2229+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pierce - 2004 - Advanced topics in types and programming languages.pdf:pdf},

1249−isbn = {9781449394592},

2230+publisher = {MIT Press},

1250−issn = {1478-6729},

2231+title = {{Advanced topics in types and programming languages}},

1251−pmid = {22215642},

2232+year = {2004}

1252−title = {{Using SQLite Chapter 7}}

2233+}

2234+@inproceedings{taha1997multi,

2235+author = {Taha, W. and Sheard, T.},

2236+booktitle = {ACM SIGPLAN Notices},

2237+number = {12},

2238+pages = {203--217},

2239+publisher = {ACM},

2240+title = {{Multi-stage programming with explicit annotations}},

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

2242+volume = {32},

2243+year = {1997}

2244+}

2245+@misc{Lorenzen,

2246+author = {Lorenzen, Florian},

2247+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Lorenzen - Unknown - A Statically Typed Functional Language With Programmable Binders.pdf:pdf},

2248+title = {{A Statically Typed Functional Language With Programmable Binders}}

1253}

2249}

1254@book{The2012,

2250@book{The2012,

1255author = {Hunt, Andrew and Thomas, David},

2251author = {Hunt, Andrew and Thomas, David},

1256booktitle = {Carcinogenesis},

2252booktitle = {Carcinogenesis},

1257doi = {10.1093/carcin/bgs054},

2253doi = {10.1093/carcin/bgs054},

1258−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},

2254+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},

1259isbn = {020161622X},

2255isbn = {020161622X},

1260issn = {1460-2180},

2256issn = {1460-2180},

1261number = {3},

2257number = {3},

@@ -1264,68 +2260,18 @@ title = {{The Pragmatic Programmer Chapter 3}},

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

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

1265volume = {33}

2261volume = {33}

1266}

2262}

1267−@misc{Brady2012b,

1268−author = {Brooks, Fred},

1269−doi = {10.1093/epirev/mxr031},

1270−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},

1271−isbn = {9780321702081},

1272−issn = {1478-6729},

1273−pmid = {22215642},

1274−title = {{The Design of Design Chapter 2}}

1275−}

1276−@inproceedings{Levitation2010,

2263+@inproceedings{pollack1990implicit,

1277−author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

2264+author = {Pollack, R.},

1278−booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},

2265+booktitle = {{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}},

1279−doi = {10.1145/1932681.1863547},

2266+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pollack - 1990 - Implicit syntax.pdf:pdf},

1280−file = {:Users/edwin/Documents/Mendeley Desktop/Chapman et al/{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},

2267+publisher = {Citeseer},

1281−isbn = {978-1-60558-794-3},

2268+title = {{Implicit syntax}},

1282−issn = {03621340},

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

1283−keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

1284−mendeley-tags = {Dependent Types},

1285−month = sep,

1286−number = {9},

1287−title = {{The gentle art of levitation}},

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

1289−volume = {45},

1290−year = {2010}

1291−}

1292−@inproceedings{Xi1999,

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

1294−author = {Xi, Hongwei and Pfenning, Frank},

1295−booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},

1296−doi = {10.1145/292540.292560},

1297−file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},

1298−isbn = {1581130953},

1299−issn = {07439016},

1300−keywords = {Dependent Types},

1301−mendeley-tags = {Dependent Types},

1302−organization = {Carnegie Mellon University},

1303−pages = {214--227},

1304−publisher = {ACM Press},

1305−series = {POPL '99},

1306−title = {{Dependent types in practical programming}},

1307−url = {http://portal.acm.org/citation.cfm?doid=292540.292560},

1308−volume = {26},

1309−year = {1999}

2270+year = {1990}

1310−}

1311−@inproceedings{Brady2003,

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

1313−booktitle = {Types for Proofs and Programs {(TYPES 2003)}},

1314−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, McBride, McKinna/Types for Proofs and Programs {(TYPES 2003)}/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},

1315−keywords = {Dependent Types},

1316−mendeley-tags = {Dependent Types},

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

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

1319−year = {2003}

1320}

2271}

1321−@inproceedings{fisher2005pads,

2272+@article{Bradya,

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

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

1323−booktitle = {ACM SIGPLAN Notices},

2274+file = {:Users/edwin/Downloads/Safari/ThePragmaticProgrammerFromJourneymantoMasterChapter7BeforetheProject.pdf:pdf},

1324−number = {6},

2275+isbn = {020161622X},

1325−pages = {295--304},

2276+title = {{The Pragmatic Programmer Chapter 7}}

1326−publisher = {ACM},

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

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

1329−volume = {40},

1330−year = {2005}

1331}

2277}

papers/impl-paper/macros.ltx+2−2

@@ -391,7 +391,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

391

392%%%%%%%%%%%% TYPE

393

394−\newcommand{\Type}{\mbox{\texttt{Set}}} %\star}

394+\newcommand{\Type}{\mbox{\texttt{Type}}} %\star}

395

396

397%%%%%%%%%%%%% ARROWS

@@ -559,7 +559,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

559\newcommand{\VectRebuild}{\FN{vectRebuild}}

560

561\newcommand{\Prop}{\TC{Prop}}

562−\newcommand{\Set}{\TC{Set}}

562+\newcommand{\Set}{\TC{Type}}

563\newcommand{\CoqType}{\TC{Type}}

564

565\newcommand{\List}{\TC{List}}

papers/impl-paper/typechecking.tex+30−22

@@ -28,7 +28,7 @@ type of types, and may be extended with other primitives.

29The function space $\all{\vx}{\vS}\SC\vT$ may also be written as $(\vx\Hab\vS)\to\vT$,

30or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with

31−the high level language. Universe levels on sets ($\Type_i$) may be left implicit and

31+the high level language. Universe levels on types ($\Type_i$) may be left implicit and

32inferred by the machine~\cite{pollack1990implicit}.

34\FFIG{

@@ -73,8 +73,14 @@ $\LET$ binding:

73\DM{

74\Axiom{\proves\RW{valid}}

75\hg

76−\Rule{\Gamma\proves\RW{valid}}

76+\Rule{\Gamma\proves\vS\Hab\Type_i}

77+{\Gamma;\lam{\vx}{\vS}\proves\RW{valid}}

78+\hg

79+\Rule{\Gamma\proves\vS\Hab\Type_i}

80+{\Gamma;\all{\vx}{\vS}\proves\RW{valid}}

81+\hg

82+\Rule{\Gamma\proves\vS\Hab\Type_i\hg\Gamma\proves\vs\Hab\vS}

77−{\Gamma;\vb\proves\RW{valid}}

83+{\Gamma;\LET\:\vx\:\defq\:\vs\Hab\vS\proves\RW{valid}}

78}

84}

80\subsubsection{Evaluation}

86\subsubsection{Evaluation}

@@ -97,7 +103,7 @@ The following contextual closure rule reduces a $\LET$ binding by creating

97a $\delta$-reducible expression:

103a $\delta$-reducible expression:

104

99\DM{

105\DM{

100−\Rule{\Gamma;\LET\:\vx\defq\vs\proves\vt\leadsto\vu}

106+\Rule{\Gamma;\LET\:\vx\defq\vs\Hab\vS\proves\vt\leadsto\vu}

101{\Gamma\proves\LET\:\vx\defq\vs\Hab\vS\SC\vt\leadsto\vu}

107{\Gamma\proves\LET\:\vx\defq\vs\Hab\vS\SC\vt\leadsto\vu}

102}

108}

103

109

@@ -256,10 +262,10 @@ sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):

256}

262}

257}

263}

258

264

259−Constructors may take recursive arguments in the family

265+Constructors may take recursive arguments in the family $\TC{T}$, which may be

260−$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---

266+higher order. Higher order recursive arguments may be computed from any type

261−if such indices do not involve $\TC{T}$ then the constructor is

267+which does not involve $\TC{T}$ itself. This restriction is known as

262−\demph{strictly positive}, which ensures that recursive arguments of the

268+\demph{strict positivity} and ensures that recursive arguments of the

263constructor are structurally smaller than the value itself.

269constructor are structurally smaller than the value itself.

264

270

265For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:

271For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:

@@ -526,7 +532,7 @@ algorithm:

526

532

527\begin{SaveVerbatim}{vAddImpSolve}

533\begin{SaveVerbatim}{vAddImpSolve}

528

534

529−vAdd : (a : Set) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n

535+vAdd : (a : Type) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n

530vAdd a O c (Nil a) (Nil a) = Nil a

536vAdd a O c (Nil a) (Nil a) = Nil a

531vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)

537vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)

532 = (::) a k ((+) c x y) (vAdd a k c xs ys)

538 = (::) a k ((+) c x y) (vAdd a k c xs ys)

@@ -541,17 +547,17 @@ switching to \TT{} notation from the ASCII \Idris{} syntax.

541\FFIG{

547\FFIG{

542\AR{

548\AR{

543\begin{array}{ll}

549\begin{array}{ll}

544−\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to

550+\FN{vAdd} & \Hab(\va\Hab\Type)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to

545 \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\

551 \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\

546\end{array}

552\end{array}

547\\

553\\

548\begin{array}{lccccccc}

554\begin{array}{lccccccc}

549\multicolumn{5}{l}{

555\multicolumn{5}{l}{

550−\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\

556+\RW{var}\:\va\Hab\Type,\:\vc\Hab\TC{Num}\;\va\SC}\\

551\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\

557\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\

552\multicolumn{5}{l}{

558\multicolumn{5}{l}{

553\RW{var}\:\AR{

559\RW{var}\:\AR{

554−\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\

560+\va\Hab\Type,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\

555\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;

561\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;

556\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk

562\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk

557\SC

563\SC

@@ -580,18 +586,20 @@ programming and theorem proving with dependent types, and appropriate mechanisms

580constructing programs and theorems:

586constructing programs and theorems:

581

587

582\begin{itemize}

588\begin{itemize}

583−\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,

589+\item \remph{Pattern matching} is a convenient abstraction for humans to write

584−in that it allows a programmer to express exactly the computational behaviour of a function.

590+programs, in that it allows a programmer to express exactly the computational

591+behaviour of a function.

585−\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},

592+\item \remph{Tactics}, such as those used in the Coq theorem

586−are a convenient abstraction for building proofs and programs by \remph{refinement}.

593+prover~\cite{Bertot2004}, are a convenient abstraction for building proofs and

594+programs by \remph{refinement}.

587\end{itemize}

595\end{itemize}

588

596

589−The idea behind the \Idris{} elaborator, therefore, is to use the high level program

597+The idea behind the \Idris{} elaborator, therefore, is to use the high level

590−to direct \demph{tactics} to build \TT{} programs by refinement. The

598+program to direct \demph{tactics} to build \TT{} programs by refinement. The

591−elaborator is implemented as an Embedded Domain Specific Language (EDSL) in Haskell.

599+elaborator is implemented as a Haskell monad capturing proof state, with a

592−The remainder

600+collection of tactics for updating and refining the proof state. The remainder

593−of this paper describes the EDSL and demonstrates how it is used to implement

601+of this paper describes this elaborator and demonstrates how it is used to

594−all of the high level features of \Idris{}.

602+implement the high level features of \Idris{}.

595

603

596

604

597

605

src/Core/CaseTree.hs+1−1

@@ -79,7 +79,7 @@ instance TermSize CaseAlt where

79small :: Name -> [Name] -> SC -> Bool

80small n args t = let as = findAllUsedArgs t args in

81 length as == length (nub as) &&

82− termsize n t < 20

82+ termsize n t < 5

84namesUsed :: SC -> [Name]

85namesUsed sc = nub $ nu' [] sc where

src/Idris/ElabDecls.hs+16−10

@@ -153,29 +153,35 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

153 collapseCons n cons

154 updateContext (addDatatype (Data n ttag cty cons))

155 mapM_ (checkPositive n) cons

156+ where

157+ -- parameters are names which are unchanged across the structure,

158+ -- which appear exactly once in the return type of a constructor

156− where findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]

159+ findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]

157 findParams ps [] = mapMaybe (\ ((x, y), n) ->

160 findParams ps [] = mapMaybe (\ ((x, y), n) ->

158 if y then Just n else Nothing)

161 if y then Just n else Nothing)

159 (zip ps [0..])

162 (zip ps [0..])

160 findParams ps (t : ts) = findParams (updateParams ps t) ts

163 findParams ps (t : ts) = findParams (updateParams ps t) ts

161

164

162 updateParams ps (Bind n (Pi t) sc)

165 updateParams ps (Bind n (Pi t) sc)

163− = updateParams ps (instantiate (P Bound n t) sc)

166+ = updateParams (updateParams ps (instantiate (P Bound n t) sc)) t

164 updateParams ps tm@(App f a)

167 updateParams ps tm@(App f a)

165 | (P _ fn _, args) <- unApply tm

168 | (P _ fn _, args) <- unApply tm

166 = if fn == n

169 = if fn == n

167− then updateParamsA ps args

170+ then updateParamsA ps args (tail args)

168 else updateParams (updateParams ps f) a

171 else updateParams (updateParams ps f) a

169 | otherwise = updateParams (updateParams ps f) a

172 | otherwise = updateParams (updateParams ps f) a

170 updateParams ps _ = ps

173 updateParams ps _ = ps

171

174

175+ updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all

176+ | n' `elem` concatMap freeNames all

177+ = (mn, False) : updateParamsA ns args (p : all)

172− updateParamsA ((Nothing, b) : ns) (P _ n' _ : args)

178+ updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all

173− = (Just n', b) : updateParamsA ns args

179+ = (Just n', b) : updateParamsA ns args (p : all)

174− updateParamsA ((Just p, b) : ns) (P _ n' _ : args)

180+ updateParamsA ((Just p, b) : ns) (tm@(P _ n' _) : args) all

175− = (Just n', b && p == n') : updateParamsA ns args

181+ = (Just n', b && p == n') : updateParamsA ns args (tm : all)

176− updateParamsA ((mn, _) : ns) (_ : args)

182+ updateParamsA ((mn, _) : ns) (p : args) all

177− = (mn, False) : updateParamsA ns args

183+ = (mn, False) : updateParamsA ns args (p : all)

178− updateParamsA ps args = ps

184+ updateParamsA ps args all = ps

179

185

180elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

186elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

181 PTerm -> String -> Name -> PTerm -> Idris ()

187 PTerm -> String -> Name -> PTerm -> Idris ()