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

git.iko.soy/Idris-dev

Some progress on implementation paper revisions

commit75e77582d90db7f943004ce3543f6acbef92db79 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 7 Feb 2013, 17:36 (14 years ago) parent2a13be4

9 files changed+2195−1194

compare with master

unifiedsplit

papers/impl-paper/conclusions.tex+26−32 papers/impl-paper/elaboration.tex+109−61 papers/impl-paper/hll.tex+11−12 papers/impl-paper/intro.tex+18−18 papers/impl-paper/library.bib+1982−1036 papers/impl-paper/macros.ltx+2−2 papers/impl-paper/typechecking.tex+30−22 src/Core/CaseTree.hs+1−1 src/Idris/ElabDecls.hs+16−10

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

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

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

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

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

11+

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

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

1214the 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

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

6264reduces the possibility of errors.

6365

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

76+several features:

7477

7578\begin{itemize}

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

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

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

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

9194Furthermore,

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

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

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

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

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

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

98−when augmented with primitive operators.

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

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

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

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

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

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

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

99102

100103We have not discussed the performance of the elaboration

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

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

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

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

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

121−language based techniques to realistic problems

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

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

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

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

126−is the right tool for this work.

127−

128−

129−

130−%\subsection{Further Work}

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

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

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

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

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

129+the right tool for this work.

131130

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,

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

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

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

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

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

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

45+%The

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

4647

4748\FFIG{

48−\AR{

49+\begin{array}{c}

4950\vb ::= \ldots

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

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

5253\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}\:

5363\Rule{

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

5565}

5666{

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

5868}

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

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

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

6170\hg

71+\mathsf{Guess}\:

6272\Rule{

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

6474}

6575{

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

6777}

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

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

70−}

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

79+\end{array}

7180}

7281{\TTdev{} extensions}

7382{ttdev}

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

7786

7887\label{sect:prfstate}

7988

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:

8190

8291\begin{itemize}

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

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

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

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

8696\item A hole queue, $\vQ$

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

8898\end{itemize}

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

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

92102in the proof term ---

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

94−in the proof.

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

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

107+problems, the proof term is complete.

108+

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

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

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

99112

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

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

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

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

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

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

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

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

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

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

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

119+implementation details. These meta-operations include:

106120

107121\begin{itemize}

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

109123the state. For example, we can:

110124\begin{itemize}

111−\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}$)

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

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

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

127+($\MO{Context}$)

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

129+to $\Gamma$.

114130\end{itemize}

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

116−relative to $\Gamma$

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

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

133+to the proof state.

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

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

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

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

123140\end{itemize}

124141

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

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

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

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

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

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

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

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

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

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

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

148+guess-bound variables.

131149

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

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

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

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

134152

135153\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)

137155}

138156

139157The 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

143161updates the proof state to:

144162

145163\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)

147165}

148166

149167

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

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

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

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

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

204223

205224\subsection{Tactics}

206225

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

211230primitive meta-operations:

212231

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

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

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

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

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

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

221243$\Gamma$, returning its normal form.

222244\item

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

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

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

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

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

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

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

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

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

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.

228263\end{itemize}

229264

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+

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

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

232280

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

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

279327 \vT' \leftarrow \Check\:\vv\\

280328 \Unify\:\vT\:\vT'\\

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

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

282330 } \\

283331}

284332}

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

288336

289337\DM{

290338\AR{

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

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

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

293341\\

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

335383scope of the binding safely.

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

337385the 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

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

340388

341389\DM{

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

367415}

368416

369417\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}$:

371419

372420\DM{

373421\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) &

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

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

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

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

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

378426 }

379427 }

380428}

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

387435\PA{\A\A}{

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

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

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

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

391439 \vS'\:\leftarrow\:\Check\:\vv\\

392440 \Unify\:\vS\:\vS'\\

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

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

420468\PA{\A\A}{

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

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

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

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

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

425473 }}

426474}

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

445493

446494\DM{

447495\AR{

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

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

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

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

450498}

451499}

452500

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

