6a8c4e7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some TODO notes and revisions in the paper

6a8c4e7Edwin Brady15 years ago

impl-paper/Makefile+1−1

compare with master

unifiedsplit

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

3all: ${PAPER}.pdf .PHONY

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

6− typechecking.tex elaboration.tex \

6+ typechecking.tex elaboration.tex delab.tex \

7 syntax.tex

9DIAGS =

impl-paper/conclusions.tex+3−1

@@ -102,7 +102,9 @@ types, by implementing a Haskell-like language augmented with \emph{full}

102dependent types.

103In this paper, we have seen how such a high level language can be implemented

104by building on top of a small, well-understood, easy to reason about type

105+theory.

106+%\todo{What makes Idris general purpose?}

105−theory. However, a programming language implementation is not an end in itself.

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

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

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

107domains. In future work, therefore, we plan to apply domain specific

109domains. In future work, therefore, we plan to apply domain specific

108language based techniques to realistic problems

110language based techniques to realistic problems

impl-paper/delab.texnew file+13

@@ -0,0 +1,13 @@

1+\section{Reversing Elaboration: From \TT{} to \Idris{}}

3+\label{sect:delab}

5+\subsection{Elaboration Properties}

7+\todo[inline]{

8+What are the properties of elaboration?

9+Need to define unelaboration, and say that elaborating then unelaborating

10+an expression yields the original expression.

11+(Works for expressions but not declarations)

12+}

13+

impl-paper/elaboration.tex+3

@@ -1435,6 +1435,8 @@ it to the current context:

1435

1436\subsubsection{\texttt{case} expressions}

1437

1438+\todo{Why not have case in \TT{}?}

1439+

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

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

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

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

1440\emph{top level} values. To elaborate a \texttt{case} expression, therefore,

1442\emph{top level} values. To elaborate a \texttt{case} expression, therefore,

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

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

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

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

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

1484

1486

1487+

1485%\subsubsection{Tactic-implicit arguments}

1488%\subsubsection{Tactic-implicit arguments}

1486

1489

1487

1490

impl-paper/hll.tex+21−36

@@ -21,16 +21,7 @@ arithmetic and comparison operators are defined for the primitive types,

21and are overloaded using type classes.

23An \Idris{} program consists of a module declaration, followed by an optional

24−list of imports and a collection of definitions and declarations, a simple example

24+list of imports and a collection of definitions and declarations, for example:

25−of which is shown in Figure \ref{constprims}. Like Haskell, the main function

26−is called \texttt{main}, and input and output is managed with an \texttt{IO}

27−monad. Unlike Haskell, however, we use a single colon \texttt{:} for type

28−declarations, and \remph{all} functions must have a top level type

29−declaration, since type inference is in general undecidable for languages with

30−dependent types.

31−

32−A module declaration also opens a \remph{namespace}. The fully qualified names

33−declared in this module are \texttt{main.x} and \texttt{main.main}.

35\begin{SaveVerbatim}{constprims}

26\begin{SaveVerbatim}{constprims}

@@ -43,13 +34,27 @@ main : IO ()

43main = putStrLn ("The answer is " ++ show x)

34main = putStrLn ("The answer is " ++ show x)

45\end{SaveVerbatim}

36\end{SaveVerbatim}

46−\codefig{constprims}{A simple \Idris{} module}

37+\useverb{constprims}

38+

39+\noindent

40+Like Haskell, the main function

41+is called \texttt{main}, and input and output is managed with an \texttt{IO}

42+monad. Unlike Haskell, however, we use a single colon \texttt{:} for type

43+declarations, emphasising the importance of types,

44+and \remph{all} functions must have a top level type

45+declaration. This is due to type inference being, in general,

46+undecidable for languages with

47+dependent types.

48+

49+A module declaration also opens a \remph{namespace}. The fully qualified names

50+declared in this module are \texttt{main.x} and \texttt{main.main}.

51+

48\subsection{Types and Functions}

53\subsection{Types and Functions}

50Data types are declared in a similar way to Haskell data types, with a similar

55Data types are declared in a similar way to Haskell data types, with a similar

51syntax. Natural numbers and lists, for example, are declared as follows in the

56syntax. Natural numbers and lists, for example, are declared as follows in the

52−library.

57+library:

54\begin{SaveVerbatim}{natlist}

59\begin{SaveVerbatim}{natlist}

@@ -60,6 +65,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists

60\end{SaveVerbatim}

65\end{SaveVerbatim}

61\useverb{natlist}

66\useverb{natlist}

68+\noindent

63The above declarations are taken from the standard library. Unary natural

69The above declarations are taken from the standard library. Unary natural

64numbers can be either zero, or

70numbers can be either zero, or

65the successor of another natural number (\texttt{S k}).

71the successor of another natural number (\texttt{S k}).

@@ -75,6 +81,7 @@ infixr 10 ::

75\end{SaveVerbatim}

81\end{SaveVerbatim}

76\useverb{infixcons}

82\useverb{infixcons}

84+\noindent

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

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

79with a precedence level of 10.

86with a precedence level of 10.

80Functions, data constructors and type constructors may all be given infix

87Functions, data constructors and type constructors may all be given infix

@@ -469,13 +476,8 @@ data Ordering = LT | EQ | GT

469

476

470class Eq a => Ord a where

477class Eq a => Ord a where

471 compare : a -> a -> Ordering

478 compare : a -> a -> Ordering

472−

473 (<) : a -> a -> Bool

479 (<) : a -> a -> Bool

474− (>) : a -> a -> Bool

480+ -- etc

475− (<=) : a -> a -> Bool

476− (>=) : a -> a -> Bool

477− max : a -> a -> a

478− min : a -> a -> a

479

481

480\end{SaveVerbatim}

482\end{SaveVerbatim}

481\useverb{eqord}

483\useverb{eqord}

@@ -513,24 +515,7 @@ showPerson p = let MkPerson name age = p in

513

515

514Another way of inspecting intermediate values of \emph{simple} types

516Another way of inspecting intermediate values of \emph{simple} types

515is to use a \texttt{case} expression.

517is to use a \texttt{case} expression.

516−The following function, for example, splits a string into two at a given character:

517−

518−\begin{SaveVerbatim}{split}

519−

520−splitAt : Char -> String -> (String, String)

521−splitAt c x = case break (== c) x of

522− (x, y) => (x, strTail y)

523−

524−\end{SaveVerbatim}

525−\useverb{split}

526−

527−\noindent

528−\texttt{break} is a library function which breaks a string into a pair of strings

529−at the point where the given function returns true. We then deconstruct the

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

531−

532−A \texttt{case} expression can match several cases, for example, to inspect an

533−intermediate value of type \texttt{Maybe a}. For example, \texttt{list\_lookup}

518+For example, \texttt{list\_lookup}

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

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

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

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

536looks up an index and returns a default value if the index is out of bounds:

521looks up an index and returns a default value if the index is out of bounds:

impl-paper/impldtp.tex+5−2

@@ -12,6 +12,7 @@

12\usepackage{url}

13%\usepackage{amsmath,amssymb}

14\usepackage{fancyvrb}

15+\usepackage{todonotes}

16\newenvironment{template}{\sffamily}

17\newenvironment{template}{\sffamily}

@@ -52,8 +53,8 @@

