From a3569e57bb1a2a8c4cb7179dc797b2122ac4f8b9 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 8 Apr 2012 19:28:53 +0100 Subject: [PATCH] Some proofreading, filling in some gaps. --- impl-paper/Makefile | 2 +- impl-paper/conclusions.tex | 14 + impl-paper/elaboration.tex | 85 +- impl-paper/hll.tex | 55 +- impl-paper/impldtp.tex | 16 +- impl-paper/intro.tex | 6 +- impl-paper/library.bib | 1656 +++++++++++++++++------------------ impl-paper/typechecking.tex | 59 +- 8 files changed, 993 insertions(+), 900 deletions(-) diff --git a/impl-paper/Makefile b/impl-paper/Makefile index 903e9ac018..aaa0ab9f15 100644 --- a/impl-paper/Makefile +++ b/impl-paper/Makefile @@ -3,7 +3,7 @@ PAPER = impldtp all: ${PAPER}.pdf .PHONY TEXFILES = ${PAPER}.tex intro.tex conclusions.tex hll.tex\ - typechecking.tex elaboration.tex compiling.tex\ + typechecking.tex elaboration.tex \ syntax.tex DIAGS = diff --git a/impl-paper/conclusions.tex b/impl-paper/conclusions.tex index e3255c1436..a07f8fca23 100644 --- a/impl-paper/conclusions.tex +++ b/impl-paper/conclusions.tex @@ -2,6 +2,13 @@ \section{Discussion} \label{sect:discussion} +Since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it makes +sense to expose the tactic language to the programmer. +Also tactic-implicit arguments as a generalisation of instance resolution. + +Discuss performance (anecdotally, how big is the library and how long to check, +and relative to previous version). + \subsection{Related Work} Oleg~\cite{McBride1999} as inspiration. \Epigram{}~\cite{McBride2004a}. @@ -17,4 +24,11 @@ \subsection{Conclusion} Elaboration is effectively a type checker for the high level language, so we have a hope of providing reasonable error messages related to the original code.] + \subsection{Further Work} + +[Would the EDSL approach work in other languages? Adding components of DTP +to imperative languages, say, using \TT{} as a verified core. +\Idris{} implementation as the beginning of a project to explore practical +DTP --- systems, protocols, security especially. And just having full +dependent types for lightweight correctness guarantees.] diff --git a/impl-paper/elaboration.tex b/impl-paper/elaboration.tex index 29982c92bd..3974c72fe5 100644 --- a/impl-paper/elaboration.tex +++ b/impl-paper/elaboration.tex @@ -9,8 +9,7 @@ \section{Elaborating \Idris{}} high level declarations are translated into a \TT{} program consisting of inductive families and pattern matching function definitions. We will need to work at the \remph{declaration} level, and at the \remph{expression} level, -defining the following meta-operations which together constitute an algorithm -for elaborating \Idris{} programs to \TT{}. +defining the following meta-operations. \begin{itemize} \item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression. @@ -90,10 +89,10 @@ \subsection{Proof State} The \remph{hole queue} is a priority queue of names of hole and guess binders $\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$ in the proof term --- -we ensure that each bound name is unique. Holes essentially refer to \remph{sub goals} +ensuring that each bound name is unique. Holes refer to \remph{sub goals} in the proof. When this queue is empty, the proof term is complete. -Creating a \TT{} expression from an \Idris{} expresson involves creating +Creating a \TT{} expression from an \Idris{} expression involves creating a new proof state, with an empty proof term, and using the high level definition to direct the building of a final proof state, with a complete proof term. @@ -162,7 +161,8 @@ \subsection{System State} \item Type class instances, $\vI$, containing dictionaries for type classes \end{itemize} -In the implementation, the system state is captured in a monad, \texttt{Idris}, and +In the implementation, the system state is captured in a monad, \texttt{Idris}, +which also wraps the current proof state. This monad includes additional information such as syntax overloadings, command line options, and optimisations, which do not concern us here. Elaboration of expressions requires access to the system state in particular in order to expand @@ -226,7 +226,7 @@ \subsection{Tactics} if it cannot find such values. If successful, $\MO{Unify}$ will update the proof state. \end{itemize} -\remph{Tactics} are specifically meta-operations which operate on the sub-term given +\demph{Tactics} are meta-operations which operate on the sub-term given by the hole at the head of the hole queue in the proof state. They take the following form: \DM{ @@ -264,7 +264,8 @@ \subsubsection{Creating and destroying holes} An obvious difficulty is in ensuring that names are unique throughout a proof term. In the implementation, we ensure that any hole created by the $\MO{Claim}$ tactic -has a unique name. In this paper, we will assume that all names are fresh. +has a unique name by checking against existing names in scope and modifying +the name if necessary. In this paper, we will assume that all created names are fresh. The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to @@ -445,7 +446,8 @@ \subsubsection{Example} We can build $\FN{id}$ either as a complete term, or by applying a sequence of tactics. To achieve this, we create a proof state initialised with the type of $\FN{id}$ and -apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$: +apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using $\MO{RunTac}$. +Note that the types on each $\MO{Lambda}$ are solved by unification: \DM{ \AR{ @@ -466,7 +468,9 @@ \subsubsection{Example} } To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate -sequencing. Using this convention, we can build $\FN{id}$'s type and definition as shown +sequencing --- in the implementation we use wrapper functions for each tactic to +apply $\MO{RunTac}$. +Using this convention, we can build $\FN{id}$'s type and definition as shown in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term. Note in particular that each $\MO{Attack}$ and each $\MO{Fill}$, which create new guesses, @@ -566,8 +570,6 @@ \subsection{Elaborating Expressions} \va :: = & \ve & (\mbox{normal argument}) \\ \mid & \iarg{\vx}{\ve} & (\mbox{implicit argument with value}) \\ \mid & \carg{\ve} & (\mbox{explicit class instance}) -\medskip\\ -\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\ \end{array} \medskip\\ \begin{array}{rll} @@ -645,11 +647,11 @@ \subsection{Elaborating Expressions} %it's the global name after all and we do that by type). To elaborate expressions, we define a meta-operation $\ttinterp{\cdot}$ which -runs relative to a proof state (see Section \ref{sect:prfstate}. Its effect is +runs relative to a proof state (see Section \ref{sect:prfstate}). Its effect is to update the proof state so that the hole in focus contains a representation of the given expression, by applying tactics. We assume that the proof state has already been set up, which means that elaboration can always be -\remph{type-directed}. The proof state contains the type of the expression we +\remph{type-directed} since the proof state contains the type of the expression we are building. \subsubsection{Elaborating variables and constants} @@ -689,11 +691,13 @@ \subsubsection{Elaborating variables and constants} } On encountering a placeholder, our assumption is that unification will eventually solve -the hole. +the hole. At the end of elaboration, any holes remaining unsolved on the left hand side +become pattern variables. If there are any unsolved on the right hand side, elaboration +fails. \subsubsection{Elaborating bindings} -To elaborate a $\lambda$ binding, we $\MO{Attack}$ the hole, which must be a function type, +To elaborate a $\lambda$-binding, we $\MO{Attack}$ the hole, which must be a function type, apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges the $\MO{Attack}$: @@ -843,7 +847,8 @@ \subsubsection{Elaborating applications} The $\MO{Instance}$ tactic focuses on the given hole and searches the context for a type class instance which would solve the goal directly. First, it examines the local -context, then recursively searches the global context. +context, then recursively searches the global context. $\MO{Instance}$ is covered +in detail in Section \ref{sect:instance}. To elaborate a simple function application, of an arbitrary expression to an arbitrary argument, we need not worry about implicit arguments or class constraints. Instead, @@ -929,19 +934,20 @@ \subsubsection{Elaborating Data Types} \subsubsection{Elaborating Pattern Matching} -[Work clause by clause, $\MO{ElabClause}$ returns a left and right hand side, and -may have the side effect of adding things to the context, such as definitions in -$\iwhere$ clauses. Collect together in a full definition at the end. - -In the simplest case, no $\iwhere$ clause:] +To elaborate a pattern matching definition, we work clause by clause, elaborating +the left and right hand sides in turn. $\MO{ElabClause}$ returns the elaborated +left and right hand sides, and may have the side effect of adding entries +to the global context, such as definitions in $\iwhere$ clauses. +First, let us consider the simplest case, with no $\iwhere$ clause: \DM{ \MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:? } How do we elaborate the left hand side, given that elaboration is type directed, and -we do not know its type until after we have elaborated it? The easiest way, which -requires no change to the elaborator, is to define a type $\TC{Infer}$: +we do not know its type until after we have elaborated it? +We can achieve this without any change to the elaborator by defining +a type $\TC{Infer}$: \DM{ \Data\hg\TC{Infer}\Hab\Set\hg\Where\hg\DC{MkInfer}\Hab\all{\va}{\Set}\SC\va\to\TC{Infer} @@ -978,7 +984,7 @@ \subsubsection{Elaborating Pattern Matching} \MO{Elab}\:\vec{\VV{pclause}}\:\mq\: \edo{ \tc\gets\vec{\MO{ElabClause}}\:\vec{\VV{pclause}}\\ -\MO{TTDecl}\:\tc +\vec{\MO{TTDecl}}\:\tc } } } @@ -1189,6 +1195,7 @@ \subsubsection{Elaborating Class and Instance Declarations} \end{SaveVerbatim} \useverb{ordparent} +\noindent In general, we elaborate \texttt{class} declarations as follows: \DM{ @@ -1201,7 +1208,13 @@ \subsubsection{Elaborating Class and Instance Declarations} \MO{Elab}\: \AR{(\RW{data}\:\TC{C}\Hab(\ta\Hab\ttt)\to\Set\:\iwhere\\ \hg\DC{InstanceC}\Hab\piconst{\tc}\td\to\TC{C}\:\ta)} -\\ +} +} +} + +\DM{ +\AR{ +\AR{ \vec{\MO{ElabMeth}}\:\vec{\VV{meth}}\:\td\\ \vec{\MO{ElabParent}}\:\tc } @@ -1220,6 +1233,7 @@ \subsubsection{Elaborating Class and Instance Declarations} } } +\noindent Then we elaborate \texttt{instance} declarations as follows: \DM{ @@ -1242,12 +1256,12 @@ \subsubsection{Elaborating Class and Instance Declarations} Adding default definitions is straightforward: simply insert the default definition where there is a method missing in an \texttt{instance} declaration. -[Key point: we've added a higher level language construct simply by elaborating in terms of -a lower level language construct. In particular, we don't need to worry about type -class \remph{resolution}, because we have a tactic to do that. -We can build a lot of extensions this way because we -have effectively built, bottom up, an Embedded Domain Specific Language for constructing -programs in \TT{}.] +\textbf{Remark:} Here, we have added a higher level language construct (type +classes) simply by elaborating in terms of lower level language constructs +(data types and functions). We achieve type class resolution by implementing a +tactic, $\MO{Instance}$. We can build several extensions this way because we +have effectively built, bottom up, an Embedded Domain Specific Language for +constructing programs in \TT{}. \subsubsection{The $\MO{Instance}$ tactic} @@ -1356,6 +1370,8 @@ \subsection{Syntax Extensions} \ve ::= & \ldots \\ \mid & \mvar{\vx} & (\mbox{metavariable}) & \mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) \\ +\medskip\\ +\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\ \end{array} } } @@ -1412,7 +1428,7 @@ \subsubsection{Metavariables} \edo{ (\tv\Hab\ttt)\gets\MO{Context}\\ \vT\gets\MO{Type}\\ -\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vt)\\ +\MO{TTDecl}\:(\vx\Hab(\tv\Hab\ttt)\to\vT)\\ \ttinterp{\vx\:\tv} } } @@ -1422,7 +1438,7 @@ \subsubsection{\texttt{case} expressions} A \texttt{case} expression allows pattern matching on intermediate values. The difficulty in elaborating \texttt{case} expressions is that \TT{} allows matching only on \emph{top level} values. To elaborate a \texttt{case} expression, therefore, -we create a new top level function standing for the expression, and call it. The natural +we create a new top level function standing for the expression, and apply it. The natural way to implement this is to use a metavariable. For example, we have already seen \texttt{lookup\_default}: @@ -1466,6 +1482,9 @@ \subsubsection{\texttt{case} expressions} Language for describing elaboration, we have been able to implement a new higher level language feature in terms of elaboration of lower level language features. +%\subsubsection{Tactic-implicit arguments} + + %\subsubsection{Pairs and Dependent Pairs} % Other extensions: do notation, idiom brackets, pairs, etc, are easily expressed diff --git a/impl-paper/hll.tex b/impl-paper/hll.tex index 5cfcb49b24..7af189e0b7 100644 --- a/impl-paper/hll.tex +++ b/impl-paper/hll.tex @@ -4,7 +4,7 @@ \section{\Idris{} --- the High Level Language} \Idris{} is a pure functional programming language with dependent types. It is -eagerly evaluted by default, and is compiled via the Epic supercombinator +eagerly evaluted by default, and compiled via the Epic supercombinator library \cite{brady2011epic}. In this section, I will give a brief introduction to programming in \Idris{}, covering the most important features. A full tutorial is available elsewhere @@ -75,7 +75,8 @@ \subsection{Types and Functions} \end{SaveVerbatim} \useverb{infixcons} -\noindent +This declares that \texttt{::} is a right associative operator (\texttt{infixr}) +with a precedence level of 10. Functions, data constructors and type constuctors may all be given infix operators as names. They may be used in prefix form if enclosed in brackets, e.g. \tDC{(::)}. @@ -105,10 +106,11 @@ \subsection{Functions} The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded for use by \texttt{Nat}, and are implemented using the above functions. Unlike Haskell, there is no restriction on whether -types and function names must begin with a capital letter or not. Function -names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S}, -\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are -all part of the same namespace. +types and function names must begin with a capital letter or not. +%Function +%names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S}, +%\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are +%all part of the same namespace. \Idris{} has an interactive prompt, at which we can test these functions: @@ -160,7 +162,8 @@ \subsubsection{\texttt{where} clauses} \textbf{Scope:} Any names which are visible in the outer scope are also visible in the \texttt{where} clause (unless they have been redefined, such as \texttt{xs} here). -\emph{However}, names which appear in the type are \emph{not} in scope. In particular, +\emph{However}, names which appear in the type are \emph{not} automatically +in scope. In particular, in the above example, the \texttt{a} in the top level type and the \texttt{a} in the auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required behaviour, the \texttt{a} can be brought into scope as follows: @@ -178,7 +181,8 @@ \subsubsection{\texttt{where} clauses} \subsubsection{Dependent Types} A standard example of a dependent type is the type of ``lists with length'', -conventionally called ``vectors''. In \Idris{}, we declare vectors as follows: +conventionally called ``vectors'' in the dependently typed programming +literature. In \Idris{}, we declare vectors as follows: \begin{SaveVerbatim}{vect} @@ -196,7 +200,7 @@ \subsubsection{Dependent Types} Ambiguous constructor names are resolved by type. This declares a family of types, which requires a different form of declaration -different from the simple type declarations above. It resembles a Haskell GADT +from the simple type declarations above. It resembles a Haskell GADT declaration: we explicitly state the type of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect} @@ -293,6 +297,17 @@ \subsubsection{Implicit Arguments} \texttt{n} and \texttt{a}, which are not declared explictly. These are \emph{implicit} arguments to \texttt{index}. We could also write the type of \texttt{index} as: +\begin{SaveVerbatim}{vindeximppl} + +index : {a:_} -> {n:_} -> Fin n -> Vect a n -> a + +\end{SaveVerbatim} +\useverb{vindeximppl} + +\noindent +Here we have given bindings for \texttt{a} and \texttt{n} with placeholders for +their types, to be inferred by the machine. We could also give the types explicitly: + \begin{SaveVerbatim}{vindeximpty} index : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a @@ -339,11 +354,14 @@ \subsection{Type Classes} can be overloaded in an ad-hoc manner and resolved according to the context in which they are used. This is mostly for convenience, to eliminate the need to decorate constructor names in similarly structured data types, and eliminate explicit qualification -of ambiguous names where only one is well-typed. +of ambiguous names where only one is well-typed --- this is especially useful +for disambiguating record field names\footnote{Records are however beyond the scope +of this paper}. -Secondly, \Idris{} implements \remph{type classes}. This allows a more principled approach -to overloading --- a type class gives a collection of overloaded operations which describe -the interface for \remph{instances} of that class. +Secondly, \Idris{} implements \remph{type classes}, following Haskell. This +allows a more principled approach to overloading --- a type class gives a +collection of overloaded operations which describe the interface for +\remph{instances} of that class. A simple example is the \texttt{Show} type class, which is defined in the library and @@ -380,11 +398,16 @@ \subsection{Type Classes} show O = "O" show (S k) = "s" ++ show k +\end{SaveVerbatim} +\useverb{shownat} + +\begin{SaveVerbatim}{shownati} + Idris> show (S (S (S O))) "sssO" : String \end{SaveVerbatim} -\useverb{shownat} +\useverb{shownati} \noindent Only one instance of a class can be given for a type --- instances may not overlap. @@ -473,7 +496,7 @@ \subsubsection{\texttt{let} bindings} \useverb{letb} \noindent -We can also do simple pattern matching in \texttt{let} bindings. For example, we can extract +We can also pattern match in \texttt{let} bindings. For example, we can extract fields from a record as follows, as well as by pattern matching at the top level: \begin{SaveVerbatim}{letp} @@ -507,7 +530,7 @@ \subsubsection{\texttt{case} expressions} pair it returns, and remove the first character of the second string. A \texttt{case} expression can match several cases, for example, to inspect an -intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which +intermediate value of type \texttt{Maybe a}. For example, \texttt{list\_lookup} looks up an index in a list, returning \texttt{Nothing} if the index is out of bounds. We can use this to write \texttt{lookup\_default}, which looks up an index and returns a default value if the index is out of bounds: diff --git a/impl-paper/impldtp.tex b/impl-paper/impldtp.tex index a112aefc54..264bab726c 100644 --- a/impl-paper/impldtp.tex +++ b/impl-paper/impldtp.tex @@ -67,9 +67,9 @@ \begin{abstract} Many components of a dependently typed programming language are by now well -understood, such as the underlying type theory, type checking, unification and +understood, for example the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high -level language is, however, folklore, discovered anew by each succesive +level language is, however, folklore, discovered anew by succesive language implementations. In this paper, I describe the implementation of a new dependently typed functional programming language, \Idris{}. \Idris{} is intended to be a \emph{general purpose} programming language @@ -127,14 +127,14 @@ \appendix -\section{Elaboration meta-operations} +%\section{Elaboration meta-operations} -It's possible that it would be useful to have a quick reference of meta-operations -used by the elaborator here. +%It's possible that it would be useful to have a quick reference of meta-operations +%used by the elaborator here. -They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$, -$\MO{NewProof}$, $\MO{NewTerm}$, -$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$. +%They are: $\ttinterp{\cdot}$, $\MO{Elab}$, $\MO{TTDecl}$, +%$\MO{NewProof}$, $\MO{NewTerm}$, +%$\MO{Term}$, $\MO{Type}$, $\MO{Context}$, $\MO{Patterns}$, $\MO{Lift}$, $\MO{Expand}$. %\input{code} diff --git a/impl-paper/intro.tex b/impl-paper/intro.tex index 8f3e8f8690..a9facd0ea0 100644 --- a/impl-paper/intro.tex +++ b/impl-paper/intro.tex @@ -50,11 +50,13 @@ \subsection{Overview} high level dependently typed programming language to a small core type theory, \TT{}, based on UTT \cite{luo1994}. The paper describes the structure of the EDSL including proof and system state, and introduces a collection of \remph{tactics} -for manipulating incompete programs. +for manipulating incomplete programs. Secondly, the paper gives a detailed description of the core type theory used by \Idris{}, including a full description of the typing rules. Finally, through describing the EDSL and the specific tactics, the paper shows how to extend \Idris{} with higher level features. +While we apply these ideas to \Idris{} specifically, the method for term construction +is equally applicable to other typed programming languages. The paper is structured as follows: In Section \ref{sect:hll} I give an overview of programming in \Idris{}, introducing the high level constructs which will be @@ -68,7 +70,7 @@ \subsection{Overview} \subsection{Typographical conventions} -This paper includes programs in two different but related languages: a high level +This paper presents programs in two different but related languages: a high level language \Idris{} intended for programmers, and a low level language \TT{} to which \Idris{} is elaborated. We distinguish these languages typographically as follows: diff --git a/impl-paper/library.bib b/impl-paper/library.bib index a5e1923353..ec36e98e9c 100644 --- a/impl-paper/library.bib +++ b/impl-paper/library.bib @@ -1,297 +1,276 @@ Automatically generated by Mendeley 1.3.1 Any changes to this file will be lost if it is regenerated by Mendeley. -@inproceedings{Sculthorpe2009, -author = {Sculthorpe, Neil and Nilsson, Henrik}, -booktitle = {International Conference on Functional Programming ({ICFP} '09)}, -file = {:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf}, -title = {{Safe functional reactive programming through dependent types}}, -url = {http://dl.acm.org/citation.cfm?id=1596558}, -year = {2009} +@inproceedings{ko2011modularising, +author = {Ko, H.S. and Gibbons, J.}, +booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming}, +file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf}, +pages = {13--24}, +publisher = {ACM}, +title = {{Modularising inductive families}}, +url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921}, +year = {2011} } -@inproceedings{Augustsson1985, -address = {Berlin, Heidelberg}, -author = {Augustsson, Lennart}, -booktitle = {Functional Programming Languages and Computer Architecture}, -doi = {10.1007/3-540-15975-4}, -editor = {Jouannaud, Jean-Pierre}, -isbn = {978-3-540-15975-9}, -keywords = {Computer Science}, -pages = {368----381}, -publisher = {Springer Berlin Heidelberg}, -series = {Lecture Notes in Computer Science}, -title = {{Compiling Pattern Matching}}, -url = {http://www.springerlink.com/content/y647423656557505/}, -volume = {201}, -year = {1985} +@inproceedings{gibbons2011modularising, +author = {Gibbons, J. and Ko, H.S. and Others}, +file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf}, +title = {{Modularising inductive families}}, +url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html}, +year = {2011} } -@inproceedings{NanevskiAAMorrisett2008, -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.}, -author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C}, -booktitle = {International Conference on Functional Programming}, -doi = {10.1145/1411204.1411237}, -file = {:home/edwin/Research/Papers/Mendeley/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf}, -isbn = {9781595939197}, -issn = {15232867}, +@article{Okasaki1993, +author = {Okasaki, Chris}, +file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf}, +journal = {Journal of functional programming}, +title = {{Red-Black Trees in A Functional Setting}}, +year = {1993} +} +@misc{Brady2012b, +author = {Brooks, Fred}, +doi = {10.1093/epirev/mxr031}, +file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf}, +isbn = {9780321702081}, +issn = {1478-6729}, +pmid = {22215642}, +title = {{The Design of Design Chapter 2}} +} +@inproceedings{Brady2003, +author = {Brady, Edwin and McBride, Conor and McKinna, James}, +booktitle = {Types for Proofs and Programs}, +file = {:home/edwin/Research/Papers/Mendeley/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf}, keywords = {Dependent Types}, mendeley-tags = {Dependent Types}, -number = {9}, -pages = {229--240}, -title = {{Ynot: Dependent types for imperative programs}}, -url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b}, -volume = {43}, -year = {2008} +title = {{Inductive families need not store their indices}}, +url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf}, +year = {2003} } -@inproceedings{McBride2004b, -author = {McBride, Conor and McKinna, James}, -booktitle = {Haskell Workshop}, -file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf}, -title = {{I am not a number : I am a free variable}}, -year = {2004} +@misc{TheMendeleySupportTeam2011, +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.}, +address = {London}, +author = {{The Mendeley Support Team}}, +booktitle = {Mendeley Desktop}, +file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf}, +keywords = {Mendeley,how-to,user manual}, +pages = {1--16}, +publisher = {Mendeley Ltd.}, +title = {{Getting Started with Mendeley}}, +url = {http://www.mendeley.com}, +year = {2011} } -@article{marlow2006making, -author = {Marlow, S. and {Peyton Jones}, S.}, -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}, -journal = {Journal of Functional Programming}, -number = {4-5}, -pages = {415--449}, -publisher = {Cambridge University Press}, -title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}}, -url = {http://dl.acm.org/citation.cfm?id=1166018}, -volume = {16}, +@inproceedings{Wadler1989, +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.}, +author = {Wadler, Philip}, +booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture}, +doi = {10.1145/99370.99404}, +file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf}, +isbn = {0897913280}, +number = {June}, +pages = {347--359}, +publisher = {ACM}, +series = {FPCA '89}, +title = {{Theorems for free!}}, +url = {http://portal.acm.org/citation.cfm?id=99404}, +year = {1989} +} +@phdthesis{norell2007thesis, +author = {Norell, Ulf}, +file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf}, +keywords = {Dependent Types}, +mendeley-tags = {Dependent Types}, +publisher = {Citeseer}, +school = {Chalmers University of Technology}, +title = {{Towards a practical programming language based on dependent type theory}}, +url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf}, +year = {2007} +} +@inproceedings{l, +author = {L\"{a}mmel, R. and Jones, S.P.}, +booktitle = {ACM SIGPLAN Notices}, +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}, +number = {3}, +pages = {26--37}, +publisher = {ACM}, +title = {{Scrap your boilerplate: a practical design pattern for generic programming}}, +url = {http://dl.acm.org/citation.cfm?id=640136.604179}, +volume = {38}, +year = {2003} +} +@inproceedings{Xi1999, +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.}, +author = {Xi, Hongwei and Pfenning, Frank}, +booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99}, +doi = {10.1145/292540.292560}, +file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf}, +isbn = {1581130953}, +issn = {07439016}, +keywords = {Dependent Types}, +mendeley-tags = {Dependent Types}, +organization = {Carnegie Mellon University}, +pages = {214--227}, +publisher = {ACM Press}, +series = {POPL '99}, +title = {{Dependent types in practical programming}}, +url = {http://portal.acm.org/citation.cfm?doid=292540.292560}, +volume = {26}, +year = {1999} +} +@inproceedings{morris2006exploring, +author = {Morris, P. and Altenkirch, T. and McBride, C.}, +booktitle = {Types for Proofs and Programs}, +file = {:home/edwin/Research/Papers/Mendeley/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf}, +pages = {252--267}, +publisher = {Springer}, +title = {{Exploring the regular tree types}}, +url = {http://www.springerlink.com/index/f9p1317716614834.pdf}, year = {2006} } -@book{Choosing2012, -author = {Fowler, Martin}, +@book{Approach2012, +author = {Hunt, Andrew and Thomas, David}, booktitle = {Carcinogenesis}, doi = {10.1093/carcin/bgs054}, -file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf}, -isbn = {9780132107549}, +file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf}, +isbn = {020161622X}, issn = {1460-2180}, number = {3}, pmid = {22383472}, -title = {{Domain Specific Languages Chapter 6}}, +title = {{The Pragmatic Programmer Chapter 2}}, url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, volume = {33} } -@misc{Protocols2012a, -author = {Anderson, Ross}, +@article{Miller1992, +author = {Miller, D}, +file = {:home/edwin/Research/Papers/Mendeley/Miller/Miller - 1992 - Unification under a mixed prefix.pdf:pdf}, +journal = {Journal of symbolic computation}, +title = {{Unification under a mixed prefix}}, +url = {http://www.sciencedirect.com/science/article/pii/074771719290011R}, +year = {1992} +} +@misc{Interface2012a, +author = {Kreibich, Jay A.}, doi = {10.1093/epirev/mxr031}, -file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf}, -isbn = {9780470068526}, +file = {:home/edwin/Research/Papers/Mendeley/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf}, +isbn = {9781449394592}, issn = {1478-6729}, pmid = {22215642}, -title = {{Security Engineering Chapter 3}} -} -@inproceedings{czarnecki2004dsl, -author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.}, -booktitle = {Domain-Specific Program Generation}, -file = {:home/edwin/Research/Papers/Mendeley/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf}, -pages = {51--72}, -publisher = {Springer}, -title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}}, -url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf}, -year = {2004} +title = {{Using SQLite Chapter 7}} } -@article{Steiner1988, -author = {Steiner, JG}, -file = {:home/edwin/Research/Papers/Mendeley/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf}, -journal = {Proc. Winter USENIX Conference}, -title = {{Kerberos: An authentication service for open network systems}}, -url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf}, -year = {1988} +@inproceedings{chlipala2010ur, +author = {Chlipala, Adam}, +booktitle = {ACM SIGPLAN Notices}, +file = {:home/edwin/Research/Papers/Mendeley/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf}, +number = {6}, +pages = {122--133}, +publisher = {ACM}, +title = {{Ur: statically-typed metaprogramming with type-level record computation}}, +url = {http://dl.acm.org/citation.cfm?id=1806612}, +volume = {45}, +year = {2010} } -@book{Fowler, -author = {Fowler, Martin}, -booktitle = {Language}, -file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf}, -isbn = {9780132107549}, -title = {{Domain Specific Languages Chapter 2}} +@book{peyton1987implementation, +author = {{Peyton Jones}, S.L.}, +publisher = {Prentice-Hall, Inc.}, +title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}}, +url = {http://dl.acm.org/citation.cfm?id=1096899}, +year = {1987} } -@article{Brady2006a, -author = {Brady, E and Hammond, K}, -file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf}, -journal = {\ldots of the 5th international conference on \ldots}, -keywords = {Dependent Types}, -mendeley-tags = {Dependent Types}, -title = {{A verified staged interpreter is a verified compiler}}, -url = {http://portal.acm.org/citation.cfm?id=1173706.1173724}, -year = {2006} +@article{dybjer1994inductive, +author = {Dybjer, P.}, +journal = {Formal aspects of computing}, +number = {4}, +pages = {440--465}, +publisher = {Springer}, +title = {{Inductive families}}, +url = {http://www.springerlink.com/index/J17824H467X6J288.pdf}, +volume = {6}, +year = {1994} } -@inproceedings{oury2008power, -author = {Oury, N. and Swierstra, W.}, -booktitle = {International Conference on Functional Programming}, -file = {:home/edwin/Research/Papers/Mendeley/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf}, -keywords = {Dependent Types}, -mendeley-tags = {Dependent Types}, -number = {9}, -pages = {39--50}, +@inproceedings{lempsink2009type, +author = {Lempsink, E. and Leather, S. and L\"{o}h, A.}, +booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming}, +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}, +pages = {61--72}, publisher = {ACM}, -title = {{The power of Pi}}, -url = {http://dl.acm.org/citation.cfm?id=1411213}, -volume = {43}, -year = {2008} -} -@phdthesis{McBride1999, -author = {McBride, Conor}, -file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf}, -keywords = {Dependent Types}, -mendeley-tags = {Dependent Types}, -school = {University of Edinburgh}, -title = {{Dependently typed functional programs and their proofs}}, -url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf}, -year = {1999} -} -@article{mcbride2010ornamental, -author = {McBride, Conor}, -file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf}, -journal = {Journal of Functional Programming}, -title = {{Ornamental algebras, algebraic ornaments}}, -url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf}, -year = {2010} -} -@article{Hughes1989, -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.}, -author = {Hughes, J}, -chapter = {2}, -doi = {10.1093/comjnl/32.2.98}, -editor = {Turner, David A}, -file = {:home/edwin/Research/Papers/Mendeley/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf}, -institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden}, -isbn = {0201172364}, -issn = {00104620}, -journal = {The Computer Journal}, -number = {2}, -pages = {98--107}, -publisher = {Br Computer Soc}, -title = {{Why Functional Programming Matters}}, -url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98}, -volume = {32}, -year = {1989} -} -@article{Chapman2005epigram, -author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor}, -file = {:home/edwin/Research/Papers/Mendeley/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf}, -journal = {Trends in Functional Programming}, -publisher = {Intellect Books}, -title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}}, -url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY}, -year = {2005} -} -@article{McBride2004a, -abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.}, -author = {McBride, Conor and McKinna, James}, -doi = {10.1017/S0956796803004829}, -file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf}, -issn = {09567968}, -journal = {Journal of Functional Programming}, -keywords = {Dependent Types}, -mendeley-tags = {Dependent Types}, -number = {1}, -pages = {69--111}, -publisher = {Cambridge University Press}, -title = {{The view from the left}}, -url = {http://www.journals.cambridge.org/abstract_S0956796803004829}, -volume = {14}, -year = {2004} -} -@phdthesis{Okasaki1996, -author = {Okasaki, Chris}, -file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf}, -school = {Carnegie Mellon University}, -title = {{Purely Functional Data Structures}}, -year = {1996} -} -@misc{pollack1997believe, -author = {Pollack, R.}, -file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf}, -title = {{How to believe a machine-checked proof}}, -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}, -year = {1997} +title = {{Type-safe diff for families of datatypes}}, +url = {http://dl.acm.org/citation.cfm?id=1596624}, +year = {2009} } -@article{Abel2010, -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.}, -author = {Abel, Andreas}, -file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf}, -journal = {EPTCS}, -pages = {1--15}, -title = {{MiniAgda: Integrating Sized and Dependent Types}}, -url = {http://arxiv.org/abs/1012.4896}, -volume = {43}, -year = {2010} +@misc{The2012b, +author = {Brooks, Fred}, +doi = {10.1093/epirev/mxr031}, +file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf}, +isbn = {9780321702081}, +issn = {1478-6729}, +pmid = {22215642}, +title = {{The Design of Design Chapter 1}} } -@inproceedings{fisher2005pads, -author = {Fisher, K. and Gruber, R.}, -booktitle = {ACM SIGPLAN Notices}, -number = {6}, -pages = {295--304}, -publisher = {ACM}, -title = {{PADS: a domain-specific language for processing ad hoc data}}, -url = {http://dl.acm.org/citation.cfm?id=1065046}, -volume = {40}, -year = {2005} +@misc{The2012c, +author = {Robbins, A and Hannah, E and Lamb, L}, +doi = {10.1093/epirev/mxr031}, +file = {:home/edwin/Research/Papers/Mendeley/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf}, +isbn = {9780596529833}, +issn = {1478-6729}, +pmid = {22215642}, +title = {{Learning the vi and Vim Editors}} } -@article{mccann2000packet, -author = {McCann, P.J. and Chandra, S.}, -journal = {ACM SIGCOMM Computer Communication Review}, -number = {4}, -pages = {321--333}, -publisher = {ACM}, -title = {{Packet types: abstract specification of network protocol messages}}, -url = {http://dl.acm.org/citation.cfm?id=347563}, -volume = {30}, -year = {2000} +@book{Brady2012, +author = {Hunt, Andrew and Thomas, David}, +booktitle = {Carcinogenesis}, +doi = {10.1093/carcin/bgs054}, +file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf}, +isbn = {020161622X}, +issn = {1460-2180}, +number = {3}, +pmid = {22383472}, +title = {{The Pragmatic Programmer Chapter 5}}, +url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, +volume = {33} } -@inproceedings{Brady2003, -author = {Brady, Edwin and McBride, Conor and McKinna, James}, -booktitle = {Types for Proofs and Programs}, -file = {:home/edwin/Research/Papers/Mendeley/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf}, -keywords = {Dependent Types}, -mendeley-tags = {Dependent Types}, -title = {{Inductive families need not store their indices}}, -url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf}, -year = {2003} +@inproceedings{Pasalic2002, +author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim}, +booktitle = {International Conference on Functional Programming}, +doi = {10.1145/583852.581499}, +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}, +isbn = {1-58113-487-8}, +issn = {03621340}, +keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming}, +month = sep, +number = {9}, +pages = {218--229}, +title = {{Tagless staged interpreters for typed languages}}, +url = {http://dl.acm.org/citation.cfm?id=583852.581499}, +volume = {37}, +year = {2002} } -@misc{TheMendeleySupportTeam2011, -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.}, -address = {London}, -author = {{The Mendeley Support Team}}, -booktitle = {Mendeley Desktop}, -file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf}, -keywords = {Mendeley,how-to,user manual}, -pages = {1--16}, -publisher = {Mendeley Ltd.}, -title = {{Getting Started with Mendeley}}, -url = {http://www.mendeley.com}, -year = {2011} +@misc{Nodes2012a, +author = {Brooks, Fred}, +doi = {10.1093/epirev/mxr031}, +file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf}, +isbn = {9780321702081}, +issn = {1478-6729}, +pmid = {22215642}, +title = {{The Design of Design Chapter 3}} } -@inproceedings{Sheard2005, -address = {New York, New York, USA}, -author = {Sheard, Tim}, -booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05}, -doi = {10.1145/1088348.1088356}, -file = {:home/edwin/Research/Papers/Mendeley/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf}, -isbn = {159593071X}, -keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic}, -month = sep, -pages = {74--85}, -publisher = {ACM Press}, -title = {{Putting curry-howard to work}}, -url = {http://dl.acm.org/citation.cfm?id=1088348.1088356}, -year = {2005} +@article{Haskell2012a, +author = {Biancuzzi, F and Warden, S}, +doi = {10.1093/epirev/mxr031}, +file = {:home/edwin/Research/Papers/Mendeley/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf}, +isbn = {9780596801670}, +issn = {1478-6729}, +pmid = {22215642}, +title = {{Masterminds of Programming Chapter 8}} } -@article{Jones2003, -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.}, -author = {Jones, Simon Peyton}, -editor = {Jones, Simon Peyton}, -isbn = {0521826144}, -journal = {Language}, -number = {1}, -publisher = {Cambridge University Press}, -title = {{Haskell 98 Language and Libraries The Revised Report}}, -url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144}, -volume = {13}, -year = {2003} +@book{An2012, +author = {Fowler, Martin}, +booktitle = {Carcinogenesis}, +doi = {10.1093/carcin/bgs054}, +file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf}, +isbn = {9780132107549}, +issn = {1460-2180}, +number = {3}, +pmid = {22383472}, +title = {{Domain Specific Languages Chapter 1}}, +url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, +volume = {33} } @article{McBride2005, author = {McBride, Conor}, @@ -308,18 +287,6 @@ @article{McBride2005 volume = {3622}, year = {2005} } -@inproceedings{chlipala2010ur, -author = {Chlipala, Adam}, -booktitle = {ACM SIGPLAN Notices}, -file = {:home/edwin/Research/Papers/Mendeley/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf}, -number = {6}, -pages = {122--133}, -publisher = {ACM}, -title = {{Ur: statically-typed metaprogramming with type-level record computation}}, -url = {http://dl.acm.org/citation.cfm?id=1806612}, -volume = {45}, -year = {2010} -} @misc{Resolution2012a, author = {Fall, Kevin R and Stevens, W. Richard}, doi = {10.1093/epirev/mxr031}, @@ -328,225 +295,31 @@ @misc{Resolution2012a pmid = {22215642}, title = {{TCP/IP Illustrated Volume 1 Chapter 11}} } -@inproceedings{gibbons2011modularising, -author = {Gibbons, J. and Ko, H.S. and Others}, -file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf}, -title = {{Modularising inductive families}}, -url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html}, -year = {2011} -} -@article{burrows1990, -author = {Burrows, Michael and Abadi, Martin and Needham, Roger}, -file = {:home/edwin/Research/Papers/Mendeley/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf}, -journal = {ACM Transactions on Computer Systems}, -pages = {18----36}, -title = {{A logic of authentication}}, -url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569}, -volume = {8}, -year = {1990} -} -@misc{Brady2012b, -author = {Brooks, Fred}, -doi = {10.1093/epirev/mxr031}, -file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf}, -isbn = {9780321702081}, -issn = {1478-6729}, -pmid = {22215642}, -title = {{The Design of Design Chapter 2}} -} -@inproceedings{Levitation2010, -author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter}, -booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}, -doi = {10.1145/1932681.1863547}, -file = {:home/edwin/Research/Papers/Mendeley/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf}, -isbn = {978-1-60558-794-3}, -issn = {03621340}, -keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems}, -mendeley-tags = {Dependent Types}, -month = sep, -number = {9}, -pages = {3}, -title = {{The gentle art of levitation}}, -url = {http://dl.acm.org/citation.cfm?id=1932681.1863547}, -volume = {45}, -year = {2010} -} -@inproceedings{Wadler1989, -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.}, -author = {Wadler, Philip}, -booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture}, -doi = {10.1145/99370.99404}, -file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf}, -isbn = {0897913280}, -number = {June}, -pages = {347--359}, -publisher = {ACM}, -series = {FPCA '89}, -title = {{Theorems for free!}}, -url = {http://portal.acm.org/citation.cfm?id=99404}, -year = {1989} -} -@article{Altenkirch2010a, -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.}, -author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter}, -file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf}, -journal = {Citeseer}, -publisher = {Citeseer}, -title = {{Generic Programming with Dependent Types}}, -url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf}, -year = {2010} -} -@inproceedings{l, -author = {L\"{a}mmel, R. and Jones, S.P.}, -booktitle = {ACM SIGPLAN Notices}, -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}, -number = {3}, -pages = {26--37}, -publisher = {ACM}, -title = {{Scrap your boilerplate: a practical design pattern for generic programming}}, -url = {http://dl.acm.org/citation.cfm?id=640136.604179}, -volume = {38}, -year = {2003} -} -@inproceedings{Xi1999, -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.}, -author = {Xi, Hongwei and Pfenning, Frank}, -booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99}, -doi = {10.1145/292540.292560}, -file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf}, -isbn = {1581130953}, -issn = {07439016}, +@phdthesis{Brady2005, +author = {Brady, Edwin}, +file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf}, keywords = {Dependent Types}, mendeley-tags = {Dependent Types}, -organization = {Carnegie Mellon University}, -pages = {214--227}, -publisher = {ACM Press}, -series = {POPL '99}, -title = {{Dependent types in practical programming}}, -url = {http://portal.acm.org/citation.cfm?doid=292540.292560}, -volume = {26}, -year = {1999} -} -@book{Approach2012, -author = {Hunt, Andrew and Thomas, David}, -booktitle = {Carcinogenesis}, -doi = {10.1093/carcin/bgs054}, -file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf}, -isbn = {020161622X}, -issn = {1460-2180}, -number = {3}, -pmid = {22383472}, -title = {{The Pragmatic Programmer Chapter 2}}, -url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, -volume = {33} -} -@article{Miller1992, -author = {Miller, D}, -file = {:home/edwin/Research/Papers/Mendeley/Miller/Miller - 1992 - Unification under a mixed prefix.pdf:pdf}, -journal = {Journal of symbolic computation}, -title = {{Unification under a mixed prefix}}, -url = {http://www.sciencedirect.com/science/article/pii/074771719290011R}, -year = {1992} -} -@misc{Interface2012a, -author = {Kreibich, Jay A.}, -doi = {10.1093/epirev/mxr031}, -file = {:home/edwin/Research/Papers/Mendeley/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf}, -isbn = {9781449394592}, -issn = {1478-6729}, -pmid = {22215642}, -title = {{Using SQLite Chapter 7}} +school = {University of Durham}, +title = {{Practical Implementation of a Dependently Typed Functional Programming Language}}, +url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf}, +year = {2005} } -@inproceedings{Brady2006b, +@inproceedings{Brady2011a, +address = {New York, New York, USA}, author = {Brady, Edwin}, -booktitle = {Implementation and Application of Functional Languages ({IFL}'06)}, -file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf}, -isbn = {978-3-540-74129-9}, -month = sep, -pages = {145----162}, -title = {{Ivor, a proof engine}}, -url = {http://dl.acm.org/citation.cfm?id=1757028.1757037}, -year = {2006} -} -@misc{TheMendeleySupportTeam2011a, -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.}, -address = {London}, -author = {{The Mendeley Support Team}}, -booktitle = {Mendeley Desktop}, -file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf}, -keywords = {Mendeley,how-to,user manual}, -pages = {1--16}, -publisher = {Mendeley Ltd.}, -title = {{Getting Started with Mendeley}}, -url = {http://www.mendeley.com}, +booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11}, +doi = {10.1145/1929529.1929536}, +file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf}, +isbn = {9781450304870}, +keywords = {Dependent Types,data description,dependent types}, +mendeley-tags = {Dependent Types}, +month = jan, +publisher = {ACM Press}, +title = {{Idris --- Systems Programming Meets Full Dependent Types}}, +url = {http://dl.acm.org/citation.cfm?id=1929529.1929536}, year = {2011} } -@book{peyton1987implementation, -author = {{Peyton Jones}, S.L.}, -publisher = {Prentice-Hall, Inc.}, -title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}}, -url = {http://dl.acm.org/citation.cfm?id=1096899}, -year = {1987} -} -@article{dybjer1994inductive, -author = {Dybjer, P.}, -journal = {Formal aspects of computing}, -number = {4}, -pages = {440--465}, -publisher = {Springer}, -title = {{Inductive families}}, -url = {http://www.springerlink.com/index/J17824H467X6J288.pdf}, -volume = {6}, -year = {1994} -} -@inproceedings{lempsink2009type, -author = {Lempsink, E. and Leather, S. and L\"{o}h, A.}, -booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming}, -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}, -pages = {61--72}, -publisher = {ACM}, -title = {{Type-safe diff for families of datatypes}}, -url = {http://dl.acm.org/citation.cfm?id=1596624}, -year = {2009} -} -@misc{The2012b, -author = {Brooks, Fred}, -doi = {10.1093/epirev/mxr031}, -file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf}, -isbn = {9780321702081}, -issn = {1478-6729}, -pmid = {22215642}, -title = {{The Design of Design Chapter 1}} -} -@book{Brady2012, -author = {Hunt, Andrew and Thomas, David}, -booktitle = {Carcinogenesis}, -doi = {10.1093/carcin/bgs054}, -file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf}, -isbn = {020161622X}, -issn = {1460-2180}, -number = {3}, -pmid = {22383472}, -title = {{The Pragmatic Programmer Chapter 5}}, -url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, -volume = {33} -} -@inproceedings{Pasalic2002, -author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim}, -booktitle = {International Conference on Functional Programming}, -doi = {10.1145/583852.581499}, -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}, -isbn = {1-58113-487-8}, -issn = {03621340}, -keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming}, -month = sep, -number = {9}, -pages = {218--229}, -title = {{Tagless staged interpreters for typed languages}}, -url = {http://dl.acm.org/citation.cfm?id=583852.581499}, -volume = {37}, -year = {2002} -} @misc{dagand2011transporting, author = {Dagand, Pierre-Evariste and McBride, Conor}, file = {:home/edwin/Research/Papers/Mendeley/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf}, @@ -554,13 +327,6 @@ @misc{dagand2011transporting url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf}, year = {2011} } -@article{Okasaki1993, -author = {Okasaki, Chris}, -file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf}, -journal = {Journal of functional programming}, -title = {{Red-Black Trees in A Functional Setting}}, -year = {1993} -} @inproceedings{taha2004gentle, author = {Taha, W.}, booktitle = {Domain-Specific Program Generation}, @@ -570,42 +336,25 @@ @inproceedings{taha2004gentle url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf}, year = {2004} } -@inproceedings{pj2006gadts, -author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.}, -booktitle = {{International Conference on Functional Programming} ({ICFP} '06)}, -file = {:home/edwin/Research/Papers/Mendeley/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf}, +@inproceedings{augustsson2008paradise, +author = {Augustsson, L. and Mansell, H. and Sittampalam, G.}, +booktitle = {International Conference on Functional Programming}, +file = {:home/edwin/Research/Papers/Mendeley/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf}, number = {9}, -pages = {50--61}, +pages = {225--228}, publisher = {ACM}, -title = {{Simple unification-based type inference for GADTs}}, -url = {http://dl.acm.org/citation.cfm?id=1159811}, -volume = {41}, -year = {2006} +title = {{Paradise: a two-stage DSL embedded in Haskell}}, +url = {http://dl.acm.org/citation.cfm?id=1411203.1411236}, +volume = {43}, +year = {2008} } -@misc{altenkirch2008nσ, -author = {Altenkirch, T. and Oury, N.}, -file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf}, -title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}}, -url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf}, -year = {2008} -} -@misc{Nodes2012a, -author = {Brooks, Fred}, -doi = {10.1093/epirev/mxr031}, -file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf}, -isbn = {9780321702081}, -issn = {1478-6729}, -pmid = {22215642}, -title = {{The Design of Design Chapter 3}} -} -@article{Haskell2012a, -author = {Biancuzzi, F and Warden, S}, -doi = {10.1093/epirev/mxr031}, -file = {:home/edwin/Research/Papers/Mendeley/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf}, -isbn = {9780596801670}, -issn = {1478-6729}, -pmid = {22215642}, -title = {{Masterminds of Programming Chapter 8}} +@misc{altenkirch2005dependent, +author = {Altenkirch, T. and McBride, C. and McKinna, J.}, +booktitle = {Manuscript, available online}, +file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf}, +title = {{Why dependent types matter}}, +url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf}, +year = {2005} } @article{Xi1998, 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.}, @@ -626,82 +375,6 @@ @article{Xi1998 volume = {33}, year = {1998} } -@inproceedings{morris2006exploring, -author = {Morris, P. and Altenkirch, T. and McBride, C.}, -booktitle = {Types for Proofs and Programs}, -file = {:home/edwin/Research/Papers/Mendeley/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf}, -pages = {252--267}, -publisher = {Springer}, -title = {{Exploring the regular tree types}}, -url = {http://www.springerlink.com/index/f9p1317716614834.pdf}, -year = {2006} -} -@article{landin1966next, -author = {Landin, P.J.}, -file = {:home/edwin/Research/Papers/Mendeley/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf}, -journal = {Communications of the ACM}, -number = {3}, -pages = {157--166}, -publisher = {ACM}, -title = {{The next 700 programming languages}}, -url = {http://dl.acm.org/citation.cfm?id=365257 )}, -volume = {9}, -year = {1966} -} -@phdthesis{Brady2005, -author = {Brady, Edwin}, -file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf}, -keywords = {Dependent Types}, -mendeley-tags = {Dependent Types}, -school = {University of Durham}, -title = {{Practical Implementation of a Dependently Typed Functional Programming Language}}, -url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf}, -year = {2005} -} -@inproceedings{Brady2011a, -address = {New York, New York, USA}, -author = {Brady, Edwin}, -booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11}, -doi = {10.1145/1929529.1929536}, -file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf}, -isbn = {9781450304870}, -keywords = {Dependent Types,data description,dependent types}, -mendeley-tags = {Dependent Types}, -month = jan, -publisher = {ACM Press}, -title = {{Idris --- Systems Programming Meets Full Dependent Types}}, -url = {http://dl.acm.org/citation.cfm?id=1929529.1929536}, -year = {2011} -} -@article{Altenkirch2010, -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.}, -author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas}, -doi = {10.1007/978-3-642-12251-4_5}, -editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n}, -file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf}, -isbn = {9783642122507}, -journal = {Computing}, -number = {Sheard 2005}, -pages = {40--55}, -publisher = {Springer Berlin Heidelberg}, -series = {Lecture Notes in Computer Science}, -title = {{Dependent Types without the Sugar}}, -url = {http://www.springerlink.com/index/91W712G2806R575H.pdf}, -volume = {6009}, -year = {2010} -} -@inproceedings{augustsson2008paradise, -author = {Augustsson, L. and Mansell, H. and Sittampalam, G.}, -booktitle = {International Conference on Functional Programming}, -file = {:home/edwin/Research/Papers/Mendeley/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf}, -number = {9}, -pages = {225--228}, -publisher = {ACM}, -title = {{Paradise: a two-stage DSL embedded in Haskell}}, -url = {http://dl.acm.org/citation.cfm?id=1411203.1411236}, -volume = {43}, -year = {2008} -} @inproceedings{augustsson1999exercise, author = {Augustsson, L. and Carlsson, M.}, booktitle = {In Workshop on Dependent Types in Programming, Gothenburg}, @@ -723,18 +396,6 @@ @article{Swierstra2011 volume = {21}, year = {2011} } -@article{fisher2006next, -author = {Fisher, K. and Mandelbaum, Y. and Walker, D.}, -file = {:home/edwin/Research/Papers/Mendeley/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf}, -journal = {Journal of the ACM}, -number = {2}, -pages = {1--51}, -publisher = {ACM}, -title = {{The next 700 data description languages}}, -url = {http://dl.acm.org/citation.cfm?id=1111039}, -volume = {15}, -year = {2010} -} @inproceedings{norell2009dependently, author = {Norell, Ulf}, booktitle = {Advanced Functional Programming}, @@ -781,14 +442,50 @@ @article{Jones1999 url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf}, year = {1999} } -@article{Epstein2011, -author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon}, -institution = {Microsoft Research}, -journal = {researchmicrosoftcom}, -number = {Section 8}, -pages = {1--12}, -title = {{Haskell for the cloud}}, -url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf}, +@article{Altenkirch2010, +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.}, +author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas}, +doi = {10.1007/978-3-642-12251-4_5}, +editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n}, +file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf}, +isbn = {9783642122507}, +journal = {Computing}, +number = {Sheard 2005}, +pages = {40--55}, +publisher = {Springer Berlin Heidelberg}, +series = {Lecture Notes in Computer Science}, +title = {{Dependent Types without the Sugar}}, +url = {http://www.springerlink.com/index/91W712G2806R575H.pdf}, +volume = {6009}, +year = {2010} +} +@book{Bertot2004, +author = {Bertot, Yves and Cast\'{e}ran, Pierre}, +publisher = {Springer}, +title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}}, +url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4}, +year = {2004} +} +@book{The2012, +author = {Hunt, Andrew and Thomas, David}, +booktitle = {Carcinogenesis}, +doi = {10.1093/carcin/bgs054}, +file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf}, +isbn = {020161622X}, +issn = {1460-2180}, +number = {3}, +pmid = {22383472}, +title = {{The Pragmatic Programmer Chapter 3}}, +url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, +volume = {33} +} +@inproceedings{ko2011modularising, +author = {Ko, H.S. and Gibbons, J.}, +booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming}, +pages = {13--24}, +publisher = {ACM}, +title = {{Modularising inductive families}}, +url = {http://dl.acm.org/citation.cfm?id=2036921}, year = {2011} } @article{danielsson2011parsing, @@ -828,28 +525,17 @@ @misc{idristutorial url = {http://idris-lang.org/tutorial}, year = {2012} } -@book{An2012, -author = {Fowler, Martin}, -booktitle = {Carcinogenesis}, -doi = {10.1093/carcin/bgs054}, -file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf}, -isbn = {9780132107549}, -issn = {1460-2180}, +@inproceedings{madhavapeddy2007melange, +author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.}, +booktitle = {ACM SIGOPS Operating Systems Review}, +file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf}, number = {3}, -pmid = {22383472}, -title = {{Domain Specific Languages Chapter 1}}, -url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, -volume = {33} -} -@inproceedings{ko2011modularising, -author = {Ko, H.S. and Gibbons, J.}, -booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming}, -file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf}, -pages = {13--24}, +pages = {101--114}, publisher = {ACM}, -title = {{Modularising inductive families}}, -url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921}, -year = {2011} +title = {{Melange: creating a functional internet}}, +url = {http://dl.acm.org/citation.cfm?id=1273009}, +volume = {41}, +year = {2007} } @inproceedings{Augustsson1998, 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.}, @@ -877,6 +563,23 @@ @inproceedings{brady2011epic url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1}, year = {2011} } +@article{Epstein2011, +author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon}, +institution = {Microsoft Research}, +journal = {researchmicrosoftcom}, +number = {Section 8}, +pages = {1--12}, +title = {{Haskell for the cloud}}, +url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf}, +year = {2011} +} +@book{Hunt, +author = {Hunt, Andrew and Thomas, David}, +booktitle = {Design}, +file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf}, +isbn = {020161622X}, +title = {{The Pragmatic Programmer Chapter 4}} +} @inproceedings{swierstra2007beauty, author = {Swierstra, W. and Altenkirch, T.}, booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop}, @@ -887,42 +590,43 @@ @inproceedings{swierstra2007beauty url = {http://dl.acm.org/citation.cfm?id=1291206}, year = {2007} } -@inproceedings{Brady2010, +@inproceedings{bradyresource, author = {Brady, Edwin and Hammond, Kevin}, -booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming}, -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}, -isbn = {9781605587943}, -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}, -mendeley-tags = {Dependent Types}, -pages = {297--308}, +booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)}, +file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf}, +pages = {242----257}, +title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}}, +url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf}, +year = {2012} +} +@article{fisher2006next, +author = {Fisher, K. and Mandelbaum, Y. and Walker, D.}, +file = {:home/edwin/Research/Papers/Mendeley/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf}, +journal = {Journal of the ACM}, +number = {2}, +pages = {1--51}, publisher = {ACM}, -title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}}, -url = {http://portal.acm.org/citation.cfm?id=1863587}, +title = {{The next 700 data description languages}}, +url = {http://dl.acm.org/citation.cfm?id=1111039}, +volume = {15}, year = {2010} } -@misc{The2012c, -author = {Robbins, A and Hannah, E and Lamb, L}, -doi = {10.1093/epirev/mxr031}, -file = {:home/edwin/Research/Papers/Mendeley/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf}, -isbn = {9780596529833}, -issn = {1478-6729}, -pmid = {22215642}, -title = {{Learning the vi and Vim Editors}} +@book{Bird2010, +author = {Bird, Richard}, +file = {:home/edwin/Research/Papers/Mendeley/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf}, +isbn = {9780521513388}, +title = {{Pearls of Functional Algorithm Design}}, +year = {2010} } -@misc{altenkirch2005dependent, -author = {Altenkirch, T. and McBride, C. and McKinna, J.}, -booktitle = {Manuscript, available online}, -file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf}, -title = {{Why dependent types matter}}, -url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf}, -year = {2005} -} -@book{Hunt, -author = {Hunt, Andrew and Thomas, David}, -booktitle = {Design}, -file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf}, -isbn = {020161622X}, -title = {{The Pragmatic Programmer Chapter 4}} +@inproceedings{stump2010resource, +author = {Stump, A. and Austin, E.}, +booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification}, +file = {:home/edwin/Research/Papers/Mendeley/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf}, +pages = {27--38}, +publisher = {ACM}, +title = {{Resource typing in Guru}}, +url = {http://dl.acm.org/citation.cfm?id=1707796}, +year = {2010} } @inproceedings{taha1997multi, author = {Taha, W. and Sheard, T.}, @@ -935,66 +639,6 @@ @inproceedings{taha1997multi volume = {32}, year = {1997} } -@book{Philosophy2012, -author = {Hunt, Andrew and Thomas, David}, -booktitle = {Carcinogenesis}, -doi = {10.1093/carcin/bgs054}, -file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf}, -isbn = {020161622X}, -issn = {1460-2180}, -number = {3}, -pmid = {22383472}, -title = {{The Pragmatic Programmer Chapter 1}}, -url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, -volume = {33} -} -@inproceedings{bradyresource, -author = {Brady, Edwin and Hammond, Kevin}, -booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)}, -file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf}, -pages = {242----257}, -title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}}, -url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf}, -year = {2012} -} -@book{The2012, -author = {Hunt, Andrew and Thomas, David}, -booktitle = {Carcinogenesis}, -doi = {10.1093/carcin/bgs054}, -file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf}, -isbn = {020161622X}, -issn = {1460-2180}, -number = {3}, -pmid = {22383472}, -title = {{The Pragmatic Programmer Chapter 3}}, -url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, -volume = {33} -} -@book{Bird2010, -author = {Bird, Richard}, -file = {:home/edwin/Research/Papers/Mendeley/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf}, -isbn = {9780521513388}, -title = {{Pearls of Functional Algorithm Design}}, -year = {2010} -} -@inproceedings{stump2010resource, -author = {Stump, A. and Austin, E.}, -booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification}, -file = {:home/edwin/Research/Papers/Mendeley/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf}, -pages = {27--38}, -publisher = {ACM}, -title = {{Resource typing in Guru}}, -url = {http://dl.acm.org/citation.cfm?id=1707796}, -year = {2010} -} -@article{McBride2007, -author = {McBride, Conor and Paterson, Ross}, -file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf}, -journal = {Journal of functional programming}, -title = {{Applicative programming with effects}}, -url = {http://journals.cambridge.org/abstract_S0956796807006326}, -year = {2007} -} @article{Wadler2001, abstract = {The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.}, author = {Wadler, Philip}, @@ -1013,18 +657,6 @@ @article{Wadler2001 volume = {925}, year = {2001} } -@inproceedings{madhavapeddy2007melange, -author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.}, -booktitle = {ACM SIGOPS Operating Systems Review}, -file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf}, -number = {3}, -pages = {101--114}, -publisher = {ACM}, -title = {{Melange: creating a functional internet}}, -url = {http://dl.acm.org/citation.cfm?id=1273009}, -volume = {41}, -year = {2007} -} @article{Hoare1978, 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.}, author = {Hoare, C A R}, @@ -1044,16 +676,44 @@ @article{Hoare1978 volume = {21}, year = {1978} } -@phdthesis{norell2007thesis, -author = {Norell, Ulf}, -file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf}, -keywords = {Dependent Types}, +@book{Philosophy2012, +author = {Hunt, Andrew and Thomas, David}, +booktitle = {Carcinogenesis}, +doi = {10.1093/carcin/bgs054}, +file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf}, +isbn = {020161622X}, +issn = {1460-2180}, +number = {3}, +pmid = {22383472}, +title = {{The Pragmatic Programmer Chapter 1}}, +url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, +volume = {33} +} +@book{While2012, +author = {Hunt, Andrew and Thomas, David}, +booktitle = {Carcinogenesis}, +doi = {10.1093/carcin/bgs054}, +file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf}, +isbn = {020161622X}, +issn = {1460-2180}, +number = {3}, +pmid = {22383472}, +title = {{The Pragmatic Programmer Chapter 6}}, +url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, +volume = {33} +} +@inproceedings{Brady2010, +author = {Brady, Edwin and Hammond, Kevin}, +booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming}, +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}, +isbn = {9781605587943}, +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}, mendeley-tags = {Dependent Types}, -publisher = {Citeseer}, -school = {Chalmers University of Technology}, -title = {{Towards a practical programming language based on dependent type theory}}, -url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf}, -year = {2007} +pages = {297--308}, +publisher = {ACM}, +title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}}, +url = {http://portal.acm.org/citation.cfm?id=1863587}, +year = {2010} } @inproceedings{Visser2008, author = {Visser, E}, @@ -1062,6 +722,19 @@ @inproceedings{Visser2008 url = {http://www.springerlink.com/index/A3213003X6268032.pdf}, year = {2008} } +@misc{TheMendeleySupportTeam2011a, +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.}, +address = {London}, +author = {{The Mendeley Support Team}}, +booktitle = {Mendeley Desktop}, +file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf}, +keywords = {Mendeley,how-to,user manual}, +pages = {1--16}, +publisher = {Mendeley Ltd.}, +title = {{Getting Started with Mendeley}}, +url = {http://www.mendeley.com}, +year = {2011} +} @inproceedings{Brady2005a, author = {Brady, E and Hammond, K}, booktitle = {Implementation and Application of Functional \ldots}, @@ -1072,40 +745,6 @@ @inproceedings{Brady2005a url = {http://www.springerlink.com/index/P446P2HH70107759.pdf}, year = {2005} } -@book{Bertot2004, -author = {Bertot, Yves and Cast\'{e}ran, Pierre}, -publisher = {Springer}, -title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}}, -url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4}, -year = {2004} -} -@inproceedings{ko2011modularising, -author = {Ko, H.S. and Gibbons, J.}, -booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming}, -pages = {13--24}, -publisher = {ACM}, -title = {{Modularising inductive families}}, -url = {http://dl.acm.org/citation.cfm?id=2036921}, -year = {2011} -} -@inproceedings{barras2008implicit, -author = {Barras, B. and Bernardo, B.}, -booktitle = {Foundations of Software Science and Computational Structures}, -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}, -pages = {365--379}, -publisher = {Springer}, -title = {{The implicit calculus of constructions as a programming language with dependent types}}, -url = {http://www.springerlink.com/index/m84h82904546l265.pdf}, -year = {2008} -} -@inproceedings{Fournet2011, -author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D}, -booktitle = {Foundations of security analysis and design {VI}}, -file = {:home/edwin/Research/Papers/Mendeley/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf}, -title = {{Cryptographic verification by typing for a sample protocol implementation}}, -url = {http://www.springerlink.com/index/V168041M46658R73.pdf}, -year = {2010} -} @inproceedings{madhavapeddy2010turning, author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.}, booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing}, @@ -1115,6 +754,14 @@ @inproceedings{madhavapeddy2010turning url = {http://dl.acm.org/citation.cfm?id=1863114}, year = {2010} } +@article{McBride2007, +author = {McBride, Conor and Paterson, Ross}, +file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf}, +journal = {Journal of functional programming}, +title = {{Applicative programming with effects}}, +url = {http://journals.cambridge.org/abstract_S0956796807006326}, +year = {2007} +} @inproceedings{bhargavan2010modular, author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.}, booktitle = {ACM Sigplan Notices}, @@ -1135,12 +782,21 @@ @inproceedings{coquand1986analysis url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf}, year = {1986} } -@misc{Abel1998, -author = {Abel, Andreas}, -booktitle = {Language}, -file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf}, -title = {{foetus - Termination Checker for Simple Functional Programs}}, -year = {1998} +@inproceedings{Augustsson1985, +address = {Berlin, Heidelberg}, +author = {Augustsson, Lennart}, +booktitle = {Functional Programming Languages and Computer Architecture}, +doi = {10.1007/3-540-15975-4}, +editor = {Jouannaud, Jean-Pierre}, +isbn = {978-3-540-15975-9}, +keywords = {Computer Science}, +pages = {368----381}, +publisher = {Springer Berlin Heidelberg}, +series = {Lecture Notes in Computer Science}, +title = {{Compiling Pattern Matching}}, +url = {http://www.springerlink.com/content/y647423656557505/}, +volume = {201}, +year = {1985} } @misc{Bloat, author = {Brooks, Fred}, @@ -1148,6 +804,16 @@ @misc{Bloat isbn = {9780321702081}, title = {{The Design of Design Chapter 4}} } +@inproceedings{barras2008implicit, +author = {Barras, B. and Bernardo, B.}, +booktitle = {Foundations of Software Science and Computational Structures}, +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}, +pages = {365--379}, +publisher = {Springer}, +title = {{The implicit calculus of constructions as a programming language with dependent types}}, +url = {http://www.springerlink.com/index/m84h82904546l265.pdf}, +year = {2008} +} @misc{Brady2012c, author = {Brooks, Fred}, doi = {10.1093/epirev/mxr031}, @@ -1160,31 +826,31 @@ @misc{Brady2012c title = {{The Design of Design Chapter 5}}, volume = {34} } -@inproceedings{atkey2009unembedding, -author = {Atkey, R. and Lindley, S. and Yallop, J.}, -booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell}, -pages = {37--48}, -publisher = {ACM}, -title = {{Unembedding domain-specific languages}}, -url = {http://dl.acm.org/citation.cfm?id=1596644}, -year = {2009} -} -@article{loh2010tutorial, -author = {L\"{o}h, A. and McBride, C. and Swierstra, W.}, -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}, -journal = {Fundamenta Informaticae}, -number = {2}, -pages = {177--207}, -publisher = {IOS Press}, -title = {{A tutorial implementation of a dependently typed lambda calculus}}, -url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf}, -volume = {102}, +@inproceedings{Fournet2011, +author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D}, +booktitle = {Foundations of security analysis and design {VI}}, +file = {:home/edwin/Research/Papers/Mendeley/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf}, +title = {{Cryptographic verification by typing for a sample protocol implementation}}, +url = {http://www.springerlink.com/index/V168041M46658R73.pdf}, year = {2010} } -@article{mcbride2008functional, -author = {McBride, C. and Paterson, R.}, -file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf}, -journal = {Journal of functional programming}, +@book{Choosing2012, +author = {Fowler, Martin}, +booktitle = {Carcinogenesis}, +doi = {10.1093/carcin/bgs054}, +file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf}, +isbn = {9780132107549}, +issn = {1460-2180}, +number = {3}, +pmid = {22383472}, +title = {{Domain Specific Languages Chapter 6}}, +url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, +volume = {33} +} +@article{mcbride2008functional, +author = {McBride, C. and Paterson, R.}, +file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf}, +journal = {Journal of functional programming}, number = {1}, pages = {1--13}, publisher = {Cambridge Univ Press}, @@ -1202,18 +868,61 @@ @inproceedings{pollack1990implicit url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf}, year = {1990} } -@book{While2012, -author = {Hunt, Andrew and Thomas, David}, -booktitle = {Carcinogenesis}, -doi = {10.1093/carcin/bgs054}, -file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf}, -isbn = {020161622X}, -issn = {1460-2180}, -number = {3}, -pmid = {22383472}, -title = {{The Pragmatic Programmer Chapter 6}}, -url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472}, -volume = {33} +@misc{altenkirch2008nσ, +author = {Altenkirch, T. and Oury, N.}, +file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf}, +title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}}, +url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf}, +year = {2008} +} +@misc{Abel1998, +author = {Abel, Andreas}, +booktitle = {Language}, +file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf}, +title = {{foetus - Termination Checker for Simple Functional Programs}}, +year = {1998} +} +@misc{pollack1997believe, +author = {Pollack, R.}, +file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf}, +title = {{How to believe a machine-checked proof}}, +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}, +year = {1997} +} +@inproceedings{atkey2009unembedding, +author = {Atkey, R. and Lindley, S. and Yallop, J.}, +booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell}, +pages = {37--48}, +publisher = {ACM}, +title = {{Unembedding domain-specific languages}}, +url = {http://dl.acm.org/citation.cfm?id=1596644}, +year = {2009} +} +@inproceedings{oury2008power, +author = {Oury, N. and Swierstra, W.}, +booktitle = {International Conference on Functional Programming}, +file = {:home/edwin/Research/Papers/Mendeley/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf}, +keywords = {Dependent Types}, +mendeley-tags = {Dependent Types}, +number = {9}, +pages = {39--50}, +publisher = {ACM}, +title = {{The power of Pi}}, +url = {http://dl.acm.org/citation.cfm?id=1411213}, +volume = {43}, +year = {2008} +} +@article{loh2010tutorial, +author = {L\"{o}h, A. and McBride, C. and Swierstra, W.}, +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}, +journal = {Fundamenta Informaticae}, +number = {2}, +pages = {177--207}, +publisher = {IOS Press}, +title = {{A tutorial implementation of a dependently typed lambda calculus}}, +url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf}, +volume = {102}, +year = {2010} } @article{gordon2003authenticity, author = {Gordon, A.D. and Jeffrey, A.}, @@ -1239,3 +948,294 @@ @misc{Attacks2012a title = {{Security Engineering Chapter 18}}, volume = {34} } +@inproceedings{Sheard2005, +address = {New York, New York, USA}, +author = {Sheard, Tim}, +booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05}, +doi = {10.1145/1088348.1088356}, +file = {:home/edwin/Research/Papers/Mendeley/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf}, +isbn = {159593071X}, +keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic}, +month = sep, +pages = {74--85}, +publisher = {ACM Press}, +title = {{Putting curry-howard to work}}, +url = {http://dl.acm.org/citation.cfm?id=1088348.1088356}, +year = {2005} +} +@inproceedings{NanevskiAAMorrisett2008, +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.}, +author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C}, +booktitle = {International Conference on Functional Programming}, +doi = {10.1145/1411204.1411237}, +file = {:home/edwin/Research/Papers/Mendeley/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf}, +isbn = {9781595939197}, +issn = {15232867}, +keywords = {Dependent Types}, +mendeley-tags = {Dependent Types}, +number = {9}, +pages = {229--240}, +title = {{Ynot: Dependent types for imperative programs}}, +url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b}, +volume = {43}, +year = {2008} +} +@inproceedings{fisher2005pads, +author = {Fisher, K. and Gruber, R.}, +booktitle = {ACM SIGPLAN Notices}, +number = {6}, +pages = {295--304}, +publisher = {ACM}, +title = {{PADS: a domain-specific language for processing ad hoc data}}, +url = {http://dl.acm.org/citation.cfm?id=1065046}, +volume = {40}, +year = {2005} +} +@inproceedings{McBride2004b, +author = {McBride, Conor and McKinna, James}, +booktitle = {Haskell Workshop}, +file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf}, +title = {{I am not a number : I am a free variable}}, +year = {2004} +} +@article{marlow2006making, +author = {Marlow, S. and {Peyton Jones}, S.}, +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}, +journal = {Journal of Functional Programming}, +number = {4-5}, +pages = {415--449}, +publisher = {Cambridge University Press}, +title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}}, +url = {http://dl.acm.org/citation.cfm?id=1166018}, +volume = {16}, +year = {2006} +} +@article{landin1966next, +author = {Landin, P.J.}, +file = {:home/edwin/Research/Papers/Mendeley/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf}, +journal = {Communications of the ACM}, +number = {3}, +pages = {157--166}, +publisher = {ACM}, +title = {{The next 700 programming languages}}, +url = {http://dl.acm.org/citation.cfm?id=365257 )}, +volume = {9}, +year = {1966} +} +@misc{Protocols2012a, +author = {Anderson, Ross}, +doi = {10.1093/epirev/mxr031}, +file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf}, +isbn = {9780470068526}, +issn = {1478-6729}, +pmid = {22215642}, +title = {{Security Engineering Chapter 3}} +} +@inproceedings{Sculthorpe2009, +author = {Sculthorpe, Neil and Nilsson, Henrik}, +booktitle = {International Conference on Functional Programming ({ICFP} '09)}, +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}, +title = {{Safe functional reactive programming through dependent types}}, +url = {http://dl.acm.org/citation.cfm?id=1596558}, +year = {2009} +} +@book{Fowler, +author = {Fowler, Martin}, +booktitle = {Language}, +file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf}, +isbn = {9780132107549}, +title = {{Domain Specific Languages Chapter 2}} +} +@article{Jones2003, +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.}, +author = {Jones, Simon Peyton}, +editor = {Jones, Simon Peyton}, +isbn = {0521826144}, +journal = {Language}, +number = {1}, +publisher = {Cambridge University Press}, +title = {{Haskell 98 Language and Libraries The Revised Report}}, +url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144}, +volume = {13}, +year = {2003} +} +@article{Brady2006a, +author = {Brady, E and Hammond, K}, +file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf}, +journal = {\ldots of the 5th international conference on \ldots}, +keywords = {Dependent Types}, +mendeley-tags = {Dependent Types}, +title = {{A verified staged interpreter is a verified compiler}}, +url = {http://portal.acm.org/citation.cfm?id=1173706.1173724}, +year = {2006} +} +@article{burrows1990, +author = {Burrows, Michael and Abadi, Martin and Needham, Roger}, +file = {:home/edwin/Research/Papers/Mendeley/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf}, +journal = {ACM Transactions on Computer Systems}, +pages = {18----36}, +title = {{A logic of authentication}}, +url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569}, +volume = {8}, +year = {1990} +} +@phdthesis{McBride1999, +author = {McBride, Conor}, +file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf}, +keywords = {Dependent Types}, +mendeley-tags = {Dependent Types}, +school = {University of Edinburgh}, +title = {{Dependently typed functional programs and their proofs}}, +url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf}, +year = {1999} +} +@article{mcbride2010ornamental, +author = {McBride, Conor}, +file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf}, +journal = {Journal of Functional Programming}, +title = {{Ornamental algebras, algebraic ornaments}}, +url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf}, +year = {2010} +} +@inproceedings{czarnecki2004dsl, +author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.}, +booktitle = {Domain-Specific Program Generation}, +file = {:home/edwin/Research/Papers/Mendeley/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf}, +pages = {51--72}, +publisher = {Springer}, +title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}}, +url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf}, +year = {2004} +} +@article{Chapman2005epigram, +author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor}, +file = {:home/edwin/Research/Papers/Mendeley/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf}, +journal = {Trends in Functional Programming}, +publisher = {Intellect Books}, +title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}}, +url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY}, +year = {2005} +} +@inproceedings{Levitation2010, +author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter}, +booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}, +doi = {10.1145/1932681.1863547}, +file = {:home/edwin/Research/Papers/Mendeley/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf}, +isbn = {978-1-60558-794-3}, +issn = {03621340}, +keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems}, +mendeley-tags = {Dependent Types}, +month = sep, +number = {9}, +pages = {3}, +title = {{The gentle art of levitation}}, +url = {http://dl.acm.org/citation.cfm?id=1932681.1863547}, +volume = {45}, +year = {2010} +} +@inproceedings{pj2006gadts, +author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.}, +booktitle = {{International Conference on Functional Programming} ({ICFP} '06)}, +file = {:home/edwin/Research/Papers/Mendeley/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf}, +number = {9}, +pages = {50--61}, +publisher = {ACM}, +title = {{Simple unification-based type inference for GADTs}}, +url = {http://dl.acm.org/citation.cfm?id=1159811}, +volume = {41}, +year = {2006} +} +@article{McBride2004a, +abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.}, +author = {McBride, Conor and McKinna, James}, +doi = {10.1017/S0956796803004829}, +file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf}, +issn = {09567968}, +journal = {Journal of Functional Programming}, +keywords = {Dependent Types}, +mendeley-tags = {Dependent Types}, +number = {1}, +pages = {69--111}, +publisher = {Cambridge University Press}, +title = {{The view from the left}}, +url = {http://www.journals.cambridge.org/abstract_S0956796803004829}, +volume = {14}, +year = {2004} +} +@article{Altenkirch2010a, +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.}, +author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter}, +file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf}, +journal = {Citeseer}, +publisher = {Citeseer}, +title = {{Generic Programming with Dependent Types}}, +url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf}, +year = {2010} +} +@article{Steiner1988, +author = {Steiner, JG}, +file = {:home/edwin/Research/Papers/Mendeley/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf}, +journal = {Proc. Winter USENIX Conference}, +title = {{Kerberos: An authentication service for open network systems}}, +url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf}, +year = {1988} +} +@phdthesis{Okasaki1996, +author = {Okasaki, Chris}, +file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf}, +school = {Carnegie Mellon University}, +title = {{Purely Functional Data Structures}}, +year = {1996} +} +@article{Abel2010, +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.}, +author = {Abel, Andreas}, +file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf}, +journal = {EPTCS}, +pages = {1--15}, +title = {{MiniAgda: Integrating Sized and Dependent Types}}, +url = {http://arxiv.org/abs/1012.4896}, +volume = {43}, +year = {2010} +} +@inproceedings{Brady2006b, +author = {Brady, Edwin}, +booktitle = {Implementation and Application of Functional Languages ({IFL}'06)}, +file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf}, +isbn = {978-3-540-74129-9}, +month = sep, +pages = {145----162}, +title = {{Ivor, a proof engine}}, +url = {http://dl.acm.org/citation.cfm?id=1757028.1757037}, +year = {2006} +} +@article{Hughes1989, +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.}, +author = {Hughes, J}, +chapter = {2}, +doi = {10.1093/comjnl/32.2.98}, +editor = {Turner, David A}, +file = {:home/edwin/Research/Papers/Mendeley/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf}, +institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden}, +isbn = {0201172364}, +issn = {00104620}, +journal = {The Computer Journal}, +number = {2}, +pages = {98--107}, +publisher = {Br Computer Soc}, +title = {{Why Functional Programming Matters}}, +url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98}, +volume = {32}, +year = {1989} +} +@article{mccann2000packet, +author = {McCann, P.J. and Chandra, S.}, +journal = {ACM SIGCOMM Computer Communication Review}, +number = {4}, +pages = {321--333}, +publisher = {ACM}, +title = {{Packet types: abstract specification of network protocol messages}}, +url = {http://dl.acm.org/citation.cfm?id=347563}, +volume = {30}, +year = {2000} +} diff --git a/impl-paper/typechecking.tex b/impl-paper/typechecking.tex index aa98d0bb36..8fa7b10c7f 100644 --- a/impl-paper/typechecking.tex +++ b/impl-paper/typechecking.tex @@ -23,7 +23,7 @@ \subsection{\TT{} syntax} \item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants. \item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces. \item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the -type of types. +type of types, and may be extended with other primitives. \end{itemize} We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$, @@ -106,7 +106,7 @@ \subsubsection{Evaluation} is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$ then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of contractions and reversed contractions. Terms which are convertible are also said to -be computationally equal. +be definitionally equal. The evaluator can also be extended by defining pattern matching functions, which will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern matching functions can be understood as extending the core language with high level @@ -151,6 +151,30 @@ \subsubsection{Typing rules} \Rule{\Gamma\proves\RW{valid}} {\Gamma\vdash\Type_n\Hab\Type_{n+1}} \\ +\mathsf{Const}_1\: +\Rule{\Gamma\proves\RW{valid}} +{\Gamma\vdash\vi\Hab\TC{Int}} +\hg +\mathsf{Const}_2\: +\Rule{\Gamma\proves\RW{valid}} +{\Gamma\vdash\VV{str}\Hab\TC{String}} +\\ +\mathsf{Const}_3\: +\Rule{\Gamma\proves\RW{valid}} +{\Gamma\vdash\TC{Int}\Hab\Type_0} +\hg +\mathsf{Const}_4\: +\Rule{\Gamma\proves\RW{valid}} +{\Gamma\vdash\TC{String}\Hab\Type_0} +\\ +%\mathsf{Pat}_1\: +%\Rule{(\pat{\vx}{\vS})\in\Gamma} +%{\Gamma\vdash\vx\Hab\vS} +%\hg +%\mathsf{Pat}_2\: +%\Rule{(\pty{\vx}{\vS})\in\Gamma} +%{\Gamma\vdash\vx\Hab\vS} +\\ \mathsf{Var}_1\: \Rule{(\lam{\vx}{\vS})\in\Gamma} {\Gamma\vdash\vx\Hab\vS} @@ -163,14 +187,6 @@ \subsubsection{Typing rules} \Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma} {\Gamma\vdash\vx\Hab\vS} \\ -%\mathsf{Pat}_1\: -%\Rule{(\pat{\vx}{\vS})\in\Gamma} -%{\Gamma\vdash\vx\Hab\vS} -%\hg -%\mathsf{Pat}_2\: -%\Rule{(\pty{\vx}{\vS})\in\Gamma} -%{\Gamma\vdash\vx\Hab\vS} -\\ \mathsf{App}\: \Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS} {\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT} @@ -230,7 +246,7 @@ \subsection{Inductive Families} \remph{values} as well as types. An inductive family is declared in a similar style to a Haskell GADT declaration~\cite{pj2006gadts} as -follows, using the de Bruijn telescope notation, $\tx$, to indicate a +follows, using vector notation, $\tx$, to indicate a sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$): \DM{ @@ -351,7 +367,7 @@ \subsubsection{Semantics} to match against it) if it is constructor headed, or a variable. Inaccessible patterns are converted to ``match anything'' patterns. We convert clauses to matchable pattern clauses with the $\MO{Clause}$ operation, given in Figure \ref{mkclause}. -We extend the telescope notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the +We extend the vector notation to meta-operations: the notation $\vec{\MO{Pat}}$ lifts the $\MO{Pat}$ operation across a list of arguments. \FFIG{ @@ -444,6 +460,25 @@ \subsubsection{Semantics} In practice, for efficiency, pattern matching is implemented by compiling the match clauses to a tree of case expressions~\cite{Augustsson1985}. +\subsection{Totality checking} + +In order to ensure termination of type checking, and therefore its decidability, +we must distinguish terms for which evaluation definitely terminates, and +those which may diverge. \TT{} takes a simple but pragmatic and +effective approach to termination +checking: any functions which do not satisfy a syntactic constraint on recursive +calls are marked as \emph{partial}. Additionally, any function which calls a partial +function are uses a data type which is not strictly positive is also marked as +partial. The syntactic constraint we use is that a recursive call in a pattern +clause must have an argument which is structurally smaller than an input argument +in the same position. \TT{} also marks functions which do not cover all possible +inputs as partial. This totality checking is independent of the rest of the type +theory, and can be extended in future. + +This approach, separating the termination requirement from the type theory, means that +an \Idris{} programmer makes the decision about the importance of totality for each +function rather than having the totality requirement imposed by the type theory. + \subsection{From \Idris{} to \TT{}} \TT{} is a very small language, consisting only of data declarations and pattern matching