459507\AR{

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

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

463511 \MO{RunTac}\;\MO{Attack} \\

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

465513 \MO{RunTac}\;\MO{Attack} \\

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

494542\AR{

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

496544 \AR{

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

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

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

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

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

500548 \MO{Fill}\;\vA \\

501549 \MO{Solve} ; \MO{Solve} ; \MO{Solve} \\

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

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

742790\RW{do}\:

743791\AR{

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

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

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

746794\MO{Focus}\:\vX\\

747795\ttinterp{\vt};\;

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

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

768816\AR{

769817\MO{Attack};\;

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

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

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

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

773821\MO{Focus}\:\vV\\

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

872920\DM{

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

874922\AR{

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

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

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

877925\MO{Try}\:

878926\AR{

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

907955

908956\DM{

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

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

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

911959 \ttinterp{\vt}\\

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

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

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

928976\DM{

929977\AR{

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

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

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

932980 \ttinterp{\vt}\\

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

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

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

937985}

938986\AR{

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

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

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

941989 \ttinterp{\vt}\\

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

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

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

9621010a type $\TC{Infer}$:

9631011

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

9661014}

9671015

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

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

11231171

11241172\begin{SaveVerbatim}{showdata}

11251173

1126−data Show : Set -> Set where

1174+data Show : Type -> Type where

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

11281176

11291177show : Show a -> a -> String

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

11821230

11831231\begin{SaveVerbatim}{orddata}

11841232

1185−data Ord : Set -> Set where

1233+data Ord : Type -> Type where

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

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

11881236

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

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

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

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

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

12281276}

12291277}

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

14181466\begin{SaveVerbatim}{appendrec}

14191467

14201468*vec> :t append_rec

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

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

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

14231471

14241472\end{SaveVerbatim}

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

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

192192

193193\begin{SaveVerbatim}{vect}

194194

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

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

196196 Nil : Vect a O

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

198198

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

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

210210declaration: it explicitly states the type

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

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

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

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

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

239239

240240\begin{SaveVerbatim}{findecl}

241241

242−data Fin : Nat -> Set where

242+data Fin : Nat -> Type where

243243 fO : Fin (S k)

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

245245

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

316316

317317\begin{SaveVerbatim}{vindeximpty}

318318

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

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

320320

321321\end{SaveVerbatim}

322322\useverb{vindeximpty}

323323

324324\noindent

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

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

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

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

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

330−of dependent types.

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

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

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

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

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

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

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

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

333332

334333\begin{SaveVerbatim}{vindexexp}

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

577576

578577\begin{SaveVerbatim}{parity}

579578

580−data Parity : Nat -> Set where

579+data Parity : Nat -> Type where

581580 even : Parity (n + n)

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

583582

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

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

3939

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

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

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

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

44−directed by high level program syntax.

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

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

47−of the underlying type theory.

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

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

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

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

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

47+type theory.

4848

4949\subsection{Contributions}

5050

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

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

5656programming language.

5757

58−The primary contribution of this paper is

59−an EDSL based method for translating programs in a

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

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

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

63−for manipulating incomplete programs.

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

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

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

67−\Idris{} with higher level features.

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

69−is equally applicable to other typed programming languages.

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

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

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+introduces a collection of \remph{tactics} for manipulating incomplete

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

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

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

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

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

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

7070

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

7272programming 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

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

4−@book{Chlipala2012,

5−author = {Chlipala, Adam},

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

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

8−year = {2012}

4+@inproceedings{Sozeau2008,

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

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

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

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

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

10+year = {2008}

911}

10−@inproceedings{czarnecki2004dsl,

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

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

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

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

18−year = {2004}

12+@inproceedings{McBride2006,

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

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

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

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

17+year = {2006}

1918}

20−@phdthesis{Brady2005,

21−author = {Brady, Edwin},

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

19+@article{McBride2005,

20+author = {McBride, Conor},

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

22+isbn = {3540285407},

23+journal = {Advanced Functional Programming},

2324keywords = {Dependent Types},

2425mendeley-tags = {Dependent Types},

25−school = {University of Durham},

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

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

26+pages = {130--170},

27+publisher = {Springer},

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

2832year = {2005}

2933}

30−@inproceedings{Kimmell2012,

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

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

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

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

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}

34+@article{Okasaki1993,

35+author = {Okasaki, Chris},

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

37+journal = {Journal of functional programming},

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

39+year = {1993}

4740}

48−@article{Altenkirch2010a,

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

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

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

52−journal = {Citeseer},

53−publisher = {Citeseer},

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

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

56−year = {2010}

41+@inproceedings{Hancock2000,

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

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

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

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

46+month = aug,

47+pages = {317--331},

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

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

50+year = {2000}

5751}

58−@article{fisher2006next,

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

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

61−journal = {Journal of the ACM},

62−number = {2},

63−pages = {1--51},

64−publisher = {ACM},

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

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

67−volume = {15},

68−year = {2010}

52+@article{Turner2004,

53+author = {Turner, D A},

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

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

56+keywords = {functional programming},

57+number = {7},

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

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

60+volume = {10},

61+year = {2004}

6962}

70−@misc{The2012b,

71−author = {Brooks, Fred},

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

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

74−isbn = {9780321702081},

75−issn = {1478-6729},

76−pmid = {22215642},

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

63+@phdthesis{norell2007thesis,

64+author = {Norell, Ulf},

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

66+keywords = {Dependent Types},

67+mendeley-tags = {Dependent Types},

68+publisher = {Citeseer},

69+school = {Chalmers University of Technology},

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}

7873}

79−@article{Chapman2005epigram,

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

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

82−journal = {Trends in Functional Programming},

83−publisher = {Intellect Books},

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

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

86−year = {2005}

74+@article{Wu,

75+annote = {1,3

76+

77+

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).

79+

80+

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

8787}

88−@misc{TheMendeleySupportTeam2011,

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

90−address = {London},

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

92−booktitle = {Mendeley Desktop},

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

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

95−pages = {1--16},

96−publisher = {Mendeley Ltd.},

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

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

99−year = {2011}

88+@inproceedings{NanevskiAAMorrisett2008,

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+author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},

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

92+doi = {10.1145/1411204.1411237},

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

94+isbn = {9781595939197},

95+issn = {15232867},

96+keywords = {Dependent Types},

97+mendeley-tags = {Dependent Types},

98+number = {9},

99+pages = {229--240},

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

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

102+volume = {43},

103+year = {2008}

100104}

101−@phdthesis{Okasaki1996,

102−author = {Okasaki, Chris},

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

104−school = {Carnegie Mellon University},

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

106−year = {1996}

105+@article{Walt,

106+annote = {-1, 5

107+

108+

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.

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

107143}

108−@article{mcbride2008functional,

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

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

111−journal = {Journal of functional programming},

144+@article{Jones2003,

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

146+author = {Jones, Simon Peyton},

147+editor = {Jones, Simon Peyton},

148+isbn = {0521826144},

149+journal = {Language},

112150number = {1},

113−pages = {1--13},

114−publisher = {Cambridge Univ Press},

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

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

117−volume = {18},

118−year = {2008}

151+publisher = {Cambridge University Press},

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

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

154+volume = {13},

155+year = {2003}

119156}

120157@inproceedings{madhavapeddy2007melange,

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

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

124161number = {3},

125162pages = {101--114},

126163publisher = {ACM},

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

129166volume = {41},

130167year = {2007}

131168}

132−@inproceedings{lempsink2009type,

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

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

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

136−pages = {61--72},

137−publisher = {ACM},

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

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

140−year = {2009}

169+@inproceedings{czarnecki2004dsl,

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

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

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

173+pages = {51--72},

174+publisher = {Springer},

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

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

177+year = {2004}

141178}

142−@book{Approach2012,

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

144−booktitle = {Carcinogenesis},

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

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

147−isbn = {020161622X},

148−issn = {1460-2180},

149−number = {3},

150−pmid = {22383472},

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

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

153−volume = {33}

179+@article{Wadler2001,

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

181+author = {Wadler, Philip},

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

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

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

185+isbn = {3540594515},

186+issn = {03029743},

187+journal = {Advanced Functional Programming},

188+number = {August 1992},

189+pages = {24--52},

190+publisher = {Springer},

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

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

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

194+volume = {925},

195+year = {2001}

154196}

155−@inproceedings{stump2010resource,

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

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

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

159−pages = {27--38},

160−publisher = {ACM},

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

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

163−year = {2010}

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

204+@inproceedings{Taha2003,

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

206+booktitle = {Principles of Programming Languages},

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

222+pages = {NP},

223+pmid = {23150082},

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

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

226+volume = {52},

227+year = {2012}

164228}

165229@article{mcbride2010ornamental,

166230author = {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},

168232journal = {Journal of Functional Programming},

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

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

171235year = {2010}

172236}

173−@article{Swierstra2011,

174−author = {Swierstra, W},

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

176−journal = {Journal of Functional Programming},

177−number = {6},

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

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

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

181−volume = {21},

182−year = {2011}

237+@inproceedings{Gall2012,

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

239+booktitle = {SCMAT},

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

241+isbn = {9781450312950},

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

243+pages = {219--228},

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

245+year = {2012}

183246}

184−@article{McBride2002,

185−author = {McBride, C},

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

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

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

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

190−year = {2000}

247+@article{Campbell-moore,

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

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

250+pages = {1--10},

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

191252}

192−@article{Xi1998,

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

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

253+@misc{Resolution2012a,

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

249255doi = {10.1093/epirev/mxr031},

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

251−isbn = {9780321702081},

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

252257issn = {1478-6729},

253−number = {1},

254−pages = {NP},

255258pmid = {22215642},

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

257−volume = {34}

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

258260}

259−@inproceedings{ko2011modularising,

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

261−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic 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},

263−pages = {13--24},

264−publisher = {ACM},

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

267−year = {2011}

261+@inproceedings{Pasalic2002,

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

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

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

271+pages = {218--229},

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

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

274+volume = {37},

275+year = {2002}

268276}

269−@book{Choosing2012,

270−author = {Fowler, Martin},

271−booktitle = {Carcinogenesis},

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

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

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}

277+@book{Projects,

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

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

280+isbn = {020161622X},

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

281282}

282−@article{marlow2006making,

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

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−journal = {Journal of Functional Programming},

286−number = {4-5},

287−pages = {415--449},

288−publisher = {Cambridge University Press},

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

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

291−volume = {16},

292−year = {2006}

283+@inproceedings{Wadler1989,

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

285+author = {Wadler, Philip},

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

290+number = {June},

291+pages = {347--359},

292+publisher = {ACM},

293+series = {FPCA '89},

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

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

296+year = {1989}

293297}

294−@article{Mandelbaum2007,

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

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

297−doi = {10.1145/1190215.1190231},

298−isbn = {1595935754},

299−issn = {03621340},

300−journal = {SIGPLAN Not},

301−number = {1},

302−pages = {77--83},

298+@inproceedings{swierstra2007beauty,

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

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

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

302+pages = {25--36},

303303publisher = {ACM},

304−series = {POPL '07},

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

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

307−volume = {42},

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

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

308306year = {2007}

309307}

310−@article{Abel2010,

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

312−author = {Abel, Andreas},

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

314−journal = {EPTCS},

315−pages = {1--15},

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

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

318−volume = {43},

319−year = {2010}

308+@inproceedings{Xi1999,

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

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

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

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

319+pages = {214--227},

320+publisher = {ACM Press},

321+series = {POPL '99},

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

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

324+volume = {26},

325+year = {1999}

320326}

321−@article{Hoare1978,

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

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

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

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

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

327−isbn = {0131532715},

328−issn = {01676423},

329−journal = {Communications of the ACM},

330−number = {8},

331−pages = {666--677},

332−pmid = {2142694823583477576},

327+@inproceedings{Kimmell2012,

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

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

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

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

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

333+year = {2012}

334+}

335+@article{mccann2000packet,

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

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

338+number = {4},

339+pages = {321--333},

333340publisher = {ACM},

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

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

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

337−volume = {21},

338−year = {1978}

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

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

343+volume = {30},

344+year = {2000}

339345}

340−@book{Bird2010,

341−author = {Bird, Richard},

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

343−isbn = {9780521513388},

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

345−year = {2010}

346+@article{McBride2007,

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

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

349+journal = {Journal of functional programming},

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

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

352+year = {2007}

346353}

347−@inproceedings{oury2008power,

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

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

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

351−keywords = {Dependent Types},

352−mendeley-tags = {Dependent Types},

353−number = {9},

354−pages = {39--50},

355−publisher = {ACM},

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

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

358−volume = {43},

359−year = {2008}

354+@misc{Ferreira2012,

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.

356+

357+

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.

359+

360+

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

362+

363+

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.

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

381+year = {2012}

360382}

361−@inproceedings{madhavapeddy2010turning,

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

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

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

365−publisher = {USENIX Association},

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

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

368−year = {2010}

383+@misc{The2012b,

384+author = {Brooks, Fred},

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

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

387+isbn = {9780321702081},

388+issn = {1478-6729},

389+pmid = {22215642},

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

369391}

370392@book{peyton1987implementation,

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

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

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

375397year = {1987}

376398}

377−@inproceedings{Pasalic2002,

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

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

407+@inproceedings{Danielsson2010,

408+author = {Danielsson, Nils Anders},

379409booktitle = {International Conference on Functional Programming},

380−doi = {10.1145/583852.581499},

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

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

410+doi = {10.1145/1932681.1863585},

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

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

383413issn = {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},

385415month = sep,

386416number = {9},

387−pages = {218--229},

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

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

390−volume = {37},

391−year = {2002}

417+pages = {285},

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

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

420+volume = {45},

421+year = {2010}

392422}

393−@inproceedings{Brady2010,

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

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

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

397−isbn = {9781605587943},

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

423+@inproceedings{augustsson1999exercise,

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

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

426+keywords = {Depe},

427+mendeley-tags = {Depe},

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

399452mendeley-tags = {Dependent Types},

400−pages = {297--308},

401−publisher = {ACM},

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

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

404−year = {2010}

453+school = {University of Edinburgh},

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

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

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

471+year = {2012}

405472}

406473@inproceedings{Fournet2011,

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

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

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

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

412479year = {2010}

413480}

414−@article{landin1966next,

415−author = {Landin, P.J.},

416−file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Communications of the ACM/Landin - 1966 - The next 700 programming languages.pdf:pdf},

417−journal = {Communications of the ACM},

418−number = {3},

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

481+@inproceedings{chlipala2010ur,

482+author = {Chlipala, Adam},

483+booktitle = {ACM SIGPLAN Notices},

484+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

485+number = {6},

486+pages = {122--133},

431487publisher = {ACM},

432−title = {{Modular verification of security protocol code by typing}},

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

488+title = {{Ur: statically-typed metaprogramming with type-level record computation}},

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

434490volume = {45},

435491year = {2010}

436492}

437−@article{Haskell2012a,

438−author = {Biancuzzi, F and Warden, S},

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

440−file = {:Users/edwin/Documents/Mendeley Desktop/Biancuzzi, Warden/Unknown/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

441−isbn = {9780596801670},

442−issn = {1478-6729},

443−pmid = {22215642},

444−title = {{Masterminds of Programming Chapter 8}}

445−}

446−@book{Brady2012,

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

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

490−publisher = {Springer},

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}

493+@article{Fluet,

494+annote = {0,3

495+

496+

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.

498+

499+

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.

501+I think this would shorten the introduction and give a much better intuition for the rules.},

502+author = {Fluet, Matthew},

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

504+pages = {1--18},

505+title = {{A Type- and Control-Flow Analysis for System F}}

496506}

497−@article{Huet1997,

498−author = {Huet, G},

499−file = {:Users/edwin/Documents/Mendeley Desktop/Huet/{Journal of Functional Programming}/Huet - 1997 - The zipper.pdf:pdf},

507+@article{Vytiniotis2011,

508+author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},

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

500510journal = {{Journal of Functional Programming}},

501−number = {5},

502−pages = {549----554},

503−title = {{The zipper}},

504−url = {http://journals.cambridge.org/abstract_S0956796897002864},

505−volume = {7},

506−year = {1997}

511+number = {4--5},

512+pages = {333----412},

513+title = {{\textsc{OutsideIn}(X) Modular type inference with local assumptions}},

514+url = {http://journals.cambridge.org/abstract_S0956796811000098},

515+volume = {21},

516+year = {2011}

507517}

508518@inproceedings{Gregoire2005,

509519author = {Gregoire, Benjamin and Mahboubi, Assia},

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

512522pages = {98----113},

513523title = {{Proving Equalities in a Commutative Ring Done Right in Coq}},

514524url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.61.3041},

515525year = {2005}

516526}

517−@misc{Bloat,

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,

527+@book{Cryptography2012,

524528author = {Anderson, Ross},

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

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

529+doi = {10.1093/intimm/dxs023},

530+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 5.pdf:pdf},

527531isbn = {9780470068526},

528−issn = {1478-6729},

529−pmid = {22215642},

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

532+issn = {1460-2377},

533+number = {4},

534+pmid = {22451589},

535+title = {{Security Engineering Chapter 5}},

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

537+volume = {24}

531538}

532−@inproceedings{Augustsson1998,

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

534−author = {Augustsson, Lennart},

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

545+@inproceedings{oury2008power,

546+author = {Oury, N. and Swierstra, W.},

535547booktitle = {International Conference on Functional Programming},

536−doi = {10.1097/MEG.0b013e328342f213},

537−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/International Conference on Functional Programming/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

538−issn = {14735687},

539−keywords = {Depe,Dependent Types},

540−mendeley-tags = {Depe,Dependent Types},

548+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

549+keywords = {Dependent Types},

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

566+keywords = {Dependent Types},

567+mendeley-tags = {Dependent Types},

541568number = {1},

542−pages = {239--250},

543−pmid = {21139473},

544−publisher = {ACM Press},

545−title = {{Cayenne - a language with dependent types}},

546−url = {http://www.cs.chalmers.se/$\sim$augustss/cayenne/paper.ps},

547−volume = {23},

548−year = {1998}

569+pages = {69--111},

570+publisher = {Cambridge University Press},

571+title = {{The view from the left}},

572+url = {http://www.journals.cambridge.org/abstract_S0956796803004829},

573+volume = {14},

574+year = {2004}

549575}

550−@book{Hunt,

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

552−booktitle = {Design},

553−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Design/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},

554−isbn = {020161622X},

555−title = {{The Pragmatic Programmer Chapter 4}}

576+@book{Cryptography2012a,

577+author = {Pfleeger, Charles P and Pfleeger, S. L.},

578+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

579+doi = {10.1093/ntr/nts035},

580+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 2.pdf:pdf},

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}

556591}

557−@article{burrows1990,

558−author = {Burrows, Michael and Abadi, Martin and Needham, Roger},

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

560−journal = {ACM Transactions on Computer Systems},

561−pages = {18----36},

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}

592+@phdthesis{Pretnar2010,

593+author = {Pretnar, Matija},

594+file = {:Users/edwin/Downloads/the-logic-and-handling-of-algebraic-effects.pdf:pdf},

595+school = {University of Edinburgh},

596+title = {{The Logic and Handling of Algebraic Effects}},

597+year = {2010}

566598}

567−@inproceedings{atkey2009unembedding,

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

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

570−pages = {37--48},

599+@inproceedings{Brady2010,

600+author = {Brady, Edwin and Hammond, Kevin},

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

606+pages = {297--308},

571607publisher = {ACM},

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

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

574−year = {2009}

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

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

610+year = {2010}

575611}

576−@inproceedings{Brady2011a,

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

578−author = {Brady, Edwin},

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

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}

612+@misc{Danielsson2002,

613+author = {Danielsson, Nils Anders and Altenkirch, Thorsten},

614+file = {:Users/edwin/Downloads/Papers/danielsson-altenkirch-subtyping.pdf:pdf},

615+title = {{Subtyping, Declaratively}},

616+year = {2002}

590617}

591−@inproceedings{gibbons2011modularising,

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

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

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

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

596−year = {2011}

618+@book{Strings2012,

619+author = {Sedgewick, Robert and Wayne, Kevin},

620+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

621+doi = {10.1093/ntr/nts035},

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

632+year = {2012}

597633}

598−@book{An2012,

599−author = {Fowler, Martin},

600−booktitle = {Carcinogenesis},

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

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

603−isbn = {9780132107549},

604−issn = {1460-2180},

605−number = {3},

606−pmid = {22383472},

607−title = {{Domain Specific Languages Chapter 1}},

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

609−volume = {33}

634+@inproceedings{Augustsson1985,

635+address = {Berlin, Heidelberg},

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

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

687+file = {:Users/edwin/Downloads/Safari/AlgorithmsFourthEditionChapterFourGraphs.pdf:pdf},

688+isbn = {9780132762571},

689+issn = {1758-5341},

690+month = dec,

691+number = {6},

692+pages = {NP},

693+pmid = {23150082},

694+title = {{Algorithms Chapter 4}},

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

709+volume = {34}

610710}

611711@inproceedings{coquand1986analysis,

612712author = {Coquand, T.},

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

615715pages = {227----246},

616716title = {{An analysis of Girard's paradox}},

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

618718year = {1986}

619719}

620−@misc{altenkirch2008nσ,

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

622−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Oury/Unknown/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},

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

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

720+@book{Harper2012,

721+author = {Harper, Robert},

722+file = {:Users/edwin/Downloads/pfpl.pdf:pdf},

723+title = {{Practical Foundations for Programming Languages}},

657724year = {2012}

658725}

659−@book{luo1994,

660−author = {Luo, Z.},

661−publisher = {Oxford University Press, Inc.},

662−title = {{Computation and reasoning: a type theory for computer science}},

663−url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},

664−year = {1994}

726+@misc{dagand2011transporting,

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

728+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

729+title = {{Transporting Functions across Ornaments}},

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

731+year = {2011}

665732}

666−@phdthesis{norell2007thesis,

667−author = {Norell, Ulf},

668−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Unknown/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},

669−keywords = {Dependent Types},

670−mendeley-tags = {Dependent Types},

671−publisher = {Citeseer},

672−school = {Chalmers University of Technology},

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

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

675−year = {2007}

733+@article{Abel2010,

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

735+author = {Abel, Andreas},

736+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},

737+journal = {EPTCS},

738+pages = {1--15},

739+title = {{MiniAgda: Integrating Sized and Dependent Types}},

740+url = {http://arxiv.org/abs/1012.4896},

741+volume = {43},

742+year = {2010}

676743}

677−@inproceedings{Brady2006b,

678−author = {Brady, Edwin},

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

680−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Implementation and Application of Functional Languages ({IFL}'06)/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

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

682−month = sep,

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

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

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

686−year = {2006}

744+@article{burrows1990,

745+author = {Burrows, Michael and Abadi, Martin and Needham, Roger},

746+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

747+journal = {ACM Transactions on Computer Systems},

748+pages = {18----36},

749+title = {{A logic of authentication}},

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

751+volume = {8},

752+year = {1990}

687753}

688−@inproceedings{chlipala2010ur,

689−author = {Chlipala, Adam},

690−booktitle = {ACM SIGPLAN Notices},

691−file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/ACM SIGPLAN Notices/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

692−number = {6},

693−pages = {122--133},

694−publisher = {ACM},

695−title = {{Ur: statically-typed metaprogramming with type-level record computation}},

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

697−volume = {45},

754+@article{loh2010tutorial,

755+author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},

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

757+journal = {Fundamenta Informaticae},

758+number = {2},

759+pages = {177--207},

760+publisher = {IOS Press},

761+title = {{A tutorial implementation of a dependently typed lambda calculus}},

762+url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},

763+volume = {102},

698764year = {2010}

699765}

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

700784@misc{Abadi1997,

701785author = {Abadi, Martin and Gordon, Andrew D},

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

704788pages = {36 -- 47},

705789title = {{A calculus for cryptographic protocols: The spi calculus}},

706790url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},

707791year = {1997}

708792}

709−@inproceedings{McBride2006,

710−author = {McBride, C and Goguen, H and McKinna, J},

711−booktitle = {Types for Proofs and Programs {(TYPES 2006)}},

712−title = {{A few constructions on constructors}},

713−url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},

714−year = {2006}

793+@article{Haskell2012a,

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

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

796+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

797+isbn = {9780596801670},

798+issn = {1478-6729},

799+pmid = {22215642},

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

715801}

716−@article{Jones2003,

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

718−author = {Jones, Simon Peyton},

719−editor = {Jones, Simon Peyton},

720−isbn = {0521826144},

721−journal = {Language},

722−number = {1},

723−publisher = {Cambridge University Press},

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

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

726−volume = {13},

802+@inproceedings{madhavapeddy2010turning,

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

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

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

806+publisher = {USENIX Association},

807+title = {{Turning down the LAMP: software specialisation for the cloud}},

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

809+year = {2010}

810+}

811+@misc{Braßel,

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

727838year = {2003}

728839}

729−@inproceedings{Visser2008,

730−author = {Visser, E},

731−booktitle = {Generative and Transformational Techniques in Software Engineering},

732−title = {{WebDSL: A case study in domain-specific language engineering}},

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

840+@book{An2012,

841+author = {Fowler, Martin},

842+booktitle = {Carcinogenesis},

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

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

734871year = {2008}

735872}

736−@inproceedings{ko2011modularising,

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

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

739−pages = {13--24},

740−publisher = {ACM},

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

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

743−year = {2011}

873+@misc{Silkensen2012,

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.

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

896+pages = {1--12},

897+title = {{Well-typed Islands Parse Faster}},

898+year = {2012}

744899}

745−@misc{Attacks2012a,

746−author = {Anderson, Ross},

900+@misc{The2012c,

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

747902doi = {10.1093/epirev/mxr031},

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

749−isbn = {9780470068526},

903+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

904+isbn = {9780596529833},

750905issn = {1478-6729},

751−number = {1},

752−pages = {NP},

753906pmid = {22215642},

754−title = {{Security Engineering Chapter 18}},

755−volume = {34}

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

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}

756960}

757961@inproceedings{l,

758962author = {L\"{a}mmel, R. and Jones, S.P.},

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

761965number = {3},

762966pages = {26--37},

763967publisher = {ACM},

@@ -766,213 +970,303 @@ url = {http://dl.acm.org/citation.cfm?id=640136.604179},

766970volume = {38},

767971year = {2003}

768972}

769−@inproceedings{Delahaye2000,

770−author = {Delahaye, D},

771−booktitle = {Logic for Programming and Automated Reasoning},

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

773−pages = {85----95},

774−publisher = {Springer},

775−title = {{A tactic language for the system Coq}},

776−url = {http://www.springerlink.com/index/EFQAH8J88K42VN8T.pdf},

777−year = {2000}

973+@phdthesis{Okasaki1996,

974+author = {Okasaki, Chris},

975+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},

976+school = {Carnegie Mellon University},

977+title = {{Purely Functional Data Structures}},

978+year = {1996}

778979}

779−@misc{pollack1997believe,

780−author = {Pollack, R.},

781−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Unknown/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},

782−title = {{How to believe a machine-checked proof}},

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

784−year = {1997}

980+@inproceedings{McBride2004b,

981+author = {McBride, Conor and McKinna, James},

982+booktitle = {Haskell Workshop},

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

984+title = {{I am not a number : I am a free variable}},

985+year = {2004}

785986}

786−@book{Bertot2004,

787−author = {Bertot, Yves and Cast\'{e}ran, Pierre},

987+@inproceedings{Brady2005a,

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

7881008publisher = {Springer},

789−title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},

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

1009+title = {{A gentle introduction to multi-stage programming}},

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

7911011year = {2004}

7921012}

793−@inproceedings{brady2011epic,

794−author = {Brady, Edwin},

795−booktitle = {Trends in Functional Programming ({TFP}’11)},

796−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Trends in Functional Programming ({TFP}’11)/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},

797−title = {{Epic --- A Library for Generating Compilers}},

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

799−year = {2011}

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

1050+author = {Rose, Eva},

1051+file = {:Users/edwin/Downloads/Papers/padl2013_submission_33.pdf:pdf},

1052+keywords = {constraints,language design,mon-,privacy policy,semantics},

1053+title = {{Declarative implementation aspects of privacy policy effects}}

8001054}

801−@article{dybjer1994inductive,

802−author = {Dybjer, P.},

803−journal = {Formal aspects of computing},

804−number = {4},

805−pages = {440--465},

1055+@inproceedings{morris2006exploring,

1056+author = {Morris, P. and Altenkirch, T. and McBride, C.},

1057+booktitle = {Types for Proofs and Programs},

1058+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

1059+pages = {252--267},

8061060publisher = {Springer},

807−title = {{Inductive families}},

808−url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},

809−volume = {6},

1061+title = {{Exploring the regular tree types}},

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

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

8101082year = {1994}

8111083}

812−@inproceedings{McBride2004b,

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

814−booktitle = {Haskell Workshop},

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

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

817−year = {2004}

1084+@misc{Hancock,

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

1086+file = {:Users/edwin/Downloads/10.1.1.25.9367.pdf:pdf},

1087+keywords = {dependent types,functional programming,interac-,monadic i,o,reactive programming,refinement,repetition constructs,tion},

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

1089+year = {2000}

8181090}

819−@article{Wadler2001,

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

821−author = {Wadler, Philip},

822−doi = {10.1007/3-540-59451-5_2},

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}

1091+@book{Chlipala2012,

1092+author = {Chlipala, Adam},

1093+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chlipala - 2012 - Certified Programming with Dependent Types.pdf:pdf},

1094+title = {{Certified Programming with Dependent Types}},

1095+year = {2012}

8361096}

837−@inproceedings{taha1997multi,

838−author = {Taha, W. and Sheard, T.},

839−booktitle = {ACM SIGPLAN Notices},

840−number = {12},

841−pages = {203--217},

1097+@article{Mandelbaum2007,

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

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

1104+number = {1},

1105+pages = {77--83},

8421106publisher = {ACM},

843−title = {{Multi-stage programming with explicit annotations}},

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

845−volume = {32},

846−year = {1997}

1107+series = {POPL '07},

1108+title = {{PADS/ML: a functional data description language}},

1109+url = {http://doi.acm.org/10.1145/1190216.1190231},

1110+volume = {42},

1111+year = {2007}

8471112}

848−@article{loh2010tutorial,

849−author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},

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

851−journal = {Fundamenta Informaticae},

852−number = {2},

853−pages = {177--207},

854−publisher = {IOS Press},

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}

1113+@article{Nabais2008,

1114+author = {Nabais, Davide},

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

1116+journal = {Most},

1117+pages = {1--5},

1118+title = {{DesCo : a Web Based Information System for Descriptional Complexity of Formal Languages}},

1119+year = {2008}

8591120}

860−@book{Philosophy2012,

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

862−booktitle = {Carcinogenesis},

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

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

865−isbn = {020161622X},

866−issn = {1460-2180},

867−number = {3},

868−pmid = {22383472},

869−title = {{The Pragmatic Programmer Chapter 1}},

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

871−volume = {33}

1121+@book{Edition2012,

1122+author = {Pfleeger, Charles P and Pfleeger, S. L.},

1123+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

1124+doi = {10.1093/ntr/nts035},

1125+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 1.pdf:pdf},

1126+isbn = {0132390779},

1127+issn = {1469-994X},

1128+month = oct,

1129+number = {10},

1130+pages = {NP},

1131+pmid = {23012339},

1132+title = {{Security in Computing Chapter 1}},

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

1134+volume = {14},

1135+year = {2012}

8721136}

873−@inproceedings{pollack1990implicit,

874−author = {Pollack, R.},

875−booktitle = {{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}},

876−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}/Pollack - 1990 - Implicit syntax.pdf:pdf},

877−publisher = {Citeseer},

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}

1137+@book{Eap,

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

1139+file = {:Users/edwin/Downloads/Safari/TCPIPIllustratedVolume1TheProtocolsSecondEditionChapter18SecurityEAPIPs.pdf:pdf},

1140+isbn = {9780132808200},

1141+title = {{TCP/IP Illustrated Chapter 18}}

8811142}

882−@article{gordon2003authenticity,

883−author = {Gordon, A.D. and Jeffrey, A.},

884−file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Journal of computer security/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

885−journal = {Journal of computer security},

886−number = {4},

887−pages = {451--520},

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}

1143+@book{Fowler,

1144+author = {Fowler, Martin},

1145+booktitle = {Language},

1146+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},

1147+isbn = {9780132107549},

1148+title = {{Domain Specific Languages Chapter 2}}

8931149}

894−@inproceedings{Wadler1989,

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

896−author = {Wadler, Philip},

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

898−doi = {10.1145/99370.99404},

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

900−isbn = {0897913280},

901−number = {June},

902−pages = {347--359},

903−publisher = {ACM},

904−series = {FPCA '89},

905−title = {{Theorems for free!}},

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

907−year = {1989}

1150+@book{Brady2012e,

1151+author = {Seibel, Peter},

1152+booktitle = {The Gerontologist},

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

1154+file = {:Users/edwin/Downloads/Safari/CodersatWorkReflectionsontheCraftofProgrammingChapter9GuySteele.pdf:pdf},

1155+isbn = {9781430219484},

1156+issn = {1758-5341},

1157+month = dec,

1158+number = {6},

1159+pages = {NP},

1160+pmid = {23150082},

1161+title = {{Coders at Work Chapter 9}},

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

1163+volume = {52},

1164+year = {2012}

9081165}

909−@inproceedings{Augustsson1985,

910−address = {Berlin, Heidelberg},

911−author = {Augustsson, Lennart},

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

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

914−editor = {Jouannaud, Jean-Pierre},

915−isbn = {978-3-540-15975-9},

916−keywords = {Computer Science},

917−pages = {368----381},

918−publisher = {Springer Berlin Heidelberg},

919−series = {Lecture Notes in Computer Science},

920−title = {{Compiling Pattern Matching}},

921−url = {http://www.springerlink.com/content/y647423656557505/},

922−volume = {201},

923−year = {1985}

1166+@article{Regular2012,

1167+author = {Kernighan, Brian},

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

1169+file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter1ARegularExpressio.pdf:pdf},

1170+isbn = {9780596510046},

1171+issn = {1758-5341},

1172+month = dec,

1173+number = {6},

1174+pages = {NP},

1175+pmid = {23150082},

1176+title = {{Beautiful Code Chapter 1}},

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

1178+volume = {52},

1179+year = {2012}

9241180}

925−@inproceedings{Brady2005a,

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

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

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

1181+@inproceedings{norell2009dependently,

1182+author = {Norell, Ulf},

1183+booktitle = {Advanced Functional Programming},

1184+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

9291185keywords = {Dependent Types},

9301186mendeley-tags = {Dependent Types},

931−title = {{A dependently typed framework for static analysis of program execution costs}},

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

933−year = {2005}

1187+pages = {230--266},

1188+publisher = {Springer},

1189+title = {{Dependently typed programming in Agda}},

1190+url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

1191+year = {2009}

9341192}

935−@article{Vytiniotis2011,

936−author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, 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},

938−journal = {{Journal of Functional Programming}},

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,

1221+author = {Vytiniotis, D and {Peyton Jones}, Simon and Shrijvers, Tom and Sulzmann, Martin},

1222+file = {:Users/edwin/Downloads/jfp-outsidein.pdf:pdf},

1223+journal = {Journal of Functional Programming},

9391224number = {4--5},

9401225pages = {333----412},

941−title = {{\textsc{OutsideIn}(X) Modular type inference with local assumptions}},

942−url = {http://journals.cambridge.org/abstract_S0956796811000098},

1226+title = {{OutsideIn (X) Modular type inference with local assumptions}},

1227+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},

9431228volume = {21},

9441229year = {2011}

9451230}

946−@article{mccann2000packet,

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

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

949−number = {4},

950−pages = {321--333},

1231+@inproceedings{fisher2005pads,

1232+author = {Fisher, K. and Gruber, R.},

1233+booktitle = {ACM SIGPLAN Notices},

1234+number = {6},

1235+pages = {295--304},

9511236publisher = {ACM},

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

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

954−volume = {30},

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}

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

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

1239+volume = {40},

1240+year = {2005}

9641241}

965−@inproceedings{norell2009dependently,

966−author = {Norell, Ulf},

967−booktitle = {Advanced Functional Programming},

968−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Advanced Functional Programming/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

969−keywords = {Dependent Types},

1242+@inproceedings{Levitation2010,

1243+author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

1244+booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},

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

1249+keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

9701250mendeley-tags = {Dependent Types},

971−pages = {230--266},

972−publisher = {Springer},

973−title = {{Dependently typed programming in Agda}},

974−url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

975−year = {2009}

1251+month = sep,

1252+number = {9},

1253+title = {{The gentle art of levitation}},

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

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}

9761270}

9771271@article{Hughes1989,

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

9801274chapter = {2},

9811275doi = {10.1093/comjnl/32.2.98},

9821276editor = {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},

9841278institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},

9851279isbn = {0201172364},

9861280issn = {00104620},

@@ -993,57 +1287,393 @@ url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},

9931287volume = {32},

9941288year = {1989}

9951289}

996−@article{Steiner1988,

997−author = {Steiner, JG},

998−file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Proc. Winter USENIX Conference/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

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

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

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

1002−year = {1988}

1290+@article{Brady2006a,

1291+author = {Brady, E and Hammond, K},

1292+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

1293+journal = {\ldots of the 5th international conference on \ldots},

1294+keywords = {Dependent Types},

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

1298+year = {2006}

10031299}

1004−@phdthesis{McBride1999,

1005−author = {McBride, Conor},

1006−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Unknown/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

1300+@article{Xi1998,

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

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

10071308keywords = {Dependent Types},

10081309mendeley-tags = {Dependent Types},

1009−school = {University of Edinburgh},

1010−title = {{Dependently typed functional programs and their proofs}},

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

1012−year = {1999}

1310+number = {5},

1311+pages = {249--257},

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

1317+year = {1998}

10131318}

1014−@inproceedings{augustsson1999exercise,

1015−author = {Augustsson, L. and Carlsson, M.},

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

1017−keywords = {Depe},

1018−mendeley-tags = {Depe},

1019−publisher = {Citeseer},

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

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

1022−year = {1999}

1319+@inproceedings{Abel2013,

1320+author = {Abel, Andreas and Pientka, Brigitte and Thibodeau, David and Setzer, Anton},

1321+booktitle = {Principles of Programming Languages},

1322+file = {:Users/edwin/Downloads/popl13.pdf:pdf},

1323+isbn = {9781450318327},

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

1325+title = {{Copatterns: Programming Infinite Structures by Observations}},

1326+year = {2013}

10231327}

1024−@inproceedings{taha2004gentle,

1025−author = {Taha, W.},

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

1027−pages = {30--50},

1028−publisher = {Springer},

1029−title = {{A gentle introduction to multi-stage programming}},

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

1031−year = {2004}

1328+@misc{pollack1997believe,

1329+author = {Pollack, R.},

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

1344+pages = {NP},

1345+pmid = {23150082},

1346+title = {{Algorithms Chapter 3}},

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

1379+year = {2012}

10321380}

10331381@inproceedings{Sculthorpe2009,

10341382author = {Sculthorpe, Neil and Nilsson, Henrik},

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

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

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

10391387year = {2009}

10401388}

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

10411671@misc{TheMendeleySupportTeam2011a,

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

10431673address = {London},

10441674author = {{The Mendeley Support Team}},

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

10471677keywords = {Mendeley,how-to,user manual},

10481678pages = {1--16},

10491679publisher = {Mendeley Ltd.},

@@ -1051,35 +1681,21 @@ title = {{Getting Started with Mendeley}},

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

10521682year = {2011}

10531683}

1054−@article{danielsson2011parsing,

1055−author = {Danielsson, N. and Norell, U.},

1056−journal = {Implementation and Application of Functional Languages},

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

1074−isbn = {9780132107549},

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

1684+@misc{Brady2012b,

1685+author = {Brooks, Fred},

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

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

1688+isbn = {9780321702081},

1689+issn = {1478-6729},

1690+pmid = {22215642},

1691+title = {{The Design of Design Chapter 2}}

10761692}

10771693@misc{Bove2008,

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

10791695author = {Bove, Ana and Dybjer, Peter},

10801696booktitle = {Notes},

10811697doi = {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},

10831699number = {February},

10841700pages = {57--99},

10851701publisher = {Springer},

@@ -1088,111 +1704,367 @@ url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},

10881704volume = {5520},

10891705year = {2008}

10901706}

1091−@article{Okasaki1993,

1092−author = {Okasaki, Chris},

1093−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Journal of functional programming/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

1094−journal = {Journal of functional programming},

1095−title = {{Red-Black Trees in A Functional Setting}},

1096−year = {1993}

1707+@article{In2012,

1708+author = {Gulhati, Ashish},

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

1710+file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter11SecureCommunicati.pdf:pdf},

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

1720+year = {2012}

10971721}

1098−@inproceedings{pj2006gadts,

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

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

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

1102−number = {9},

1103−pages = {50--61},

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

1730+@inproceedings{lempsink2009type,

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

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

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

1734+pages = {61--72},

11041735publisher = {ACM},

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

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

1107−volume = {41},

1108−year = {2006}

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

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

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

1753+year = {2011}

11091754}

11101755@misc{altenkirch2005dependent,

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

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

11141759title = {{Why dependent types matter}},

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

11161761year = {2005}

11171762}

1118−@misc{The2012c,

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

1763+@misc{Nodes2012a,

1764+author = {Brooks, Fred},

11201765doi = {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},

1122−isbn = {9780596529833},

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

1767+isbn = {9780321702081},

11231768issn = {1478-6729},

11241769pmid = {22215642},

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

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

11261771}

1127−@misc{Resolution2012a,

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

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

1130−file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Unknown/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

1131−issn = {1478-6729},

1132−pmid = {22215642},

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

1772+@article{danielsson2011parsing,

1773+author = {Danielsson, N. and Norell, U.},

1774+journal = {Implementation and Application of Functional Languages},

1775+pages = {80--99},

1776+publisher = {Springer},

1777+title = {{Parsing mixfix operators}},

1778+url = {http://www.springerlink.com/index/386243257W504252.pdf},

1779+year = {2011}

11341780}

1135−@article{Brady2006a,

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

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

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

1139−keywords = {Dependent Types},

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}

1781+@book{Bird2010,

1782+author = {Bird, Richard},

1783+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},

1784+isbn = {9780521513388},

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

1786+year = {2010}

11441787}

1145−@inproceedings{swierstra2007beauty,

1146−author = {Swierstra, W. and Altenkirch, T.},

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

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

1149−pages = {25--36},

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

1822+@inproceedings{stump2010resource,

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

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

1825+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

1826+pages = {27--38},

11501827publisher = {ACM},

1151−title = {{Beauty in the beast}},

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

1153−year = {2007}

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

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

1830+year = {2010}

11541831}

1155−@article{McBride2004a,

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

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

1158−doi = {10.1017/S0956796803004829},

1159−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/Journal of Functional Programming/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

1160−issn = {09567968},

1832+@article{fisher2006next,

1833+author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},

1834+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},

1835+journal = {Journal of the ACM},

1836+number = {2},

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

11611903journal = {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},

11621948keywords = {Dependent Types},

11631949mendeley-tags = {Dependent Types},

1164−number = {1},

1165−pages = {69--111},

1166−publisher = {Cambridge University Press},

1167−title = {{The view from the left}},

1168−url = {http://www.journals.cambridge.org/abstract_S0956796803004829},

1169−volume = {14},

1170−year = {2004}

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

1964+pages = {81--92},

1965+title = {{The size-change principle for program termination}},

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

1967+volume = {36},

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

11711975}

1172−@misc{Nodes2012a,

1173−author = {Brooks, Fred},

1976+@misc{Caldwell,

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

11742000doi = {10.1093/epirev/mxr031},

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

1176−isbn = {9780321702081},

2001+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},

2002+isbn = {9780470068526},

11772003issn = {1478-6729},

2004+number = {1},

2005+pages = {NP},

11782006pmid = {22215642},

1179−title = {{The Design of Design Chapter 3}}

2007+title = {{Security Engineering Chapter 18}},

2008+volume = {34}

11802009}

1181−@inproceedings{Hancock2000,

1182−author = {Hancock, Peter and Setzer, Anton},

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

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

1185−isbn = {3-540-67895-6},

1186−month = aug,

1187−pages = {317--331},

1188−title = {{Interactive Programs in Dependent Type Theory}},

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

1190−year = {2000}

2010+@inproceedings{bhargavan2010modular,

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

2012+booktitle = {ACM Sigplan Notices},

2013+number = {1},

2014+pages = {445--456},

2015+publisher = {ACM},

2016+title = {{Modular verification of security protocol code by typing}},

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

2018+volume = {45},

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}

11912063}

11922064@inproceedings{augustsson2008paradise,

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

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

11962068number = {9},

11972069pages = {225--228},

11982070publisher = {ACM},

@@ -1201,61 +2073,185 @@ url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},

12012073volume = {43},

12022074year = {2008}

12032075}

1204−@misc{Abel1998,

1205−author = {Abel, Andreas},

1206−booktitle = {Language},

1207−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Language/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

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

1209−year = {1998}

2076+@article{marlow2006making,

2077+author = {Marlow, S. and {Peyton Jones}, S.},

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

2079+journal = {Journal of Functional Programming},

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

2086+year = {2006}

12102087}

1211−@article{Jones1999,

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

1213−author = {Jones, Mark P},

1214−journal = {October},

1215−publisher = {Citeseer},

1216−title = {{Typing Haskell in Haskell}},

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

2088+@misc{TheMendeleySupportTeam2011b,

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

2090+address = {London},

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

2092+booktitle = {Mendeley Desktop},

2093+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf: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},

12182198year = {1999}

12192199}

1220−@inproceedings{morris2006exploring,

1221−author = {Morris, P. and Altenkirch, T. and McBride, C.},

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

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

1224−pages = {252--267},

1225−publisher = {Springer},

1226−title = {{Exploring the regular tree types}},

1227−url = {http://www.springerlink.com/index/f9p1317716614834.pdf},

1228−year = {2006}

2200+@article{Altenkirch2010a,

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

2202+author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},

2203+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},

2204+journal = {Citeseer},

2205+publisher = {Citeseer},

2206+title = {{Generic Programming with Dependent Types}},

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

2208+year = {2010}

12292209}

1230−@inproceedings{Sheard2005,

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

1232−author = {Sheard, Tim},

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

1234−doi = {10.1145/1088348.1088356},

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

1236−isbn = {159593071X},

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

1238−month = sep,

1239−pages = {74--85},

1240−publisher = {ACM Press},

1241−title = {{Putting curry-howard to work}},

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

1243−year = {2005}

2210+@book{Edition2012a,

2211+author = {Pfleeger, Charles P and Pfleeger, S. L.},

2212+booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

2213+doi = {10.1093/ntr/nts035},

2214+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computer Chapter 12.pdf:pdf},

2215+isbn = {0132390779},

2216+issn = {1469-994X},

2217+month = oct,

2218+number = {10},

2219+pages = {NP},

2220+pmid = {23012339},

2221+title = {{Security in Computer Chapter 12}},

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

2223+volume = {14},

2224+year = {2012}

12442225}

1245−@misc{Interface2012a,

1246−author = {Kreibich, Jay A.},

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

1248−file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Unknown/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

1249−isbn = {9781449394592},

1250−issn = {1478-6729},

1251−pmid = {22215642},

1252−title = {{Using SQLite Chapter 7}}

2226+@book{Pierce2004,

2227+author = {Pierce, Benjamin},

2228+editor = {Pierce, Benjamin},

2229+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pierce - 2004 - Advanced topics in types and programming languages.pdf:pdf},

2230+publisher = {MIT Press},

2231+title = {{Advanced topics in types and programming languages}},

2232+year = {2004}

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

12532249}

12542250@book{The2012,

12552251author = {Hunt, Andrew and Thomas, David},

12562252booktitle = {Carcinogenesis},

12572253doi = {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},

12592255isbn = {020161622X},

12602256issn = {1460-2180},

12612257number = {3},

@@ -1264,68 +2260,18 @@ title = {{The Pragmatic Programmer Chapter 3}},

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

12652261volume = {33}

12662262}

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,

1277−author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

1278−booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},

1279−doi = {10.1145/1932681.1863547},

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

1281−isbn = {978-1-60558-794-3},

1282−issn = {03621340},

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}

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}

2263+@inproceedings{pollack1990implicit,

2264+author = {Pollack, R.},

2265+booktitle = {{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}},

2266+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pollack - 1990 - Implicit syntax.pdf:pdf},

2267+publisher = {Citeseer},

2268+title = {{Implicit syntax}},

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

2270+year = {1990}

13202271}

1321−@inproceedings{fisher2005pads,

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

1323−booktitle = {ACM SIGPLAN Notices},

1324−number = {6},

1325−pages = {295--304},

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}

2272+@article{Bradya,

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

2274+file = {:Users/edwin/Downloads/Safari/ThePragmaticProgrammerFromJourneymantoMasterChapter7BeforetheProject.pdf:pdf},

2275+isbn = {020161622X},

2276+title = {{The Pragmatic Programmer Chapter 7}}

13312277}

papers/impl-paper/macros.ltx+2−2

@@ -391,7 +391,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

391391

392392%%%%%%%%%%%% TYPE

393393

394−\newcommand{\Type}{\mbox{\texttt{Set}}} %\star}

394+\newcommand{\Type}{\mbox{\texttt{Type}}} %\star}

395395

396396

397397%%%%%%%%%%%%% ARROWS

@@ -559,7 +559,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

559559\newcommand{\VectRebuild}{\FN{vectRebuild}}

560560

561561\newcommand{\Prop}{\TC{Prop}}

562−\newcommand{\Set}{\TC{Set}}

562+\newcommand{\Set}{\TC{Type}}

563563\newcommand{\CoqType}{\TC{Type}}

564564

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

2828

2929The function space $\all{\vx}{\vS}\SC\vT$ may also be written as $(\vx\Hab\vS)\to\vT$,

3030or $\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

3232inferred by the machine~\cite{pollack1990implicit}.

3333

3434\FFIG{

@@ -73,8 +73,14 @@ $\LET$ binding:

7373\DM{

7474\Axiom{\proves\RW{valid}}

7575\hg

76−\Rule{\Gamma\proves\RW{valid}}

77−{\Gamma;\vb\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}

83+{\Gamma;\LET\:\vx\:\defq\:\vs\Hab\vS\proves\RW{valid}}

7884}

7985

8086\subsubsection{Evaluation}

@@ -97,7 +103,7 @@ The following contextual closure rule reduces a $\LET$ binding by creating

97103a $\delta$-reducible expression:

98104

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

101107{\Gamma\proves\LET\:\vx\defq\vs\Hab\vS\SC\vt\leadsto\vu}

102108}

103109

@@ -256,10 +262,10 @@ sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):

256262}

257263}

258264

259−Constructors may take recursive arguments in the family

260−$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---

261−if such indices do not involve $\TC{T}$ then the constructor is

262−\demph{strictly positive}, which ensures that recursive arguments of the

265+Constructors may take recursive arguments in the family $\TC{T}$, which may be

266+higher order. Higher order recursive arguments may be computed from any type

267+which does not involve $\TC{T}$ itself. This restriction is known as

268+\demph{strict positivity} and ensures that recursive arguments of the

263269constructor are structurally smaller than the value itself.

264270

265271For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:

@@ -526,7 +532,7 @@ algorithm:

526532

527533\begin{SaveVerbatim}{vAddImpSolve}

528534

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

530536vAdd a O c (Nil a) (Nil a) = Nil a

531537vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)

532538 = (::) a k ((+) c x y) (vAdd a k c xs ys)

@@ -541,17 +547,17 @@ switching to \TT{} notation from the ASCII \Idris{} syntax.

541547\FFIG{

542548\AR{

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

545551 \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\

546552\end{array}

547553\\

548554\begin{array}{lccccccc}

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

551557\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\

552558\multicolumn{5}{l}{

553559\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,\\

555561\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;

556562\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk

557563\SC

@@ -580,18 +586,20 @@ programming and theorem proving with dependent types, and appropriate mechanisms

580586constructing programs and theorems:

581587

582588\begin{itemize}

583−\item \remph{Pattern matching} is a convenient abstraction for humans to write programs,

584−in that it allows a programmer to express exactly the computational behaviour of a function.

585−\item \remph{Tactics}, such as those used in the Coq theorem prover~\cite{Bertot2004},

586−are a convenient abstraction for building proofs and programs by \remph{refinement}.

589+\item \remph{Pattern matching} is a convenient abstraction for humans to write

590+programs, in that it allows a programmer to express exactly the computational

591+behaviour of a function.

592+\item \remph{Tactics}, such as those used in the Coq theorem

593+prover~\cite{Bertot2004}, are a convenient abstraction for building proofs and

594+programs by \remph{refinement}.

587595\end{itemize}

588596

589−The idea behind the \Idris{} elaborator, therefore, is to use the high level program

590−to direct \demph{tactics} to build \TT{} programs by refinement. The

591−elaborator is implemented as an Embedded Domain Specific Language (EDSL) in Haskell.

592−The remainder

593−of this paper describes the EDSL and demonstrates how it is used to implement

594−all of the high level features of \Idris{}.

597+The idea behind the \Idris{} elaborator, therefore, is to use the high level

598+program to direct \demph{tactics} to build \TT{} programs by refinement. The

599+elaborator is implemented as a Haskell monad capturing proof state, with a

600+collection of tactics for updating and refining the proof state. The remainder

601+of this paper describes this elaborator and demonstrates how it is used to

602+implement the high level features of \Idris{}.

595603

596604

597605

src/Core/CaseTree.hs+1−1

@@ -79,7 +79,7 @@ instance TermSize CaseAlt where

7979small :: Name -> [Name] -> SC -> Bool

8080small n args t = let as = findAllUsedArgs t args in

8181 length as == length (nub as) &&

82− termsize n t < 20

82+ termsize n t < 5

8383

8484namesUsed :: SC -> [Name]

8585namesUsed 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)

153153 collapseCons n cons

154154 updateContext (addDatatype (Data n ttag cty cons))

155155 mapM_ (checkPositive n) cons

156− where findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]

156+ where

157+ -- parameters are names which are unchanged across the structure,

158+ -- which appear exactly once in the return type of a constructor

159+ findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]

157160 findParams ps [] = mapMaybe (\ ((x, y), n) ->

158161 if y then Just n else Nothing)

159162 (zip ps [0..])

160163 findParams ps (t : ts) = findParams (updateParams ps t) ts

161164

162165 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

164167 updateParams ps tm@(App f a)

165168 | (P _ fn _, args) <- unApply tm

166169 = if fn == n

167− then updateParamsA ps args

170+ then updateParamsA ps args (tail args)

168171 else updateParams (updateParams ps f) a

169172 | otherwise = updateParams (updateParams ps f) a

170173 updateParams ps _ = ps

171174

172− updateParamsA ((Nothing, b) : ns) (P _ n' _ : args)

173− = (Just n', b) : updateParamsA ns args

174− updateParamsA ((Just p, b) : ns) (P _ n' _ : args)

175− = (Just n', b && p == n') : updateParamsA ns args

176− updateParamsA ((mn, _) : ns) (_ : args)

177− = (mn, False) : updateParamsA ns args

178− updateParamsA ps args = ps

175+ updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all

176+ | n' `elem` concatMap freeNames all

177+ = (mn, False) : updateParamsA ns args (p : all)

178+ updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all

179+ = (Just n', b) : updateParamsA ns args (p : all)

180+ updateParamsA ((Just p, b) : ns) (tm@(P _ n' _) : args) all

181+ = (Just n', b && p == n') : updateParamsA ns args (tm : all)

182+ updateParamsA ((mn, _) : ns) (p : args) all

183+ = (mn, False) : updateParamsA ns args (p : all)

184+ updateParamsA ps args all = ps

179185

180186elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

181187 PTerm -> String -> Name -> PTerm -> Idris ()