52\newcommand{\hdecl}[1]{\texttt{#1}}

53\newcommand{\hdecl}[1]{\texttt{#1}}

55−\title[Implementation of a General Purpose Language with Dependent Types]

56+\title

56− {Implementation of a General Purpose Programming Language with Dependent Types}

57+ {Implementing General Purpose Dependently Typed Programming Languages}

57%\subtitle{Implementing Domain Specific Languages by Overloading}

58%\subtitle{Implementing Domain Specific Languages by Overloading}

59\author[Edwin Brady]

60\author[Edwin Brady]

@@ -116,6 +117,8 @@ implementation of new high level language constructs.

116

117

117\input{elaboration.tex}

118\input{elaboration.tex}

118

119

120+\input{delab.tex}

121+

119%\input{compiling.tex}

122%\input{compiling.tex}

120

123

121%\input{syntax.tex}

124%\input{syntax.tex}

impl-paper/intro.tex+100−21

@@ -2,9 +2,13 @@

3Dependently typed programming languages, such as Agda \cite{norell2007thesis}

4and Coq \cite{Bertot2004}, have emerged in recent years as a promising approach

5−to ensuring the correctness of software. The \Idris{} language

5+to ensuring the correctness of software. Type checking ensures a program has

6+the intended meaning; \emph{dependent} types, where types may be predicated

7+on values, allow a programmer to give a program a \emph{precise} type and

8+hence have increased confidence of its correctness.

9+The \Idris{} language

6−\cite{Brady2011a} aims to take these ideas further, by providing support for

10+\cite{Brady2011a} aims to take this ideas further, by providing support for

7−verification of general purpose systems software. In contrast to Agda and Coq,

11+verification of \emph{general purpose} systems software. In contrast to Agda and Coq,

8which have arisen from the theorem proving community, \Idris{} takes Haskell as

12which have arisen from the theorem proving community, \Idris{} takes Haskell as

9its main influence. Recent Haskell extensions such as GADTs and type families have

13its main influence. Recent Haskell extensions such as GADTs and type families have

10given some of the power of dependent types to Haskell programmers. In the short

14given some of the power of dependent types to Haskell programmers. In the short

@@ -19,18 +23,18 @@ language, has no such limitation, essentially asking the question:

19\emph{``What if Haskell had \emph{full} dependent types?''}

23\emph{``What if Haskell had \emph{full} dependent types?''}

20\end{center}

24\end{center}

26+By \emph{full} dependent types, we mean that there is no restriction on which

22−It is important for the sake of usability of a programming language to provide

27+values may appear in types. It is important for the sake of usability of a

23−a notation which allows programmers to express high level concepts

28+programming language to provide a notation which allows programmers to express

24−in a natural way. Taking Haskell as a starting point means that \Idris{} offers

29+high level concepts in a natural way. Taking Haskell as a starting point means

25−high level structures such as type classes, \texttt{do}-notation, primitive types

30+that \Idris{} offers a variety of high level structures such as type classes,

26−and monadic I/O, for example.

31+\texttt{do}-notation, primitive types and monadic I/O, for example.

27−Furthermore, a goal of \Idris{} is to

32+Furthermore, a goal of \Idris{} is to support high level domain specific

28−support high level domain specific language implementation, providing appropriate

33+language implementation, providing appropriate notation for \emph{domain

29−notation for \emph{domain experts} and \emph{systems programmers}, who should not

34+experts} and \emph{systems programmers}, who should not be required to be type

30−be required to be type theorists in order to solve programming problems.

35+theorists in order to solve programming problems. Nevertheless, it is

31−Nevertheless, it is important for the sake of correctness of the language implementation

36+important for the sake of correctness of the language implementation to have a

32−to have a small core language with well understood meta-theory

37+well-defined core language with well-understood meta-theory \cite{Altenkirch2010}.

33−\cite{Altenkirch2010}.

34How can we achieve both of these goals?

38How can we achieve both of these goals?

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

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

@@ -42,14 +46,18 @@ As we shall see, this method allows higher level language constructs to be

42constructed in a straightforward manner, without compromising the simplicity

46constructed in a straightforward manner, without compromising the simplicity

43of the underlying type theory.

47of the underlying type theory.

45−\subsection{Overview}

49+\subsection{Contributions}

50+

51+\todo{Who is this paper for?}

47A dependently typed programming language relies on several components, many of

53A dependently typed programming language relies on several components, many of

48which are now well understood. For example, we rely on a type checker for

54which are now well understood. For example, we rely on a type checker for

49the core type theory \cite{Chapman2005epigram,loh2010tutorial}, a

55the core type theory \cite{Chapman2005epigram,loh2010tutorial}, a

50unification algorithm \cite{Miller1992} and an evaluator. However, it is less

56unification algorithm \cite{Miller1992} and an evaluator. However, it is less

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

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

58+programming language.

59+\todo{Anecdotal evidence for this?}

52−programming language. Therefore, the primary contribution of this paper is

60+Therefore, the primary contribution of this paper is

53an EDSL based method for translating programs in a

61an EDSL based method for translating programs in a

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

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

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

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

@@ -62,15 +70,16 @@ describing the EDSL and the specific tactics, the paper shows how to extend

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

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

63is equally applicable to other typed programming languages.

71is equally applicable to other typed programming languages.

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

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

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

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

67translated to the core language; Section \ref{sect:typechecking} describes the

75translated to the core language; Section \ref{sect:typechecking} describes the

68core language \TT{} and its typing rules, covering expressions, data types

76core language \TT{} and its typing rules, covering expressions, data types

69and pattern matching; Section \ref{sect:elaboration} describes the method

77and pattern matching; Section \ref{sect:elaboration} describes the method

70for translating \Idris{} to \TT{}, beginning with a restricted language

78for translating \Idris{} to \TT{}, beginning with a restricted language

71−\IdrisM{} before extending to higher level features; finally, in

79+\IdrisM{} before extending to higher level features; Section

80+\ref{sect:delab} describes the process for translating back to \Idris{}

81+and properties of the translation; finally,

72−Section \ref{sect:discussion} we discuss related work and conclude.

82+Section \ref{sect:discussion} discusses related work and concludes.

73−

75\subsection{Typographical conventions}

84\subsection{Typographical conventions}

@@ -93,4 +102,74 @@ of \emph{meta-operations}, which in practice are Haskell programs. Meta-operatio

93are operations on \Idris{} and \TT{} syntax, and are identified by their names being

102are operations on \Idris{} and \TT{} syntax, and are identified by their names being

94in $\MO{SmallCaps}$.

103in $\MO{SmallCaps}$.

104

105+\subsection{Elaboration Example}

106+

107+\Idris{} is a Haskell-like pure functional programming language with dependent types.

108+A simple example program is the following, which adds corresponding elements of

109+vectors of the same length:

110+

111+\begin{SaveVerbatim}{vadd}

112+

113+vAdd : Num a => Vect a n -> Vect a n -> Vect a n

114+vAdd [] [] = []

115+vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

116+

117+\end{SaveVerbatim}

118+\useverb{vadd}

119+

120+\noindent

121+This illustrates some basic features of \Idris{}:

122+

123+\begin{itemize}

124+\item A single colon is used for type declarations, and a double colon for the

125+cons operator.

126+\item Functions are defined by pattern matching, with a top level type declaration.

127+Names which are free in the type declaration (\texttt{a} and \texttt{n}) here

128+are implicitly bound.

129+\item The type system ensures that both input vectors are the same length (\texttt{n})

130+and have the same element type (\texttt{a}), and that the element type and length

131+are preserved in the output vector.

132+\item Functions can be overloaded using \remph{type classes}. Here, the element type

133+of the vector \texttt{a} must be numeric and therefore supports the \texttt{+} operator.

134+\end{itemize}

135+

136+\noindent

137+\Idris{} programs elaborate into a small core language, \TT{}, which is a $\lambda$-calculus

138+with dependent types, augmented with algebraic data types and pattern matching.

139+\TT{} programs are fully explicitly typed, including the names \texttt{a} and \texttt{n}

140+in the type declaration, and the names bound in each pattern match clause.

141+Type classes are also made explicit.

142+The \TT{} translation of \texttt{vAdd} is:

143+

144+\DM{

145+\AR{

146+\begin{array}{ll}

147+\FN{vAdd} & \Hab(\va\Hab\Set)\to(\vn\Hab\Nat)\to\TC{Num}\:\va\to

148+ \Vect\:\va\:\vn\to\Vect\:\va\:\vn\to\Vect\:\va\:\vn\\

149+\end{array}

150+\\

151+\begin{array}{lccccccc}

152+\multicolumn{5}{l}{

153+\RW{var}\:\va\Hab\Set,\:\vc\Hab\TC{Num}\;\va\SC}\\

154+\hg\FN{vAdd} & \va & \Z & \vc & (\DC{Nil}\;\va) & (\DC{Nil}\;\va) & \Ret{\DC{Nil}\;\va} \\

155+\multicolumn{5}{l}{

156+\RW{var}\:\AR{

157+\va\Hab\Set,\:\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\

158+\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;

159+\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk

160+\SC

161+}

162+}\\

163+\hg\FN{vAdd} & \va & (\suc\;\vk) & \vc

164+ & ((\DC{::})\;\va\;\vk\;\vx\;\vxs)

165+ & ((\DC{::})\;\va\;\vk\;\vy\;\vys)

166+ & \\

167+ & & \MRet{5}{((\DC{::})\;\va\;\vk\;((+)\;\vc\;\vx\;\vy)\; (\FN{vAdd}\;\va\;\vk\;\vc\;\vxs\;\vys))}

168+\end{array}

169+}

170+}

171+

172+\noindent

173+The rest of this paper describes \Idris{} and \TT{}, and systematically explains

174+how to translate from one to the other.

175

impl-paper/library.bib+983−970

@@ -1,96 +1,68 @@

1Automatically generated by Mendeley 1.3.1

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

4−@inproceedings{McBride2006,

4+@book{Cryptography2012,

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

5+author = {Anderson, Ross},

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

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

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

7+file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 5.pdf:pdf},

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

8+isbn = {9780470068526},

9−year = {2006}

9+issn = {1460-2377},

10−}

10+month = apr,

11−@inproceedings{czarnecki2004dsl,

11+number = {4},

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

12+pmid = {22451589},

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

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

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

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

15−pages = {51--72},

15+volume = {24}

16−publisher = {Springer},

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

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

19−year = {2004}

20−}

21−@phdthesis{Brady2005,

22−author = {Brady, Edwin},

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

24−keywords = {Dependent Types},

25−mendeley-tags = {Dependent Types},

26−school = {University of Durham},

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

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

29−year = {2005}

30−}

31−@inproceedings{Kimmell2012,

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

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

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}

16}

38−@article{Epstein2011,

17+@inproceedings{ko2011modularising,

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

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

40−institution = {Microsoft Research},

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

41−journal = {researchmicrosoftcom},

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

42−number = {Section 8},

43−pages = {1--12},

21+pages = {13--24},

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

22+publisher = {ACM},

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

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

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

46year = {2011}

25year = {2011}

47}

26}

48−@article{Altenkirch2010a,

27+@inproceedings{gibbons2011modularising,

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

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

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

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

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

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

52−journal = {Citeseer},

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

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}

32+year = {2011}

57}

33}

58−@article{fisher2006next,

34+@article{Okasaki1993,

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

35+author = {Okasaki, Chris},

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

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

61−journal = {Journal of the ACM},

37+journal = {Journal of functional programming},

62−number = {2},

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

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}

39+year = {1993}

69}

40}

70−@misc{The2012b,

41+@misc{Brady2012b,

71author = {Brooks, Fred},

42author = {Brooks, Fred},

72doi = {10.1093/epirev/mxr031},

43doi = {10.1093/epirev/mxr031},

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

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

74isbn = {9780321702081},

45isbn = {9780321702081},

75issn = {1478-6729},

46issn = {1478-6729},

76pmid = {22215642},

47pmid = {22215642},

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

48+title = {{The Design of Design Chapter 2}}

78}

49}

79−@article{Chapman2005epigram,

50+@inproceedings{Brady2003,

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

51+author = {Brady, Edwin and McBride, Conor and McKinna, James},

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

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

82−journal = {Trends in Functional Programming},

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

83−publisher = {Intellect Books},

54+keywords = {Dependent Types},

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

55+mendeley-tags = {Dependent Types},

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

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

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

86−year = {2005}

58+year = {2003}

87}

59}

88@misc{TheMendeleySupportTeam2011,

60@misc{TheMendeleySupportTeam2011,

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

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

90address = {London},

62address = {London},

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

63author = {{The Mendeley Support Team}},

92booktitle = {Mendeley Desktop},

64booktitle = {Mendeley Desktop},

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

65+file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

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

66keywords = {Mendeley,how-to,user manual},

95pages = {1--16},

67pages = {1--16},

96publisher = {Mendeley Ltd.},

68publisher = {Mendeley Ltd.},

@@ -98,52 +70,78 @@ title = {{Getting Started with Mendeley}},

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

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

99year = {2011}

71year = {2011}

100}

72}

101−@phdthesis{Okasaki1996,

73+@inproceedings{Wadler1989,

102−author = {Okasaki, Chris},

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

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

75+author = {Wadler, Philip},

104−school = {Carnegie Mellon University},

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

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

77+doi = {10.1145/99370.99404},

78+file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},

79+isbn = {0897913280},

80+number = {June},

81+pages = {347--359},

82+publisher = {ACM},

83+series = {FPCA '89},

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

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

106−year = {1996}

86+year = {1989}

107}

87}

108−@article{mcbride2008functional,

88+@phdthesis{norell2007thesis,

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

89+author = {Norell, Ulf},

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

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

111−journal = {Journal of functional programming},

91+keywords = {Dependent Types},

112−number = {1},

92+mendeley-tags = {Dependent Types},

113−pages = {1--13},

93+publisher = {Citeseer},

114−publisher = {Cambridge Univ Press},

94+school = {Chalmers University of Technology},

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

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

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

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

117−volume = {18},

118−year = {2008}

97+year = {2007}

119}

98}

120−@inproceedings{madhavapeddy2007melange,

99+@inproceedings{l,

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

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

122−booktitle = {ACM SIGOPS Operating Systems Review},

101+booktitle = {ACM SIGPLAN Notices},

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

102+file = {:home/edwin/Research/Papers/Mendeley/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},

124number = {3},

103number = {3},

125−pages = {101--114},

104+pages = {26--37},

126publisher = {ACM},

105publisher = {ACM},

127−title = {{Melange: creating a functional internet}},

106+title = {{Scrap your boilerplate: a practical design pattern for generic programming}},

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

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

129−volume = {41},

108+volume = {38},

130−year = {2007}

109+year = {2003}

131}

110}

132−@inproceedings{lempsink2009type,

111+@inproceedings{Xi1999,

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

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

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

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

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

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

115+doi = {10.1145/292540.292560},

116+file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},

117+isbn = {1581130953},

118+issn = {07439016},

119+keywords = {Dependent Types},

120+mendeley-tags = {Dependent Types},

121+organization = {Carnegie Mellon University},

136−pages = {61--72},

122+pages = {214--227},

137−publisher = {ACM},

123+publisher = {ACM Press},

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

124+series = {POPL '99},

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

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

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

127+volume = {26},

140−year = {2009}

128+year = {1999}

129+}

130+@inproceedings{morris2006exploring,

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

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

133+file = {:home/edwin/Research/Papers/Mendeley/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

134+pages = {252--267},

135+publisher = {Springer},

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

137+url = {http://www.springerlink.com/index/f9p1317716614834.pdf},

138+year = {2006}

141}

139}

142@book{Approach2012,

140@book{Approach2012,

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

141author = {Hunt, Andrew and Thomas, David},

144booktitle = {Carcinogenesis},

142booktitle = {Carcinogenesis},

145doi = {10.1093/carcin/bgs054},

143doi = {10.1093/carcin/bgs054},

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

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

147isbn = {020161622X},

145isbn = {020161622X},

148issn = {1460-2180},

146issn = {1460-2180},

149number = {3},

147number = {3},

@@ -152,220 +150,99 @@ title = {{The Pragmatic Programmer Chapter 2}},

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

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

153volume = {33}

151volume = {33}

154}

152}

153+@article{Miller1992,

154+author = {Miller, Dale},

155+file = {:home/edwin/Research/Papers/Mendeley/Miller/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},

156+journal = {Journal of Symbolic Computation},

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

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

159+year = {1992}

160+}

161+@misc{Interface2012a,

162+author = {Kreibich, Jay A.},

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

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

165+isbn = {9781449394592},

166+issn = {1478-6729},

167+pmid = {22215642},

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

169+}

155−@inproceedings{stump2010resource,

170+@inproceedings{chlipala2010ur,

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

171+author = {Chlipala, Adam},

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

172+booktitle = {ACM SIGPLAN Notices},

158−file = {:Users/edwin/Documents/Mendeley Desktop/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

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

174+number = {6},

159−pages = {27--38},

175+pages = {122--133},

160publisher = {ACM},

176publisher = {ACM},

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

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

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

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

179+volume = {45},

163year = {2010}

180year = {2010}

164}

181}

165−@article{mcbride2010ornamental,

182+@book{peyton1987implementation,

166−author = {McBride, Conor},

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

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

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

168−journal = {Journal of Functional Programming},

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

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

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

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

171−year = {2010}

187+year = {1987}

172}

188}

173−@article{Swierstra2011,

189+@article{dybjer1994inductive,

174−author = {Swierstra, W},

190+author = {Dybjer, P.},

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

191+journal = {Formal aspects of computing},

176−journal = {Journal of Functional Programming},

177−number = {6},

192+number = {4},

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

193+pages = {440--465},

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

194+publisher = {Springer},

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

195+title = {{Inductive families}},

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

181−volume = {21},

197+volume = {6},

182−year = {2011}

198+year = {1994}

183}

199}

184−@article{McBride2002,

200+@inproceedings{lempsink2009type,

185−author = {McBride, C},

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

186−journal = {Types for proofs and programs},

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

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

203+file = {:home/edwin/Research/Papers/Mendeley/Lempsink, Leather, L\"{o}h/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},

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

204+pages = {61--72},

205+publisher = {ACM},

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

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

189−year = {2000}

208+year = {2009}

190}

209}

191−@article{Xi1998,

210+@misc{The2012b,

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

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

194−doi = {10.1145/277652.277732},

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

196−isbn = {0897919874},

197−issn = {03621340},

198−journal = {ACM Sigplan Notices},

199−keywords = {Dependent Types},

200−mendeley-tags = {Dependent Types},

201−number = {5},

202−pages = {249--257},

203−publisher = {ACM},

204−series = {PLDI '98},

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

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

207−volume = {33},

208−year = {1998}

209−}

210−@misc{idristutorial,

211−author = {Brady, Edwin},

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

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

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

215−year = {2012}

216−}

217−@inproceedings{NanevskiAAMorrisett2008,

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

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

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

221−doi = {10.1145/1411204.1411237},

222−file = {:Users/edwin/Documents/Mendeley Desktop/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},

223−isbn = {9781595939197},

224−issn = {15232867},

225−keywords = {Dependent Types},

226−mendeley-tags = {Dependent Types},

227−number = {9},

228−pages = {229--240},

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

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

231−volume = {43},

232−year = {2008}

233−}

234−@misc{Brady2012c,

235author = {Brooks, Fred},

211author = {Brooks, Fred},

236doi = {10.1093/epirev/mxr031},

212doi = {10.1093/epirev/mxr031},

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

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

238isbn = {9780321702081},

214isbn = {9780321702081},

239issn = {1478-6729},

215issn = {1478-6729},

240−number = {1},

241−pages = {NP},

242pmid = {22215642},

216pmid = {22215642},

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

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

244−volume = {34}

245}

218}

246−@inproceedings{ko2011modularising,

219+@misc{The2012c,

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

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

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

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

249−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

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

250−pages = {13--24},

223+isbn = {9780596529833},

251−publisher = {ACM},

224+issn = {1478-6729},

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

225+pmid = {22215642},

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

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

254−year = {2011}

255}

227}

256−@book{Choosing2012,

228+@book{Brady2012,

257−author = {Fowler, Martin},

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

258booktitle = {Carcinogenesis},

230booktitle = {Carcinogenesis},

259doi = {10.1093/carcin/bgs054},

231doi = {10.1093/carcin/bgs054},

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

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

261−isbn = {9780132107549},

233+isbn = {020161622X},

262issn = {1460-2180},

234issn = {1460-2180},

263number = {3},

235number = {3},

264pmid = {22383472},

236pmid = {22383472},

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

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

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

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

267volume = {33}

239volume = {33}

268}

240}

269−@article{marlow2006making,

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

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

272−journal = {Journal of Functional Programming},

273−number = {4-5},

274−pages = {415--449},

275−publisher = {Cambridge University Press},

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

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

278−volume = {16},

279−year = {2006}

280−}

281−@article{Mandelbaum2007,

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

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

284−doi = {10.1145/1190215.1190231},

285−isbn = {1595935754},

286−issn = {03621340},

287−journal = {SIGPLAN Not},

288−number = {1},

289−pages = {77--83},

290−publisher = {ACM},

291−series = {POPL '07},

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

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

294−volume = {42},

295−year = {2007}

296−}

297−@article{Abel2010,

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

299−author = {Abel, Andreas},

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

301−journal = {EPTCS},

302−pages = {1--15},

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

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

305−volume = {43},

306−year = {2010}

307−}

308−@article{Hoare1978,

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

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

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

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

313−file = {:Users/edwin/Documents/Mendeley Desktop/Hoare/Hoare - 1978 - Communicating sequential processes.pdf:pdf},

314−isbn = {0131532715},

315−issn = {01676423},

316−journal = {Communications of the ACM},

317−number = {8},

318−pages = {666--677},

319−pmid = {2142694823583477576},

320−publisher = {ACM},

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

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

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

324−volume = {21},

325−year = {1978}

326−}

327−@book{Bird2010,

328−author = {Bird, Richard},

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

330−isbn = {9780521513388},

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

332−year = {2010}

333−}

334−@inproceedings{oury2008power,

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

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

337−file = {:Users/edwin/Documents/Mendeley Desktop/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

338−keywords = {Dependent Types},

339−mendeley-tags = {Dependent Types},

340−number = {9},

341−pages = {39--50},

342−publisher = {ACM},

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

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

345−volume = {43},

346−year = {2008}

347−}

348−@inproceedings{madhavapeddy2010turning,

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

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

351−file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},

352−publisher = {USENIX Association},

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

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

355−year = {2010}

356−}

357−@book{peyton1987implementation,

358−author = {{Peyton Jones}, S.L.},

359−publisher = {Prentice-Hall, Inc.},

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

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

362−year = {1987}

363−}

364@inproceedings{Pasalic2002,

241@inproceedings{Pasalic2002,

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

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

366booktitle = {International Conference on Functional Programming},

243booktitle = {International Conference on Functional Programming},

367doi = {10.1145/583852.581499},

244doi = {10.1145/583852.581499},

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

245+file = {:home/edwin/Research/Papers/Mendeley/Pa\v{s}alic, Taha, Sheard/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},

369isbn = {1-58113-487-8},

246isbn = {1-58113-487-8},

370issn = {03621340},

247issn = {03621340},

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

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

@@ -377,94 +254,43 @@ url = {http://dl.acm.org/citation.cfm?id=583852.581499},

377volume = {37},

254volume = {37},

378year = {2002}

255year = {2002}

379}

256}

380−@inproceedings{Brady2010,

257+@misc{Nodes2012a,

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

258+author = {Brooks, Fred},

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

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

383−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},

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

384−isbn = {9781605587943},

261+isbn = {9780321702081},

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

262+issn = {1478-6729},

386−mendeley-tags = {Dependent Types},

263+pmid = {22215642},

387−pages = {297--308},

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

388−publisher = {ACM},

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

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

391−year = {2010}

392−}

393−@inproceedings{Fournet2011,

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

395−booktitle = {Foundations of security analysis and design {VI}},

396−file = {:Users/edwin/Documents/Mendeley Desktop/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},

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

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

399−year = {2010}

400−}

401−@article{landin1966next,

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

403−file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},

404−journal = {Communications of the ACM},

405−number = {3},

406−pages = {157--166},

407−publisher = {ACM},

408−title = {{The next 700 programming languages}},

409−url = {http://dl.acm.org/citation.cfm?id=365257 )},

410−volume = {9},

411−year = {1966}

412−}

413−@inproceedings{bhargavan2010modular,

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

415−booktitle = {ACM Sigplan Notices},

416−number = {1},

417−pages = {445--456},

418−publisher = {ACM},

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

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

421−volume = {45},

422−year = {2010}

423}

265}

424@article{Haskell2012a,

266@article{Haskell2012a,

425author = {Biancuzzi, F and Warden, S},

267author = {Biancuzzi, F and Warden, S},

426doi = {10.1093/epirev/mxr031},

268doi = {10.1093/epirev/mxr031},

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

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

428isbn = {9780596801670},

270isbn = {9780596801670},

429issn = {1478-6729},

271issn = {1478-6729},

430pmid = {22215642},

272pmid = {22215642},

431title = {{Masterminds of Programming Chapter 8}}

273title = {{Masterminds of Programming Chapter 8}}

432}

274}

433−@book{Brady2012,

275+@book{An2012,

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

276+author = {Fowler, Martin},

435booktitle = {Carcinogenesis},

277booktitle = {Carcinogenesis},

436doi = {10.1093/carcin/bgs054},

278doi = {10.1093/carcin/bgs054},

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

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

438−isbn = {020161622X},

280+isbn = {9780132107549},

439issn = {1460-2180},

281issn = {1460-2180},

440number = {3},

282number = {3},

441pmid = {22383472},

283pmid = {22383472},

442−title = {{The Pragmatic Programmer Chapter 5}},

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

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

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

444volume = {33}

286volume = {33}

445}

287}

446−@article{McBride2007,

288+@article{McBride2002,

447−author = {McBride, Conor and Paterson, Ross},

289+author = {McBride, C},

448−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},

290+journal = {Types for proofs and programs},

449−journal = {Journal of functional programming},

291+title = {{Elimination with a Motive}},

450−title = {{Applicative programming with effects}},

451−url = {http://journals.cambridge.org/abstract_S0956796807006326},

452−year = {2007}

453−}

454−@inproceedings{Altenkirch2010,

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

456−author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},

457−booktitle = {{FLOPS 2010}},

458−doi = {10.1007/978-3-642-12251-4_5},

459−editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},

460−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},

461−isbn = {9783642122507},

462−pages = {40----55},

463−publisher = {Springer Berlin Heidelberg},

464−series = {Lecture Notes in Computer Science},

465−title = {{Dependent Types without the Sugar}},

466−url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},

292+url = {http://www.springerlink.com/index/vbpg19305t46f6dm.pdf},

467−year = {2010}

293+year = {2000}

468}

294}

469@article{McBride2005,

295@article{McBride2005,

470author = {McBride, Conor},

296author = {McBride, Conor},

@@ -481,71 +307,30 @@ url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},

481volume = {3622},

307volume = {3622},

482year = {2005}

308year = {2005}

483}

309}

484−@misc{Bloat,

310+@misc{Resolution2012a,

485−author = {Brooks, Fred},

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

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

487−isbn = {9780321702081},

488−title = {{The Design of Design Chapter 4}}

489−}

490−@misc{Protocols2012a,

491−author = {Anderson, Ross},

492doi = {10.1093/epirev/mxr031},

312doi = {10.1093/epirev/mxr031},

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

313+file = {:home/edwin/Research/Papers/Mendeley/Fall, Stevens/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

494−isbn = {9780470068526},

495issn = {1478-6729},

314issn = {1478-6729},

496pmid = {22215642},

315pmid = {22215642},

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

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

498}

317}

499−@inproceedings{Augustsson1998,

318+@phdthesis{Brady2005,

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

319+author = {Brady, Edwin},

501−author = {Augustsson, Lennart},

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

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

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

504−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

505−issn = {14735687},

506−keywords = {Depe,Dependent Types},

321+keywords = {Dependent Types},

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

322+mendeley-tags = {Dependent Types},

508−number = {1},

323+school = {University of Durham},

509−pages = {239--250},

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

510−pmid = {21139473},

511−publisher = {ACM Press},

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

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

514−volume = {23},

515−year = {1998}

516−}

517−@book{Hunt,

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

519−booktitle = {Design},

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

521−isbn = {020161622X},

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

523−}

524−@article{burrows1990,

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

526−file = {:Users/edwin/Documents/Mendeley Desktop/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

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

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

529−title = {{A logic of authentication}},

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

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

531−volume = {8},

532−year = {1990}

533−}

534−@inproceedings{atkey2009unembedding,

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

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

537−pages = {37--48},

538−publisher = {ACM},

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

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

541−year = {2009}

326+year = {2005}

542}

327}

543@inproceedings{Brady2011a,

328@inproceedings{Brady2011a,

544address = {New York, New York, USA},

329address = {New York, New York, USA},

545author = {Brady, Edwin},

330author = {Brady, Edwin},

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

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

547doi = {10.1145/1929529.1929536},

332doi = {10.1145/1929529.1929536},

548−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},

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

549isbn = {9781450304870},

334isbn = {9781450304870},

550keywords = {Dependent Types,data description,dependent types},

335keywords = {Dependent Types,data description,dependent types},

551mendeley-tags = {Dependent Types},

336mendeley-tags = {Dependent Types},

@@ -555,223 +340,329 @@ title = {{Idris --- Systems Programming Meets Full Dependent Types}},

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

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

556year = {2011}

341year = {2011}

557}

342}

558−@inproceedings{gibbons2011modularising,

343+@misc{dagand2011transporting,

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

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

560−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

345+file = {:home/edwin/Research/Papers/Mendeley/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

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

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

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

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

563year = {2011}

348year = {2011}

564}

349}

565−@book{An2012,

566−author = {Fowler, Martin},

567−booktitle = {Carcinogenesis},

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

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

570−isbn = {9780132107549},

571−issn = {1460-2180},

572−number = {3},

573−pmid = {22383472},

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

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

576−volume = {33}

577−}

578−@inproceedings{coquand1986analysis,

350+@inproceedings{taha2004gentle,

579−author = {Coquand, T.},

351+author = {Taha, W.},

580−booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},

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

581−file = {:Users/edwin/Documents/Mendeley Desktop/Coquand/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},

582−pages = {227----246},

353+pages = {30--50},

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

354+publisher = {Springer},

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

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

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

585−year = {1986}

357+year = {2004}

586}

358}

587−@misc{altenkirch2008nσ,

359+@inproceedings{augustsson2008paradise,

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

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

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

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

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

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

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

363+number = {9},

364+pages = {225--228},

365+publisher = {ACM},

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

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

368+volume = {43},

592year = {2008}

369year = {2008}

593}

370}

594−@inproceedings{barras2008implicit,

371+@misc{altenkirch2005dependent,

595−author = {Barras, B. and Bernardo, B.},

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

596−booktitle = {Foundations of Software Science and Computational Structures},

373+booktitle = {Manuscript, available online},

597−file = {:Users/edwin/Documents/Mendeley Desktop/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},

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

598−pages = {365--379},

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

599−publisher = {Springer},

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

600−title = {{The implicit calculus of constructions as a programming language with dependent types}},

601−url = {http://www.springerlink.com/index/m84h82904546l265.pdf},

602−year = {2008}

377+year = {2005}

603}

378}

604−@book{While2012,

379+@article{Xi1998,

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

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

606−booktitle = {Carcinogenesis},

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

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

382+doi = {10.1145/277652.277732},

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

383+file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},

609−isbn = {020161622X},

384+isbn = {0897919874},

610−issn = {1460-2180},

385+issn = {03621340},

386+journal = {ACM Sigplan Notices},

387+keywords = {Dependent Types},

388+mendeley-tags = {Dependent Types},

611−number = {3},

389+number = {5},

612−pmid = {22383472},

390+pages = {249--257},

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

391+publisher = {ACM},

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

392+series = {PLDI '98},

393+title = {{Eliminating array bound checking through dependent types}},

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

615−volume = {33}

395+volume = {33},

396+year = {1998}

616}

397}

617−@inproceedings{bradyresource,

398+@inproceedings{augustsson1999exercise,

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

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

619−booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},

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

620−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},

401+keywords = {Depe},

621−pages = {242----257},

402+mendeley-tags = {Depe},

622−title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},

403+publisher = {Citeseer},

623−url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},

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

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

624−year = {2012}

406+year = {1999}

625}

407}

626−@book{luo1994,

408+@article{Swierstra2011,

627−author = {Luo, Z.},

409+author = {Swierstra, W},

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

410+file = {:home/edwin/Research/Papers/Mendeley/Swierstra/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},

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

411+journal = {Journal of Functional Programming},

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

412+number = {6},

413+pages = {575----583},

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

415+url = {http://journals.cambridge.org/abstract_S0956796811000207},

416+volume = {21},

631−year = {1994}

417+year = {2011}

632}

418}

633−@phdthesis{norell2007thesis,

419+@inproceedings{norell2009dependently,

634author = {Norell, Ulf},

420author = {Norell, Ulf},

421+booktitle = {Advanced Functional Programming},

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

422+file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

636keywords = {Dependent Types},

423keywords = {Dependent Types},

637mendeley-tags = {Dependent Types},

424mendeley-tags = {Dependent Types},

425+pages = {230--266},

638−publisher = {Citeseer},

426+publisher = {Springer},

639−school = {Chalmers University of Technology},

427+title = {{Dependently typed programming in Agda}},

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

428+url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

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

642−year = {2007}

429+year = {2009}

643−}

644−@inproceedings{Brady2006b,

645−author = {Brady, Edwin},

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

647−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

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

649−month = sep,

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

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

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

653−year = {2006}

654}

430}

655−@inproceedings{chlipala2010ur,

431+@article{Mandelbaum2007,

656−author = {Chlipala, Adam},

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

657−booktitle = {ACM SIGPLAN Notices},

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

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

434+doi = {10.1145/1190215.1190231},

435+isbn = {1595935754},

436+issn = {03621340},

437+journal = {SIGPLAN Not},

659−number = {6},

438+number = {1},

660−pages = {122--133},

439+pages = {77--83},

661publisher = {ACM},

440publisher = {ACM},

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

441+series = {POPL '07},

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

442+title = {{PADS/ML: a functional data description language}},

443+url = {http://doi.acm.org/10.1145/1190216.1190231},

664−volume = {45},

444+volume = {42},

665−year = {2010}

445+year = {2007}

666}

446}

667@misc{Abadi1997,

447@misc{Abadi1997,

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

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

669booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},

449booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},

670−file = {:Users/edwin/Documents/Mendeley Desktop/Abadi, Gordon/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},

450+file = {:home/edwin/Research/Papers/Mendeley/Abadi, Gordon/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},

671pages = {36 -- 47},

451pages = {36 -- 47},

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

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

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

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

674year = {1997}

454year = {1997}

675}

455}

676−@article{Jones2003,

456+@article{Jones1999,

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

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

678−author = {Jones, Simon Peyton},

458+author = {Jones, Mark P},

679−editor = {Jones, Simon Peyton},

680−isbn = {0521826144},

681−journal = {Language},

459+journal = {October},

682−number = {1},

460+publisher = {Citeseer},

683−publisher = {Cambridge University Press},

461+title = {{Typing Haskell in Haskell}},

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

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

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

686−volume = {13},

687−year = {2003}

463+year = {1999}

688}

464}

689−@inproceedings{Visser2008,

465+@inproceedings{Altenkirch2010,

690−author = {Visser, E},

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

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

467+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},

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

468+booktitle = {{FLOPS 2010}},

469+doi = {10.1007/978-3-642-12251-4_5},

470+editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},

471+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},

472+isbn = {9783642122507},

473+pages = {40----55},

474+publisher = {Springer Berlin Heidelberg},

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

476+title = {{Dependent Types without the Sugar}},

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

477+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},

694−year = {2008}

478+year = {2010}

695}

479}

480+@book{Bertot2004,

481+author = {Bertot, Yves and Cast\'{e}ran, Pierre},

482+publisher = {Springer},

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

484+url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},

485+year = {2004}

486+}

487+@book{The2012,

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

489+booktitle = {Carcinogenesis},

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

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

492+isbn = {020161622X},

493+issn = {1460-2180},

494+number = {3},

495+pmid = {22383472},

496+title = {{The Pragmatic Programmer Chapter 3}},

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

498+volume = {33}

499+}

696−@inproceedings{ko2011modularising,

500+@inproceedings{ko2011modularising,

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

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

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

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

699−pages = {13--24},

503+pages = {13--24},

700−publisher = {ACM},

504+publisher = {ACM},

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

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

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

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

703year = {2011}

507year = {2011}

704}

508}

705−@misc{Attacks2012a,

509+@article{danielsson2011parsing,

706−author = {Anderson, Ross},

510+author = {Danielsson, N. and Norell, U.},

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

511+journal = {Implementation and Application of Functional Languages},

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

709−isbn = {9780470068526},

710−issn = {1478-6729},

711−number = {1},

712−pages = {NP},

512+pages = {80--99},

713−pmid = {22215642},

513+publisher = {Springer},

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

514+title = {{Parsing mixfix operators}},

715−volume = {34}

515+url = {http://www.springerlink.com/index/386243257W504252.pdf},

516+year = {2011}

716}

517}

518+@misc{Bove2008,

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

520+author = {Bove, Ana and Dybjer, Peter},

521+booktitle = {Notes},

522+doi = {10.1007/978-3-642-03153-3_2},

523+file = {:home/edwin/Research/Papers/Mendeley/Bove, Dybjer/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},

524+number = {February},

525+pages = {57--99},

526+publisher = {Springer},

527+title = {{Dependent Types at Work}},

528+url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},

529+volume = {5520},

530+year = {2008}

531+}

532+@book{luo1994,

533+author = {Luo, Z.},

534+publisher = {Oxford University Press, Inc.},

535+title = {{Computation and reasoning: a type theory for computer science}},

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

537+year = {1994}

538+}

539+@misc{idristutorial,

540+author = {Brady, Edwin},

541+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},

542+title = {{Programming in Idris : a tutorial}},

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

544+year = {2012}

545+}

717−@inproceedings{l,

546+@inproceedings{madhavapeddy2007melange,

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

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

719−booktitle = {ACM SIGPLAN Notices},

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

720−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},

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

721number = {3},

550number = {3},

722−pages = {26--37},

551+pages = {101--114},

723publisher = {ACM},

552publisher = {ACM},

724−title = {{Scrap your boilerplate: a practical design pattern for generic programming}},

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

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

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

726−volume = {38},

555+volume = {41},

727−year = {2003}

728−}

729−@misc{pollack1997believe,

730−author = {Pollack, R.},

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

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

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

734−year = {1997}

556+year = {2007}

735}

557}

736−@book{Bertot2004,

558+@inproceedings{Augustsson1998,

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

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

560+author = {Augustsson, Lennart},

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

562+doi = {10.1097/MEG.0b013e328342f213},

563+file = {:home/edwin/Research/Papers/Mendeley/Augustsson/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

564+issn = {14735687},

565+keywords = {Depe,Dependent Types},

566+mendeley-tags = {Depe,Dependent Types},

567+number = {1},

568+pages = {239--250},

569+pmid = {21139473},

738−publisher = {Springer},

570+publisher = {ACM Press},

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

571+title = {{Cayenne - a language with dependent types}},

740−url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},

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

573+volume = {23},

741−year = {2004}

574+year = {1998}

742}

575}

743@inproceedings{brady2011epic,

576@inproceedings{brady2011epic,

744author = {Brady, Edwin},

577author = {Brady, Edwin},

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

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

746−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},

579+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},

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

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

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

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

749year = {2011}

582year = {2011}

750}

583}

751−@article{dybjer1994inductive,

584+@article{Epstein2011,

752−author = {Dybjer, P.},

585+author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},

753−journal = {Formal aspects of computing},

586+institution = {Microsoft Research},

754−number = {4},

587+journal = {researchmicrosoftcom},

755−pages = {440--465},

588+number = {Section 8},

756−publisher = {Springer},

589+pages = {1--12},

757−title = {{Inductive families}},

590+title = {{Haskell for the cloud}},

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

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

759−volume = {6},

592+year = {2011}

760−year = {1994}

761}

593}

762−@inproceedings{McBride2004b,

594+@book{Hunt,

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

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

764−booktitle = {Haskell Workshop},

596+booktitle = {Design},

765−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},

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

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

598+isbn = {020161622X},

767−year = {2004}

599+title = {{The Pragmatic Programmer Chapter 4}}

600+}

601+@inproceedings{swierstra2007beauty,

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

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

604+file = {:home/edwin/Research/Papers/Mendeley/Swierstra, Altenkirch/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},

605+pages = {25--36},

606+publisher = {ACM},

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

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

609+year = {2007}

610+}

611+@inproceedings{bradyresource,

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

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

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

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

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

617+url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},

618+year = {2012}

619+}

620+@article{fisher2006next,

621+author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},

622+file = {:home/edwin/Research/Papers/Mendeley/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},

623+journal = {Journal of the ACM},

624+number = {2},

625+pages = {1--51},

626+publisher = {ACM},

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

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

629+volume = {15},

630+year = {2010}

631+}

632+@book{Bird2010,

633+author = {Bird, Richard},

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

635+isbn = {9780521513388},

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

637+year = {2010}

638+}

639+@inproceedings{stump2010resource,

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

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

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

643+pages = {27--38},

644+publisher = {ACM},

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

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

647+year = {2010}

648+}

649+@inproceedings{taha1997multi,

650+author = {Taha, W. and Sheard, T.},

651+booktitle = {ACM SIGPLAN Notices},

652+number = {12},

653+pages = {203--217},

654+publisher = {ACM},

655+title = {{Multi-stage programming with explicit annotations}},

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

657+volume = {32},

658+year = {1997}

768}

659}

769@article{Wadler2001,

660@article{Wadler2001,

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

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

771author = {Wadler, Philip},

662author = {Wadler, Philip},

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

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

773editor = {Jeuring, Johan and Meijer, Erik},

664editor = {Jeuring, Johan and Meijer, Erik},

774−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 2001 - Monads for functional programming.pdf:pdf},

665+file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 2001 - Monads for functional programming.pdf:pdf},

775isbn = {3540594515},

666isbn = {3540594515},

776issn = {03029743},

667issn = {03029743},

777journal = {Advanced Functional Programming},

668journal = {Advanced Functional Programming},

@@ -784,34 +675,30 @@ url = {http://www.springerlink.com/index/715264614rh13340.pdf},

784volume = {925},

675volume = {925},

785year = {2001}

676year = {2001}

786}

677}

787−@inproceedings{taha1997multi,

678+@article{Hoare1978,

788−author = {Taha, W. and Sheard, T.},

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

789−booktitle = {ACM SIGPLAN Notices},

680+author = {Hoare, C A R},

790−number = {12},

681+doi = {10.1016/0167-6423(87)90028-1},

791−pages = {203--217},

682+editor = {McKeag, R M and Macnaghten, A M},

683+file = {:home/edwin/Research/Papers/Mendeley/Hoare/Hoare - 1978 - Communicating sequential processes.pdf:pdf},

684+isbn = {0131532715},

685+issn = {01676423},

686+journal = {Communications of the ACM},

687+number = {8},

688+pages = {666--677},

689+pmid = {2142694823583477576},

792publisher = {ACM},

690publisher = {ACM},

793−title = {{Multi-stage programming with explicit annotations}},

691+series = {International Series in Computer Science},

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

692+title = {{Communicating sequential processes}},

795−volume = {32},

693+url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},

796−year = {1997}

694+volume = {21},

797−}

695+year = {1978}

798−@article{loh2010tutorial,

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

800−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},

801−journal = {Fundamenta Informaticae},

802−number = {2},

803−pages = {177--207},

804−publisher = {IOS Press},

805−title = {{A tutorial implementation of a dependently typed lambda calculus}},

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

807−volume = {102},

808−year = {2010}

809}

696}

810@book{Philosophy2012,

697@book{Philosophy2012,

811author = {Hunt, Andrew and Thomas, David},

698author = {Hunt, Andrew and Thomas, David},

812booktitle = {Carcinogenesis},

699booktitle = {Carcinogenesis},

813doi = {10.1093/carcin/bgs054},

700doi = {10.1093/carcin/bgs054},

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

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

815isbn = {020161622X},

702isbn = {020161622X},

816issn = {1460-2180},

703issn = {1460-2180},

817number = {3},

704number = {3},

@@ -820,41 +707,112 @@ title = {{The Pragmatic Programmer Chapter 1}},

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

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

821volume = {33}

708volume = {33}

822}

709}

823−@inproceedings{pollack1990implicit,

710+@inproceedings{Kimmell2012,

824−author = {Pollack, R.},

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

825−booktitle = {Informal Proceedings of First Workshop on Logical Frameworks, Antibes},

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

826−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},

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

827−publisher = {Citeseer},

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

828−title = {{Implicit syntax}},

715+year = {2012}

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

830−year = {1990}

831−}

832−@article{gordon2003authenticity,

833−author = {Gordon, A.D. and Jeffrey, A.},

834−file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

835−journal = {Journal of computer security},

836−number = {4},

837−pages = {451--520},

838−publisher = {IOS Press},

839−title = {{Authenticity by typing for security protocols}},

840−url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},

841−volume = {11},

842−year = {2003}

843}

716}

844−@inproceedings{Wadler1989,

717+@book{While2012,

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

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

846−author = {Wadler, Philip},

719+booktitle = {Carcinogenesis},

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

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

848−doi = {10.1145/99370.99404},

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

849−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},

722+isbn = {020161622X},

850−isbn = {0897913280},

723+issn = {1460-2180},

851−number = {June},

724+number = {3},

852−pages = {347--359},

725+pmid = {22383472},

726+title = {{The Pragmatic Programmer Chapter 6}},

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

728+volume = {33}

729+}

730+@inproceedings{Brady2010,

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

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

733+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},

734+isbn = {9781605587943},

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

736+mendeley-tags = {Dependent Types},

737+pages = {297--308},

853publisher = {ACM},

738publisher = {ACM},

854−series = {FPCA '89},

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

855−title = {{Theorems for free!}},

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

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

741+year = {2010}

857−year = {1989}

742+}

743+@inproceedings{Visser2008,

744+author = {Visser, E},

745+booktitle = {Generative and Transformational Techniques in Software Engineering},

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

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

748+year = {2008}

749+}

750+@misc{TheMendeleySupportTeam2011a,

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

752+address = {London},

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

754+booktitle = {Mendeley Desktop},

755+file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

756+keywords = {Mendeley,how-to,user manual},

757+pages = {1--16},

758+publisher = {Mendeley Ltd.},

759+title = {{Getting Started with Mendeley}},

760+url = {http://www.mendeley.com},

761+year = {2011}

762+}

763+@inproceedings{Brady2005a,

764+author = {Brady, E and Hammond, K},

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

766+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},

767+keywords = {Dependent Types},

768+mendeley-tags = {Dependent Types},

769+title = {{A dependently typed framework for static analysis of program execution costs}},

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

771+year = {2005}

772+}

773+@inproceedings{madhavapeddy2010turning,

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

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

776+file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},

777+publisher = {USENIX Association},

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

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

780+year = {2010}

781+}

782+@article{McBride2007,

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

784+file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},

785+journal = {Journal of functional programming},

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

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

788+year = {2007}

789+}

790+@inproceedings{bhargavan2010modular,

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

792+booktitle = {ACM Sigplan Notices},

793+number = {1},

794+pages = {445--456},

795+publisher = {ACM},

796+title = {{Modular verification of security protocol code by typing}},

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

798+volume = {45},

799+year = {2010}

800+}

801+@article{McBride2006,

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

803+journal = {Types for Proofs and Programs},

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

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

806+year = {2006}

807+}

808+@inproceedings{coquand1986analysis,

809+author = {Coquand, T.},

810+booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},

811+file = {:home/edwin/Research/Papers/Mendeley/Coquand/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},

812+pages = {227----246},

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

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

815+year = {1986}

858}

816}

859@inproceedings{Augustsson1985,

817@inproceedings{Augustsson1985,

860address = {Berlin, Heidelberg},

818address = {Berlin, Heidelberg},

@@ -872,19 +830,147 @@ url = {http://www.springerlink.com/content/y647423656557505/},

872volume = {201},

830volume = {201},

873year = {1985}

831year = {1985}

874}

832}

875−@inproceedings{Brady2005a,

833+@misc{Bloat,

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

834+author = {Brooks, Fred},

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

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

878−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},

836+isbn = {9780321702081},

837+title = {{The Design of Design Chapter 4}}

838+}

839+@inproceedings{barras2008implicit,

840+author = {Barras, B. and Bernardo, B.},

841+booktitle = {Foundations of Software Science and Computational Structures},

842+file = {:home/edwin/Research/Papers/Mendeley/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},

843+pages = {365--379},

844+publisher = {Springer},

845+title = {{The implicit calculus of constructions as a programming language with dependent types}},

846+url = {http://www.springerlink.com/index/m84h82904546l265.pdf},

847+year = {2008}

848+}

849+@misc{Brady2012c,

850+author = {Brooks, Fred},

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

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

853+isbn = {9780321702081},

854+issn = {1478-6729},

855+number = {1},

856+pages = {NP},

857+pmid = {22215642},

858+title = {{The Design of Design Chapter 5}},

859+volume = {34}

860+}

861+@inproceedings{Fournet2011,

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

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

864+file = {:home/edwin/Research/Papers/Mendeley/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},

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

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

867+year = {2010}

868+}

869+@book{Choosing2012,

870+author = {Fowler, Martin},

871+booktitle = {Carcinogenesis},

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

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

874+isbn = {9780132107549},

875+issn = {1460-2180},

876+number = {3},

877+pmid = {22383472},

878+title = {{Domain Specific Languages Chapter 6}},

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

880+volume = {33}

881+}

882+@article{mcbride2008functional,

883+author = {McBride, C. and Paterson, R.},

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

885+journal = {Journal of functional programming},

886+number = {1},

887+pages = {1--13},

888+publisher = {Cambridge Univ Press},

889+title = {{Functional pearl: Applicative programming with effects}},

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

891+volume = {18},

892+year = {2008}

893+}

894+@inproceedings{pollack1990implicit,

895+author = {Pollack, R.},

896+booktitle = {Informal Proceedings of First Workshop on Logical Frameworks, Antibes},

897+file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},

898+publisher = {Citeseer},

899+title = {{Implicit syntax}},

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

901+year = {1990}

902+}

903+@misc{altenkirch2008nσ,

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

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

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

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

908+year = {2008}

909+}

910+@misc{Abel1998,

911+author = {Abel, Andreas},

912+booktitle = {Language},

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

914+title = {{foetus - Termination Checker for Simple Functional Programs}},

915+year = {1998}

916+}

917+@misc{pollack1997believe,

918+author = {Pollack, R.},

919+file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},

920+title = {{How to believe a machine-checked proof}},

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

922+year = {1997}

923+}

924+@inproceedings{atkey2009unembedding,

925+author = {Atkey, R. and Lindley, S. and Yallop, J.},

926+booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},

927+pages = {37--48},

928+publisher = {ACM},

929+title = {{Unembedding domain-specific languages}},

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

931+year = {2009}

932+}

933+@inproceedings{oury2008power,

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

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

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

879keywords = {Dependent Types},

937keywords = {Dependent Types},

880mendeley-tags = {Dependent Types},

938mendeley-tags = {Dependent Types},

881−title = {{A dependently typed framework for static analysis of program execution costs}},

939+number = {9},

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

940+pages = {39--50},

883−year = {2005}

941+publisher = {ACM},

942+title = {{The power of Pi}},

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

944+volume = {43},

945+year = {2008}

946+}

947+@article{loh2010tutorial,

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

949+file = {:home/edwin/Research/Papers/Mendeley/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},

950+journal = {Fundamenta Informaticae},

951+number = {2},

952+pages = {177--207},

953+publisher = {IOS Press},

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

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

956+volume = {102},

957+year = {2010}

958+}

959+@article{gordon2003authenticity,

960+author = {Gordon, A.D. and Jeffrey, A.},

961+file = {:home/edwin/Research/Papers/Mendeley/Gordon, Jeffrey/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

962+journal = {Journal of computer security},

963+number = {4},

964+pages = {451--520},

965+publisher = {IOS Press},

966+title = {{Authenticity by typing for security protocols}},

967+url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},

968+volume = {11},

969+year = {2003}

884}

970}

885@article{Vytiniotis2011,

971@article{Vytiniotis2011,

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

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

887−file = {:Users/edwin/Downloads/S0956796811000098a.pdf:pdf},

973+file = {:home/edwin/Research/Papers/Mendeley/Vytiniotis et al/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions.pdf:pdf},

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

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

889number = {4--5},

975number = {4--5},

890pages = {333----412},

976pages = {333----412},

@@ -893,162 +979,207 @@ url = {http://journals.cambridge.org/abstract_S0956796811000098},

893volume = {21},

979volume = {21},

894year = {2011}

980year = {2011}

895}

981}

896−@article{mccann2000packet,

982+@misc{Attacks2012a,

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

983+author = {Anderson, Ross},

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

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

899−number = {4},

985+file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},

900−pages = {321--333},

986+isbn = {9780470068526},

901−publisher = {ACM},

987+issn = {1478-6729},

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

988+number = {1},

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

989+pages = {NP},

904−volume = {30},

990+pmid = {22215642},

905−year = {2000}

991+title = {{Security Engineering Chapter 18}},

992+volume = {34}

906}

993}

907−@article{Miller1992,

994+@inproceedings{Sheard2005,

908−author = {Miller, Dale},

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

909−file = {:Users/edwin/Documents/Papers/Miller/1992 Miller-Unification under a mixed prefix.pdf:pdf},

996+author = {Sheard, Tim},

910−journal = {Journal of Symbolic Computation},

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

911−title = {{Unification under a mixed prefix}},

998+doi = {10.1145/1088348.1088356},

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

999+file = {:home/edwin/Research/Papers/Mendeley/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},

913−year = {1992}

1000+isbn = {159593071X},

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

1002+month = sep,

1003+pages = {74--85},

1004+publisher = {ACM Press},

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

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

1007+year = {2005}

914}

1008}

915−@inproceedings{norell2009dependently,

1009+@inproceedings{NanevskiAAMorrisett2008,

916−author = {Norell, Ulf},

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

917−booktitle = {Advanced Functional Programming},

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

918−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

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

1013+doi = {10.1145/1411204.1411237},

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

1015+isbn = {9781595939197},

1016+issn = {15232867},

919keywords = {Dependent Types},

1017keywords = {Dependent Types},

920mendeley-tags = {Dependent Types},

1018mendeley-tags = {Dependent Types},

921−pages = {230--266},

1019+number = {9},

922−publisher = {Springer},

1020+pages = {229--240},

923−title = {{Dependently typed programming in Agda}},

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

924−url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},

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

925−year = {2009}

1023+volume = {43},

1024+year = {2008}

926}

1025}

927−@article{Hughes1989,

1026+@inproceedings{fisher2005pads,

928−abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},

1027+author = {Fisher, K. and Gruber, R.},

929−author = {Hughes, J},

1028+booktitle = {ACM SIGPLAN Notices},

930−chapter = {2},

1029+number = {6},

931−doi = {10.1093/comjnl/32.2.98},

1030+pages = {295--304},

932−editor = {Turner, David A},

1031+publisher = {ACM},

933−file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},

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

934−institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},

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

935−isbn = {0201172364},

1034+volume = {40},

936−issn = {00104620},

1035+year = {2005}

937−journal = {The Computer Journal},

938−number = {2},

939−pages = {98--107},

940−publisher = {Br Computer Soc},

941−title = {{Why Functional Programming Matters}},

942−url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},

943−volume = {32},

944−year = {1989}

945}

1036}

946−@article{Steiner1988,

1037+@inproceedings{McBride2004b,

947−author = {Steiner, JG},

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

948−file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

1039+booktitle = {Haskell Workshop},

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

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

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

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

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

1042+year = {2004}

952−year = {1988}

953}

1043}

954−@phdthesis{McBride1999,

1044+@article{marlow2006making,

955−author = {McBride, Conor},

1045+author = {Marlow, S. and {Peyton Jones}, S.},

956−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

1046+file = {:home/edwin/Research/Papers/Mendeley/Marlow, Peyton Jones/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},

957−keywords = {Dependent Types},

1047+journal = {Journal of Functional Programming},

958−mendeley-tags = {Dependent Types},

1048+number = {4-5},

959−school = {University of Edinburgh},

1049+pages = {415--449},

960−title = {{Dependently typed functional programs and their proofs}},

1050+publisher = {Cambridge University Press},

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

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

962−year = {1999}

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

1053+volume = {16},

1054+year = {2006}

963}

1055}

964−@inproceedings{augustsson1999exercise,

1056+@article{landin1966next,

965−author = {Augustsson, L. and Carlsson, M.},

1057+author = {Landin, P.J.},

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

1058+file = {:home/edwin/Research/Papers/Mendeley/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},

967−keywords = {Depe},

1059+journal = {Communications of the ACM},

968−mendeley-tags = {Depe},

1060+number = {3},

969−publisher = {Citeseer},

1061+pages = {157--166},

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

1062+publisher = {ACM},

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

1063+title = {{The next 700 programming languages}},

972−year = {1999}

1064+url = {http://dl.acm.org/citation.cfm?id=365257 )},

1065+volume = {9},

1066+year = {1966}

973}

1067}

974−@inproceedings{taha2004gentle,

1068+@misc{Protocols2012a,

975−author = {Taha, W.},

1069+author = {Anderson, Ross},

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

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

977−pages = {30--50},

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

978−publisher = {Springer},

1072+isbn = {9780470068526},

979−title = {{A gentle introduction to multi-stage programming}},

1073+issn = {1478-6729},

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

1074+pmid = {22215642},

981−year = {2004}

1075+title = {{Security Engineering Chapter 3}}

982}

1076}

983@inproceedings{Sculthorpe2009,

1077@inproceedings{Sculthorpe2009,

984author = {Sculthorpe, Neil and Nilsson, Henrik},

1078author = {Sculthorpe, Neil and Nilsson, Henrik},

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

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

986−file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},

1080+file = {:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf;:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf},

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

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

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

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

989year = {2009}

1083year = {2009}

990}

1084}

991−@misc{TheMendeleySupportTeam2011a,

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

993−address = {London},

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

995−booktitle = {Mendeley Desktop},

996−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

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

998−pages = {1--16},

999−publisher = {Mendeley Ltd.},

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

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

1002−year = {2011}

1003−}

1004−@article{danielsson2011parsing,

1005−author = {Danielsson, N. and Norell, U.},

1006−journal = {Implementation and Application of Functional Languages},

1007−pages = {80--99},

1008−publisher = {Springer},

1009−title = {{Parsing mixfix operators}},

1010−url = {http://www.springerlink.com/index/386243257W504252.pdf},

1011−year = {2011}

1012−}

1013−@misc{dagand2011transporting,

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

1015−file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

1016−title = {{Transporting Functions across Ornaments}},

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

1018−year = {2011}

1019−}

1020@book{Fowler,

1085@book{Fowler,

1021author = {Fowler, Martin},

1086author = {Fowler, Martin},

1022booktitle = {Language},

1087booktitle = {Language},

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

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

1024isbn = {9780132107549},

1089isbn = {9780132107549},

1025title = {{Domain Specific Languages Chapter 2}}

1090title = {{Domain Specific Languages Chapter 2}}

1026}

1091}

1027−@misc{Bove2008,

1092+@article{Jones2003,

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

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

1029−author = {Bove, Ana and Dybjer, Peter},

1094+author = {Jones, Simon Peyton},

1030−booktitle = {Notes},

1095+editor = {Jones, Simon Peyton},

1031−doi = {10.1007/978-3-642-03153-3_2},

1096+isbn = {0521826144},

1032−file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},

1097+journal = {Language},

1033−number = {February},

1098+number = {1},

1034−pages = {57--99},

1099+publisher = {Cambridge University Press},

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

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

1102+volume = {13},

1103+year = {2003}

1104+}

1105+@article{Brady2006a,

1106+author = {Brady, E and Hammond, K},

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

1108+journal = {\ldots of the 5th international conference on \ldots},

1109+keywords = {Dependent Types},

1110+mendeley-tags = {Dependent Types},

1111+title = {{A verified staged interpreter is a verified compiler}},

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

1113+year = {2006}

1114+}

1115+@article{burrows1990,

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

1117+file = {:home/edwin/Research/Papers/Mendeley/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

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

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

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

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

1122+volume = {8},

1123+year = {1990}

1124+}

1125+@phdthesis{McBride1999,

1126+author = {McBride, Conor},

1127+file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

1128+keywords = {Dependent Types},

1129+mendeley-tags = {Dependent Types},

1130+school = {University of Edinburgh},

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

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

1133+year = {1999}

1134+}

1135+@article{mcbride2010ornamental,

1136+author = {McBride, Conor},

1137+file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},

1138+journal = {Journal of Functional Programming},

1139+title = {{Ornamental algebras, algebraic ornaments}},

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

1141+year = {2010}

1142+}

1143+@inproceedings{czarnecki2004dsl,

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

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

1146+file = {:home/edwin/Research/Papers/Mendeley/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},

1147+pages = {51--72},

1035publisher = {Springer},

1148publisher = {Springer},

1036−title = {{Dependent Types at Work}},

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

1037−url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},

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

1038−volume = {5520},

1151+year = {2004}

1039−year = {2008}

1152+}

1153+@article{Chapman2005epigram,

1154+author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},

1155+file = {:home/edwin/Research/Papers/Mendeley/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},

1156+journal = {Trends in Functional Programming},

1157+publisher = {Intellect Books},

1158+title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},

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

1160+year = {2005}

1040}

1161}

1041−@article{Okasaki1993,

1162+@inproceedings{Levitation2010,

1042−author = {Okasaki, Chris},

1163+author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

1043−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

1164+booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},

1044−journal = {Journal of functional programming},

1165+doi = {10.1145/1932681.1863547},

1045−title = {{Red-Black Trees in A Functional Setting}},

1166+file = {:home/edwin/Research/Papers/Mendeley/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},

1046−year = {1993}

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

1168+issn = {03621340},

1169+keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

1170+mendeley-tags = {Dependent Types},

1171+month = sep,

1172+number = {9},

1173+pages = {3},

1174+title = {{The gentle art of levitation}},

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

1176+volume = {45},

1177+year = {2010}

1047}

1178}

1048@inproceedings{pj2006gadts,

1179@inproceedings{pj2006gadts,

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

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

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

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

1051−file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},

1182+file = {:home/edwin/Research/Papers/Mendeley/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},

1052number = {9},

1183number = {9},

1053pages = {50--61},

1184pages = {50--61},

1054publisher = {ACM},

1185publisher = {ACM},

@@ -1057,56 +1188,11 @@ url = {http://dl.acm.org/citation.cfm?id=1159811},

1057volume = {41},

1188volume = {41},

1058year = {2006}

1189year = {2006}

1059}

1190}

1060−@misc{altenkirch2005dependent,

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

1062−booktitle = {Manuscript, available online},

1063−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

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

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

1066−year = {2005}

1067−}

1068−@misc{The2012c,

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

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

1071−file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

1072−isbn = {9780596529833},

1073−issn = {1478-6729},

1074−pmid = {22215642},

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

1076−}

1077−@misc{Resolution2012a,

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

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

1080−file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

1081−issn = {1478-6729},

1082−pmid = {22215642},

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

1084−}

1085−@article{Brady2006a,

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

1087−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

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

1089−keywords = {Dependent Types},

1090−mendeley-tags = {Dependent Types},

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

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

1093−year = {2006}

1094−}

1095−@inproceedings{swierstra2007beauty,

1096−author = {Swierstra, W. and Altenkirch, T.},

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

1098−file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra, Altenkirch/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},

1099−pages = {25--36},

1100−publisher = {ACM},

1101−title = {{Beauty in the beast}},

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

1103−year = {2007}

1104−}

1105@article{McBride2004a,

1191@article{McBride2004a,

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

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

1107author = {McBride, Conor and McKinna, James},

1193author = {McBride, Conor and McKinna, James},

1108doi = {10.1017/S0956796803004829},

1194doi = {10.1017/S0956796803004829},

1109−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

1195+file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

1110issn = {09567968},

1196issn = {09567968},

1111journal = {Journal of Functional Programming},

1197journal = {Journal of Functional Programming},

1112keywords = {Dependent Types},

1198keywords = {Dependent Types},

@@ -1119,153 +1205,80 @@ url = {http://www.journals.cambridge.org/abstract_S0956796803004829},

1119volume = {14},

1205volume = {14},

1120year = {2004}

1206year = {2004}

1121}

1207}

1122−@misc{Nodes2012a,

1208+@article{Altenkirch2010a,

1123−author = {Brooks, Fred},

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

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

1210+author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},

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

1211+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},

1126−isbn = {9780321702081},

1212+journal = {Citeseer},

1127−issn = {1478-6729},

1128−pmid = {22215642},

1129−title = {{The Design of Design Chapter 3}}

1130−}

1131−@inproceedings{augustsson2008paradise,

1132−author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},

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

1134−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},

1135−number = {9},

1136−pages = {225--228},

1137−publisher = {ACM},

1138−title = {{Paradise: a two-stage DSL embedded in Haskell}},

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

1140−volume = {43},

1141−year = {2008}

1142−}

1143−@misc{Abel1998,

1144−author = {Abel, Andreas},

1145−booktitle = {Language},

1146−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

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

1148−year = {1998}

1149−}

1150−@article{Jones1999,

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

1152−author = {Jones, Mark P},

1153−journal = {October},

1154publisher = {Citeseer},

1213publisher = {Citeseer},

1155−title = {{Typing Haskell in Haskell}},

1214+title = {{Generic Programming with Dependent Types}},

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

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

1157−year = {1999}

1216+year = {2010}

1158−}

1159−@inproceedings{morris2006exploring,

1160−author = {Morris, P. and Altenkirch, T. and McBride, C.},

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

1162−file = {:Users/edwin/Documents/Mendeley Desktop/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

1163−pages = {252--267},

1164−publisher = {Springer},

1165−title = {{Exploring the regular tree types}},

1166−url = {http://www.springerlink.com/index/f9p1317716614834.pdf},

1167−year = {2006}

1168−}

1169−@inproceedings{Sheard2005,

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

1171−author = {Sheard, Tim},

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

1173−doi = {10.1145/1088348.1088356},

1174−file = {:Users/edwin/Documents/Mendeley Desktop/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},

1175−isbn = {159593071X},

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

1177−month = sep,

1178−pages = {74--85},

1179−publisher = {ACM Press},

1180−title = {{Putting curry-howard to work}},

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

1182−year = {2005}

1183−}

1184−@misc{Interface2012a,

1185−author = {Kreibich, Jay A.},

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

1187−file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

1188−isbn = {9781449394592},

1189−issn = {1478-6729},

1190−pmid = {22215642},

1191−title = {{Using SQLite Chapter 7}}

1192}

1217}

1193−@book{The2012,

1218+@article{Steiner1988,

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

1219+author = {Steiner, JG},

1195−booktitle = {Carcinogenesis},

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

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

1221+journal = {Proc. Winter USENIX Conference},

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

1222+title = {{Kerberos: An authentication service for open network systems}},

1198−isbn = {020161622X},

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

1199−issn = {1460-2180},

1224+year = {1988}

1200−number = {3},

1201−pmid = {22383472},

1202−title = {{The Pragmatic Programmer Chapter 3}},

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

1204−volume = {33}

1205}

1225}

1206−@misc{Brady2012b,

1226+@phdthesis{Okasaki1996,

1207−author = {Brooks, Fred},

1227+author = {Okasaki, Chris},

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

1228+file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},

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

1229+school = {Carnegie Mellon University},

1210−isbn = {9780321702081},

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

1211−issn = {1478-6729},

1231+year = {1996}

1212−pmid = {22215642},

1213−title = {{The Design of Design Chapter 2}}

1214}

1232}

1215−@inproceedings{Levitation2010,

1233+@article{Abel2010,

1216−author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

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

1217−booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},

1235+author = {Abel, Andreas},

1218−doi = {10.1145/1932681.1863547},

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

1219−file = {:Users/edwin/Documents/Mendeley Desktop/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},

1237+journal = {EPTCS},

1220−isbn = {978-1-60558-794-3},

1238+pages = {1--15},

1221−issn = {03621340},

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

1222−keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

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

1223−mendeley-tags = {Dependent Types},

1241+volume = {43},

1224−month = sep,

1225−number = {9},

1226−pages = {3},

1227−title = {{The gentle art of levitation}},

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

1229−volume = {45},

1230year = {2010}

1242year = {2010}

1231}

1243}

1232−@inproceedings{Xi1999,

1244+@inproceedings{Brady2006b,

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

1245+author = {Brady, Edwin},

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

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

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

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

1236−doi = {10.1145/292540.292560},

1248+isbn = {978-3-540-74129-9},

1237−file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},

1249+month = sep,

1238−isbn = {1581130953},

1250+pages = {145----162},

1239−issn = {07439016},

1251+title = {{Ivor, a proof engine}},

1240−keywords = {Dependent Types},

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

1241−mendeley-tags = {Dependent Types},

1253+year = {2006}

1242−organization = {Carnegie Mellon University},

1243−pages = {214--227},

1244−publisher = {ACM Press},

1245−series = {POPL '99},

1246−title = {{Dependent types in practical programming}},

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

1248−volume = {26},

1249−year = {1999}

1250}

1254}

1251−@inproceedings{Brady2003,

1255+@article{Hughes1989,

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

1256+abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},

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

1257+author = {Hughes, J},

1254−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},

1258+chapter = {2},

1255−keywords = {Dependent Types},

1259+doi = {10.1093/comjnl/32.2.98},

1256−mendeley-tags = {Dependent Types},

1260+editor = {Turner, David A},

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

1261+file = {:home/edwin/Research/Papers/Mendeley/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},

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

1262+institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},

1259−year = {2003}

1263+isbn = {0201172364},

1264+issn = {00104620},

1265+journal = {The Computer Journal},

1266+number = {2},

1267+pages = {98--107},

1268+publisher = {Br Computer Soc},

1269+title = {{Why Functional Programming Matters}},

1270+url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},

1271+volume = {32},

1272+year = {1989}

1260}

1273}

1261−@inproceedings{fisher2005pads,

1274+@article{mccann2000packet,

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

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

1263−booktitle = {ACM SIGPLAN Notices},

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

1264−number = {6},

1277+number = {4},

1265−pages = {295--304},

1278+pages = {321--333},

1266publisher = {ACM},

1279publisher = {ACM},

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

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

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

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

1269−volume = {40},

1282+volume = {30},

1270−year = {2005}

1283+year = {2000}

1271}

1284}

impl-paper/typechecking.tex+10−11

@@ -479,6 +479,14 @@ This approach, separating the termination requirement from the type theory, mean

479an \Idris{} programmer makes the decision about the importance of totality for each

480function rather than having the totality requirement imposed by the type theory.

481

482+\subsection{\TT{} examples}

483+

484+\todo[inline]{

485+\TT{} as a more general purpose intermediate language --- superset of System $\mathcal{F}$

486+for example. Primitive operators. A couple of example programs (derived from high

487+level examples in e.g. ML?).

488+}

489+

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

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

483

491

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

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

@@ -498,22 +506,13 @@ features of the high level language.

498

506

499\subsubsection{Example Elaboration}

507\subsubsection{Example Elaboration}

500

508

501−Consider the following \Idris{} function:

509+Recall the following \Idris{} function:

502−

503−\begin{SaveVerbatim}{vadd}

504

510

505−vAdd : Num a => Vect a n -> Vect a n -> Vect a n

506−vAdd [] [] = []

507−vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

508−

509−\end{SaveVerbatim}

510\useverb{vadd}

511\useverb{vadd}

511

512

512\noindent

513\noindent

513−This adds corresponding elements of vectors of the same length. The vectors can contain

514+In order to elaborate

514−any numeric type, overloaded using the \texttt{Num} type class. In order to elaborate

515this to \TT{}, we must resolve the implicit arguments, and make the type class explicit.

516−

517The first step is to make the implicit arguments explicit, using a placeholder

516The first step is to make the implicit arguments explicit, using a placeholder

518to stand for the arguments we have not yet resolved. The type class argument is

517to stand for the arguments we have not yet resolved. The type class argument is

519also treated as an implicit argument, to which we give the name \texttt{c}:

518also treated as an implicit argument, to which we give the name \texttt{c}: