git.iko.soy/Idris-dev
on master help sign in
related work and conclusion
20f5db1Edwin Brady
impl-paper/conclusions.tex+109−20
compare with master
unifiedsplit
@@ -2,33 +2,122 @@
2
2
3\label{sect:discussion}
3\label{sect:discussion}
4
4
5−Since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it makes
6−sense to expose the tactic language to the programmer.
7−Also tactic-implicit arguments as a generalisation of instance resolution.
8−
9−Discuss performance (anecdotally, how big is the library and how long to check,
5+%Discuss performance (anecdotally, how big is the library and how long to check,
10−and relative to previous version).
6+%and relative to previous version).
11
7
12\subsection{Related Work}
8\subsection{Related Work}
13
9
14−Oleg~\cite{McBride1999} as inspiration. \Epigram{}~\cite{McBride2004a}.
10+Dependently typed programming languages have becoming more prominent in recent
15−How does Agda~\cite{norell2007thesis} work?
11+years as tools for verifying software correctness, and several experimental
16−Earlier \Idris{}, with \Ivor{}~\cite{Brady2006b}.
12+languages are being developed, in particular Agda \cite{norell2007thesis}, Epigram
13+\cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.
14+
15+An earlier implementation of \Idris{} was built on the \Ivor{} proof engine
16+\cite{Brady2006b}. This implementation differed in one important way --- unlike
17+the present implementation, there was limited separation between the type theory
18+and the high level language. The type theory itself supported implicit syntax and
19+unification, with high level constructs such as the \texttt{with} rule implemented
20+directly. Two important disadvantages were found with this approach, however:
21+firstly, the type checker is much more complicated when combined with
22+unification, making it harder to maintain; secondly, adding new high level features
23+requires the type checker to support those features directly. In contrast, elaboration
24+by tactics gives a clean separation between the low level and high level languages.
25+
26+The Agda implementation is based on a type theory with
27+implicit syntax and pattern matching --- Norell gives an algorithm for type checking
28+a dependently typed language with pattern matching and metavariables
29+\cite{norell2007thesis}. Unlike the present \Idris{} implementation, metavariables
30+and implicit arguments are part of the type theory. This has the advantage that
31+implicit arguments can be used more freely, at the expense of complicating the type
32+system.
33+
34+Epigram \cite{McBride2004a} and Oleg \cite{McBride1999}
35+have provided much of the inspiration for the \Idris{} elaborator. Indeed,
36+the hole and guess bindings of \TTdev{} are taken directly from Oleg.
37+\Epigram{} does not implement pattern matching directly, but rather translates
38+pattern matching into elimination rules \cite{McBride2002}. This has the
39+advantage that
40+elimination rules provide termination and coverage proofs \emph{by construction}.
41+Furthermore they simplify implementation of the evaluator and provide easy
42+optimisation opportunities \cite{Brady2003}. However, it requires the
43+implementation of extra machinery for constructor manipulation
44+\cite{McBride2006} and so we have avoided it in the present implementation.
45+
46+%Comparison with GHC's type system and type checker. \cite{Vytiniotis2011}
17
47
18−Comparison with GHC's type system and type checker.
48+%[Observation: separate elaboration and type checking, sort of like in GHC which
49+%type checks the high level language and produces a type correct core language.
50+%Elaboration is effectively a type checker for the high level language, so we have
51+%a hope of providing reasonable error messages related to the original code.]
19
52
20\subsection{Conclusion}
53\subsection{Conclusion}
21
54
22−[Observation: separate elaboration and type checking, sort of like in GHC which
55+In this paper, I have given an overview of the programming language \Idris{},
23−type checks the high level language and produces a type correct core language.
56+and its core type theory \TT{}, giving a detailed algorithm for translating
24−Elaboration is effectively a type checker for the high level language, so we have
57+high level programs into \TT{}.
25−a hope of providing reasonable error messages related to the original code.]
58+\TT{} itself is deliberately small and simple, and the design has deliberately
59+resisted innovation so that we can rely on existing metatheoretic properties
60+being preserved. The kernel of the \Idris{} implementation consists of a type checker
61+and evaluator for \TT{} along with a pattern match compiler, which are implemented
62+in under 1000 lines of Haskell code. It is important that this kernel remains small
63+--- the correctness of the language implementation relies to a large extent on
64+the correctness of the underlying type system, and keeping the implementation small
65+reduces the possibility of errors.
66+
67+The approach we have taken to implementing the high level language, implementing
68+a tactic language as an embedded DSL, allows us to
69+build programs on top of a small and unchanging kernel, rather than extending
70+the core language to deal with implicit syntax, unification and type classes.
71+High level \Idris{} features are implemented by describing the corresponding
72+sequence of tactics to build an equivalent program in \TT{}, via a development
73+calculus of incomplete terms, \TTdev{}. A significant advantage we have found with
74+this approach is that higher level features can easily be implemented in terms
75+of existing elaborator components. For example, once we have implemented elaboration
76+for data types and functions, it is easy to add several features:
77+
78+\begin{itemize}
79+\item \textbf{Type classes}: A dictionary is merely a record containing the
80+functions which implement a type class instance. Since we have a tactic based
81+refinement engine, we can implement type class resolution as a tactic.
82+\item \textbf{\texttt{where} clauses}: We have access to local variables and
83+their types, so we can
84+elaborate \texttt{where} clauses at the point of definition simply by lifting
85+them to the top level.
86+\item \textbf{\texttt{case} expressions}: Similar to \texttt{where} clauses,
87+these are implemented by lifting the branches out to a top level function.
88+\end{itemize}
89+
90+We do not need to make any changes to the core language type system in order to
91+implement these high level features.
92+Other high level features such as dependent records, tuples and monad comprehensions
93+can be added equally easily. Furthermore,
94+since we have used a tactic-based EDSL to elaborate \Idris{} to \TT{}, it is
95+possible to expose the tactic language to the programmer. This opens up the
96+possibility of implementing domain specific decision procedures, or implementing
97+user defined tactics in a style similar to Coq's \texttt{Ltac} language \cite{Bertot2004}.
98+
99+The objective of this implementation of \Idris{} is to provide a platform
100+for experimenting with realistic, general purpose programming with dependent
101+types, by implementing a Haskell-like language augmented with \emph{full}
102+dependent types.
103+In this paper, we have seen how such a high level language can be implemented
104+by building on top of a small, well-understood, easy to reason about type
105+theory. However, a programming language implementation is not an end in itself.
106+Programming languages exist to support research and practice in many different
107+domains. In future work, therefore, we plan to apply domain specific
108+language based techniques to realistic problems
109+in important safety critical domains such as security and network protocol
110+design and implementation. In order to be successful, we need a language which
111+is expressive enough to describe protocol specifications at a high level, and robust
112+enough to guarantee correct implementation of those protocols. We hope that \Idris{}
113+is that language!
114+
26
115
27
116
28−\subsection{Further Work}
117+%\subsection{Further Work}
29
118
30−[Would the EDSL approach work in other languages? Adding components of DTP
119+%[Would the EDSL approach work in other languages? Adding components of DTP
31−to imperative languages, say, using \TT{} as a verified core.
120+%to imperative languages, say, using \TT{} as a verified core.
32−\Idris{} implementation as the beginning of a project to explore practical
121+%\Idris{} implementation as the beginning of a project to explore practical
33−DTP --- systems, protocols, security especially. And just having full
122+%DTP --- systems, protocols, security especially. And just having full
34−dependent types for lightweight correctness guarantees.]
123+%dependent types for lightweight correctness guarantees.]
impl-paper/library.bib+988−958
@@ -1,55 +1,96 @@
1Automatically generated by Mendeley 1.3.1
1Automatically generated by Mendeley 1.3.1
2Any changes to this file will be lost if it is regenerated by Mendeley.
2Any changes to this file will be lost if it is regenerated by Mendeley.
3
3
4−@inproceedings{ko2011modularising,
4+@article{McBride2006,
5−author = {Ko, H.S. and Gibbons, J.},
5+author = {McBride, C and Goguen, Healfdene and McKinna, James},
6−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
6+journal = {Types for Proofs and Programs},
7−file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
7+title = {{A few constructions on constructors}},
8−pages = {13--24},
8+url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
9−publisher = {ACM},
10−title = {{Modularising inductive families}},
11−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},
12−year = {2011}
9+year = {2006}
13}
10}
14−@inproceedings{gibbons2011modularising,
11+@inproceedings{czarnecki2004dsl,
15−author = {Gibbons, J. and Ko, H.S. and Others},
12+author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},
16−file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
13+booktitle = {Domain-Specific Program Generation},
17−title = {{Modularising inductive families}},
14+file = {:Users/edwin/Documents/Mendeley Desktop/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},
18−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
15+pages = {51--72},
16+publisher = {Springer},
17+title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},
18+url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},
19+year = {2004}
20+}
21+@phdthesis{Brady2005,
22+author = {Brady, Edwin},
23+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
24+keywords = {Dependent Types},
25+mendeley-tags = {Dependent Types},
26+school = {University of Durham},
27+title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},
28+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf},
29+year = {2005}
30+}
31+@inproceedings{Kimmell2012,
32+author = {Kimmell, G and Stump, A and {Eades III}, HD and Fu, Peng and Sheard, Tim and Weirich, S and Casinghino, C and Sj\"{o}berg, V and Collins, N and Ahn, KY},
33+booktitle = {Programming Languages meets Program Verification},
34+title = {{Equational reasoning about programs with general recursion and call-by-value semantics}},
35+url = {http://dl.acm.org/citation.cfm?id=2103780},
36+year = {2012}
37+}
38+@article{Epstein2011,
39+author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},
40+institution = {Microsoft Research},
41+journal = {researchmicrosoftcom},
42+number = {Section 8},
43+pages = {1--12},
44+title = {{Haskell for the cloud}},
45+url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf},
19year = {2011}
46year = {2011}
20}
47}
21−@article{Okasaki1993,
48+@article{Altenkirch2010a,
22−author = {Okasaki, Chris},
49+abstract = {We begin by revisiting the idea of using a universe of types to write generic programs in a dependently typed setting by constructing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Positive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach presented here we are able to represent all of Epigrams datatypes within Epigram including the universe of datatypes itself.},
23−file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
50+author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},
24−journal = {Journal of functional programming},
51+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
25−title = {{Red-Black Trees in A Functional Setting}},
52+journal = {Citeseer},
53+publisher = {Citeseer},
54+title = {{Generic Programming with Dependent Types}},
55+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf},
26−year = {1993}
56+year = {2010}
27}
57}
28−@misc{Brady2012b,
58+@article{fisher2006next,
59+author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},
60+file = {:Users/edwin/Documents/Mendeley Desktop/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},
61+journal = {Journal of the ACM},
62+number = {2},
63+pages = {1--51},
64+publisher = {ACM},
65+title = {{The next 700 data description languages}},
66+url = {http://dl.acm.org/citation.cfm?id=1111039},
67+volume = {15},
68+year = {2010}
69+}
70+@misc{The2012b,
29author = {Brooks, Fred},
71author = {Brooks, Fred},
30doi = {10.1093/epirev/mxr031},
72doi = {10.1093/epirev/mxr031},
31−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
73+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
32isbn = {9780321702081},
74isbn = {9780321702081},
33issn = {1478-6729},
75issn = {1478-6729},
34pmid = {22215642},
76pmid = {22215642},
35−title = {{The Design of Design Chapter 2}}
77+title = {{The Design of Design Chapter 1}}
36}
78}
37−@inproceedings{Brady2003,
79+@article{Chapman2005epigram,
38−author = {Brady, Edwin and McBride, Conor and McKinna, James},
80+author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},
39−booktitle = {Types for Proofs and Programs},
81+file = {:Users/edwin/Documents/Mendeley Desktop/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},
40−file = {:home/edwin/Research/Papers/Mendeley/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},
82+journal = {Trends in Functional Programming},
41−keywords = {Dependent Types},
83+publisher = {Intellect Books},
42−mendeley-tags = {Dependent Types},
84+title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
43−title = {{Inductive families need not store their indices}},
85+url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
44−url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},
45−year = {2003}
86+year = {2005}
46}
87}
47@misc{TheMendeleySupportTeam2011,
88@misc{TheMendeleySupportTeam2011,
48abstract = {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.},
89abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
49address = {London},
90address = {London},
50author = {{The Mendeley Support Team}},
91author = {{The Mendeley Support Team}},
51booktitle = {Mendeley Desktop},
92booktitle = {Mendeley Desktop},
52−file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
93+file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
53keywords = {Mendeley,how-to,user manual},
94keywords = {Mendeley,how-to,user manual},
54pages = {1--16},
95pages = {1--16},
55publisher = {Mendeley Ltd.},
96publisher = {Mendeley Ltd.},
@@ -57,78 +98,52 @@ title = {{Getting Started with Mendeley}},
57url = {http://www.mendeley.com},
98url = {http://www.mendeley.com},
58year = {2011}
99year = {2011}
59}
100}
60−@inproceedings{Wadler1989,
101+@phdthesis{Okasaki1996,
61−abstract = {From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds' abstraction theorem for the polymorphic lambda calculus.},
102+author = {Okasaki, Chris},
62−author = {Wadler, Philip},
103+file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
63−booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
104+school = {Carnegie Mellon University},
64−doi = {10.1145/99370.99404},
105+title = {{Purely Functional Data Structures}},
65−file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},
66−isbn = {0897913280},
67−number = {June},
68−pages = {347--359},
69−publisher = {ACM},
70−series = {FPCA '89},
71−title = {{Theorems for free!}},
72−url = {http://portal.acm.org/citation.cfm?id=99404},
73−year = {1989}
106+year = {1996}
74}
107}
75−@phdthesis{norell2007thesis,
108+@article{mcbride2008functional,
76−author = {Norell, Ulf},
109+author = {McBride, C. and Paterson, R.},
77−file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
110+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
78−keywords = {Dependent Types},
111+journal = {Journal of functional programming},
79−mendeley-tags = {Dependent Types},
112+number = {1},
113+pages = {1--13},
80−publisher = {Citeseer},
114+publisher = {Cambridge Univ Press},
81−school = {Chalmers University of Technology},
115+title = {{Functional pearl: Applicative programming with effects}},
82−title = {{Towards a practical programming language based on dependent type theory}},
116+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=1457860},
83−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
117+volume = {18},
84−year = {2007}
118+year = {2008}
85}
119}
86−@inproceedings{l,
120+@inproceedings{madhavapeddy2007melange,
87−author = {L\"{a}mmel, R. and Jones, S.P.},
121+author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
88−booktitle = {ACM SIGPLAN Notices},
122+booktitle = {ACM SIGOPS Operating Systems Review},
89−file = {:home/edwin/Research/Papers/Mendeley/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},
123+file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},
90number = {3},
124number = {3},
91−pages = {26--37},
125+pages = {101--114},
92publisher = {ACM},
126publisher = {ACM},
93−title = {{Scrap your boilerplate: a practical design pattern for generic programming}},
127+title = {{Melange: creating a functional internet}},
94−url = {http://dl.acm.org/citation.cfm?id=640136.604179},
128+url = {http://dl.acm.org/citation.cfm?id=1273009},
95−volume = {38},
96−year = {2003}
97−}
98−@inproceedings{Xi1999,
99−abstract = {Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.},
100−author = {Xi, Hongwei and Pfenning, Frank},
101−booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},
102−doi = {10.1145/292540.292560},
103−file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},
104−isbn = {1581130953},
105−issn = {07439016},
106−keywords = {Dependent Types},
107−mendeley-tags = {Dependent Types},
108−organization = {Carnegie Mellon University},
109−pages = {214--227},
110−publisher = {ACM Press},
111−series = {POPL '99},
112−title = {{Dependent types in practical programming}},
113−url = {http://portal.acm.org/citation.cfm?doid=292540.292560},
114−volume = {26},
129+volume = {41},
115−year = {1999}
130+year = {2007}
116}
131}
117−@inproceedings{morris2006exploring,
132+@inproceedings{lempsink2009type,
118−author = {Morris, P. and Altenkirch, T. and McBride, C.},
133+author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},
119−booktitle = {Types for Proofs and Programs},
134+booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},
120−file = {:home/edwin/Research/Papers/Mendeley/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},
135+file = {:Users/edwin/Documents/Mendeley Desktop/Lempsink, Leather, L\"{o}h/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},
121−pages = {252--267},
136+pages = {61--72},
122−publisher = {Springer},
137+publisher = {ACM},
123−title = {{Exploring the regular tree types}},
138+title = {{Type-safe diff for families of datatypes}},
124−url = {http://www.springerlink.com/index/f9p1317716614834.pdf},
139+url = {http://dl.acm.org/citation.cfm?id=1596624},
125−year = {2006}
140+year = {2009}
126}
141}
127@book{Approach2012,
142@book{Approach2012,
128author = {Hunt, Andrew and Thomas, David},
143author = {Hunt, Andrew and Thomas, David},
129booktitle = {Carcinogenesis},
144booktitle = {Carcinogenesis},
130doi = {10.1093/carcin/bgs054},
145doi = {10.1093/carcin/bgs054},
131−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
146+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
132isbn = {020161622X},
147isbn = {020161622X},
133issn = {1460-2180},
148issn = {1460-2180},
134number = {3},
149number = {3},
@@ -137,99 +152,220 @@ title = {{The Pragmatic Programmer Chapter 2}},
137url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
152url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
138volume = {33}
153volume = {33}
139}
154}
140−@article{Miller1992,
141−author = {Miller, D},
142−file = {:home/edwin/Research/Papers/Mendeley/Miller/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},
143−journal = {Journal of symbolic computation},
144−title = {{Unification under a mixed prefix}},
145−url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},
146−year = {1992}
147−}
148−@misc{Interface2012a,
149−author = {Kreibich, Jay A.},
150−doi = {10.1093/epirev/mxr031},
151−file = {:home/edwin/Research/Papers/Mendeley/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
152−isbn = {9781449394592},
153−issn = {1478-6729},
154−pmid = {22215642},
155−title = {{Using SQLite Chapter 7}}
156−}
157−@inproceedings{chlipala2010ur,
155+@inproceedings{stump2010resource,
158−author = {Chlipala, Adam},
156+author = {Stump, A. and Austin, E.},
159−booktitle = {ACM SIGPLAN Notices},
157+booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},
160−file = {:home/edwin/Research/Papers/Mendeley/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
158+file = {:Users/edwin/Documents/Mendeley Desktop/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},
161−number = {6},
162−pages = {122--133},
159+pages = {27--38},
163publisher = {ACM},
160publisher = {ACM},
164−title = {{Ur: statically-typed metaprogramming with type-level record computation}},
161+title = {{Resource typing in Guru}},
165−url = {http://dl.acm.org/citation.cfm?id=1806612},
162+url = {http://dl.acm.org/citation.cfm?id=1707796},
166−volume = {45},
167year = {2010}
163year = {2010}
168}
164}
169−@book{peyton1987implementation,
165+@article{mcbride2010ornamental,
170−author = {{Peyton Jones}, S.L.},
166+author = {McBride, Conor},
171−publisher = {Prentice-Hall, Inc.},
167+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
172−title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}},
168+journal = {Journal of Functional Programming},
173−url = {http://dl.acm.org/citation.cfm?id=1096899},
169+title = {{Ornamental algebras, algebraic ornaments}},
170+url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},
174−year = {1987}
171+year = {2010}
175}
172}
176−@article{dybjer1994inductive,
173+@article{Swierstra2011,
177−author = {Dybjer, P.},
174+author = {Swierstra, W},
178−journal = {Formal aspects of computing},
175+file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},
176+journal = {Journal of Functional Programming},
179−number = {4},
177+number = {6},
180−pages = {440--465},
178+pages = {575----583},
181−publisher = {Springer},
179+title = {{Sorted: Verifying the Problem of the {Dutch National} Flag in {Agda}}},
182−title = {{Inductive families}},
180+url = {http://journals.cambridge.org/abstract_S0956796811000207},
183−url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
184−volume = {6},
181+volume = {21},
185−year = {1994}
182+year = {2011}
186}
183}
187−@inproceedings{lempsink2009type,
184+@article{McBride2002,
188−author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},
185+author = {McBride, C},
189−booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},
186+journal = {Types for proofs and programs},
190−file = {:home/edwin/Research/Papers/Mendeley/Lempsink, Leather, L\"{o}h/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},
187+title = {{Elimination with a Motive}},
188+url = {http://www.springerlink.com/index/vbpg19305t46f6dm.pdf},
189+year = {2000}
190+}
191+@article{Xi1998,
192+abstract = {We present a type-based approach to eliminating array bound checking and list tag checking by conservatively extending Standard ML with a restricted form of dependent types. This enables the programmer to capture more invariants through types while type-checking remains decidable in theory and can still be performed efficiently in practice. We illustrate our approach through concrete examples and present the result of our preliminary experiments which support support the feasibility and effectiveness of our approach.},
193+author = {Xi, Hongwei and Pfenning, Frank},
194+doi = {10.1145/277652.277732},
195+file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},
196+isbn = {0897919874},
197+issn = {03621340},
198+journal = {ACM Sigplan Notices},
199+keywords = {Dependent Types},
200+mendeley-tags = {Dependent Types},
201+number = {5},
191−pages = {61--72},
202+pages = {249--257},
192publisher = {ACM},
203publisher = {ACM},
193−title = {{Type-safe diff for families of datatypes}},
204+series = {PLDI '98},
205+title = {{Eliminating array bound checking through dependent types}},
194−url = {http://dl.acm.org/citation.cfm?id=1596624},
206+url = {http://portal.acm.org/citation.cfm?doid=277652.277732},
207+volume = {33},
195−year = {2009}
208+year = {1998}
196}
209}
197−@misc{The2012b,
210+@misc{idristutorial,
211+author = {Brady, Edwin},
212+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
213+title = {{Programming in Idris : a tutorial}},
214+url = {http://idris-lang.org/tutorial},
215+year = {2012}
216+}
217+@inproceedings{NanevskiAAMorrisett2008,
218+abstract = {We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions. The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which, abstracts the implementation details and ensures that the modules properly implement the finite map abstraction. Copyright 2008 ACM.},
219+author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},
220+booktitle = {International Conference on Functional Programming},
221+doi = {10.1145/1411204.1411237},
222+file = {:Users/edwin/Documents/Mendeley Desktop/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},
223+isbn = {9781595939197},
224+issn = {15232867},
225+keywords = {Dependent Types},
226+mendeley-tags = {Dependent Types},
227+number = {9},
228+pages = {229--240},
229+title = {{Ynot: Dependent types for imperative programs}},
230+url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},
231+volume = {43},
232+year = {2008}
233+}
234+@misc{Brady2012c,
198−author = {Brooks, Fred},
235+author = {Brooks, Fred},
199doi = {10.1093/epirev/mxr031},
236doi = {10.1093/epirev/mxr031},
200−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
237+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},
201isbn = {9780321702081},
238isbn = {9780321702081},
202issn = {1478-6729},
239issn = {1478-6729},
240+number = {1},
241+pages = {NP},
203pmid = {22215642},
242pmid = {22215642},
204−title = {{The Design of Design Chapter 1}}
243+title = {{The Design of Design Chapter 5}},
244+volume = {34}
205}
245}
206−@misc{The2012c,
246+@inproceedings{ko2011modularising,
207−author = {Robbins, A and Hannah, E and Lamb, L},
247+author = {Ko, H.S. and Gibbons, J.},
208−doi = {10.1093/epirev/mxr031},
248+booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
209−file = {:home/edwin/Research/Papers/Mendeley/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
249+file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
210−isbn = {9780596529833},
250+pages = {13--24},
211−issn = {1478-6729},
251+publisher = {ACM},
212−pmid = {22215642},
252+title = {{Modularising inductive families}},
213−title = {{Learning the vi and Vim Editors}}
253+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},
254+year = {2011}
214}
255}
215−@book{Brady2012,
256+@book{Choosing2012,
216−author = {Hunt, Andrew and Thomas, David},
257+author = {Fowler, Martin},
217booktitle = {Carcinogenesis},
258booktitle = {Carcinogenesis},
218doi = {10.1093/carcin/bgs054},
259doi = {10.1093/carcin/bgs054},
219−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
260+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
220−isbn = {020161622X},
261+isbn = {9780132107549},
221issn = {1460-2180},
262issn = {1460-2180},
222number = {3},
263number = {3},
223pmid = {22383472},
264pmid = {22383472},
224−title = {{The Pragmatic Programmer Chapter 5}},
265+title = {{Domain Specific Languages Chapter 6}},
225url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
266url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
226volume = {33}
267volume = {33}
227}
268}
269+@article{marlow2006making,
270+author = {Marlow, S. and {Peyton Jones}, S.},
271+file = {:Users/edwin/Documents/Mendeley Desktop/Marlow, Peyton Jones/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},
272+journal = {Journal of Functional Programming},
273+number = {4-5},
274+pages = {415--449},
275+publisher = {Cambridge University Press},
276+title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}},
277+url = {http://dl.acm.org/citation.cfm?id=1166018},
278+volume = {16},
279+year = {2006}
280+}
281+@article{Mandelbaum2007,
282+abstract = {Massive amounts of useful data are stored and processed in ad hoc formats for which common tools like parsers, printers, query engines and format converters are not readily available. In this paper, we explain the design and implementation of PADS/ML , a new language and system that facilitates the generation of data processing tools for ad hoc formats. The PADS/ML design includes features such as dependent, polymorphic and recursive datatypes, which allow programmers to describe the syntax and semantics of ad hoc data in a concise, easy-to-read notation. The PADS/ML implementation compiles these descriptions into ml structures and functors that include types for parsed data, functions for parsing and printing, and auxiliary support for user-specified, format-dependent and format-independent tool generation.},
283+author = {Mandelbaum, Yitzhak and Fisher, Kathleen and Walker, David and Fernandez, Mary and Gleyzer, Artem},
284+doi = {10.1145/1190215.1190231},
285+isbn = {1595935754},
286+issn = {03621340},
287+journal = {SIGPLAN Not},
288+number = {1},
289+pages = {77--83},
290+publisher = {ACM},
291+series = {POPL '07},
292+title = {{PADS/ML: a functional data description language}},
293+url = {http://doi.acm.org/10.1145/1190216.1190231},
294+volume = {42},
295+year = {2007}
296+}
297+@article{Abel2010,
298+abstract = {Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.},
299+author = {Abel, Andreas},
300+file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
301+journal = {EPTCS},
302+pages = {1--15},
303+title = {{MiniAgda: Integrating Sized and Dependent Types}},
304+url = {http://arxiv.org/abs/1012.4896},
305+volume = {43},
306+year = {2010}
307+}
308+@article{Hoare1978,
309+abstract = {This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of a familiar programming exercises.},
310+author = {Hoare, C A R},
311+doi = {10.1016/0167-6423(87)90028-1},
312+editor = {McKeag, R M and Macnaghten, A M},
313+file = {:Users/edwin/Documents/Mendeley Desktop/Hoare/Hoare - 1978 - Communicating sequential processes.pdf:pdf},
314+isbn = {0131532715},
315+issn = {01676423},
316+journal = {Communications of the ACM},
317+number = {8},
318+pages = {666--677},
319+pmid = {2142694823583477576},
320+publisher = {ACM},
321+series = {International Series in Computer Science},
322+title = {{Communicating sequential processes}},
323+url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},
324+volume = {21},
325+year = {1978}
326+}
327+@book{Bird2010,
328+author = {Bird, Richard},
329+file = {:Users/edwin/Documents/Mendeley Desktop/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
330+isbn = {9780521513388},
331+title = {{Pearls of Functional Algorithm Design}},
332+year = {2010}
333+}
334+@inproceedings{oury2008power,
335+author = {Oury, N. and Swierstra, W.},
336+booktitle = {International Conference on Functional Programming},
337+file = {:Users/edwin/Documents/Mendeley Desktop/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
338+keywords = {Dependent Types},
339+mendeley-tags = {Dependent Types},
340+number = {9},
341+pages = {39--50},
342+publisher = {ACM},
343+title = {{The power of Pi}},
344+url = {http://dl.acm.org/citation.cfm?id=1411213},
345+volume = {43},
346+year = {2008}
347+}
348+@inproceedings{madhavapeddy2010turning,
349+author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
350+booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
351+file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},
352+publisher = {USENIX Association},
353+title = {{Turning down the LAMP: software specialisation for the cloud}},
354+url = {http://dl.acm.org/citation.cfm?id=1863114},
355+year = {2010}
356+}
357+@book{peyton1987implementation,
358+author = {{Peyton Jones}, S.L.},
359+publisher = {Prentice-Hall, Inc.},
360+title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}},
361+url = {http://dl.acm.org/citation.cfm?id=1096899},
362+year = {1987}
363+}
228@inproceedings{Pasalic2002,
364@inproceedings{Pasalic2002,
229author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},
365author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},
230booktitle = {International Conference on Functional Programming},
366booktitle = {International Conference on Functional Programming},
231doi = {10.1145/583852.581499},
367doi = {10.1145/583852.581499},
232−file = {:home/edwin/Research/Papers/Mendeley/Pa\v{s}alic, Taha, Sheard/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},
368+file = {:Users/edwin/Documents/Mendeley Desktop/Pa\v{s}alic, Taha, Sheard/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},
233isbn = {1-58113-487-8},
369isbn = {1-58113-487-8},
234issn = {03621340},
370issn = {03621340},
235keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},
371keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},
@@ -241,37 +377,95 @@ url = {http://dl.acm.org/citation.cfm?id=583852.581499},
241volume = {37},
377volume = {37},
242year = {2002}
378year = {2002}
243}
379}
244−@misc{Nodes2012a,
380+@inproceedings{Brady2010,
245−author = {Brooks, Fred},
381+author = {Brady, Edwin and Hammond, Kevin},
246−doi = {10.1093/epirev/mxr031},
382+booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
247−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
383+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},
248−isbn = {9780321702081},
384+isbn = {9781605587943},
249−issn = {1478-6729},
385+keywords = {Dependent Types,code generation gives,contrast,dependent types,efficient,harder,however,implementation,likely efficient,ness interpreter,partial evaluation,resulting implementation,un,verify its correctness},
250−pmid = {22215642},
386+mendeley-tags = {Dependent Types},
251−title = {{The Design of Design Chapter 3}}
387+pages = {297--308},
388+publisher = {ACM},
389+title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},
390+url = {http://portal.acm.org/citation.cfm?id=1863587},
391+year = {2010}
392+}
393+@inproceedings{Fournet2011,
394+author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},
395+booktitle = {Foundations of security analysis and design {VI}},
396+file = {:Users/edwin/Documents/Mendeley Desktop/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},
397+title = {{Cryptographic verification by typing for a sample protocol implementation}},
398+url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
399+year = {2010}
400+}
401+@article{landin1966next,
402+author = {Landin, P.J.},
403+file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
404+journal = {Communications of the ACM},
405+number = {3},
406+pages = {157--166},
407+publisher = {ACM},
408+title = {{The next 700 programming languages}},
409+url = {http://dl.acm.org/citation.cfm?id=365257 )},
410+volume = {9},
411+year = {1966}
412+}
413+@inproceedings{bhargavan2010modular,
414+author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},
415+booktitle = {ACM Sigplan Notices},
416+number = {1},
417+pages = {445--456},
418+publisher = {ACM},
419+title = {{Modular verification of security protocol code by typing}},
420+url = {http://dl.acm.org/citation.cfm?id=1707801.1706350},
421+volume = {45},
422+year = {2010}
252}
423}
253@article{Haskell2012a,
424@article{Haskell2012a,
254author = {Biancuzzi, F and Warden, S},
425author = {Biancuzzi, F and Warden, S},
255doi = {10.1093/epirev/mxr031},
426doi = {10.1093/epirev/mxr031},
256−file = {:home/edwin/Research/Papers/Mendeley/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
427+file = {:Users/edwin/Documents/Mendeley Desktop/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
257isbn = {9780596801670},
428isbn = {9780596801670},
258issn = {1478-6729},
429issn = {1478-6729},
259pmid = {22215642},
430pmid = {22215642},
260title = {{Masterminds of Programming Chapter 8}}
431title = {{Masterminds of Programming Chapter 8}}
261}
432}
262−@book{An2012,
433+@book{Brady2012,
263−author = {Fowler, Martin},
434+author = {Hunt, Andrew and Thomas, David},
264booktitle = {Carcinogenesis},
435booktitle = {Carcinogenesis},
265doi = {10.1093/carcin/bgs054},
436doi = {10.1093/carcin/bgs054},
266−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
437+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
267−isbn = {9780132107549},
438+isbn = {020161622X},
268issn = {1460-2180},
439issn = {1460-2180},
269number = {3},
440number = {3},
270pmid = {22383472},
441pmid = {22383472},
271−title = {{Domain Specific Languages Chapter 1}},
442+title = {{The Pragmatic Programmer Chapter 5}},
272url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
443url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
273volume = {33}
444volume = {33}
274}
445}
446+@article{McBride2007,
447+author = {McBride, Conor and Paterson, Ross},
448+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
449+journal = {Journal of functional programming},
450+title = {{Applicative programming with effects}},
451+url = {http://journals.cambridge.org/abstract_S0956796807006326},
452+year = {2007}
453+}
454+@inproceedings{Altenkirch2010,
455+abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
456+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas},
457+booktitle = {{FLOPS 2010}},
458+doi = {10.1007/978-3-642-12251-4_5},
459+editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
460+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
461+isbn = {9783642122507},
462+pages = {40----55},
463+publisher = {Springer Berlin Heidelberg},
464+series = {Lecture Notes in Computer Science},
465+title = {{Dependent Types without the Sugar}},
466+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
467+year = {2010}
468+}
275@article{McBride2005,
469@article{McBride2005,
276author = {McBride, Conor},
470author = {McBride, Conor},
277editor = {Vene, Varmo and Uustalu, Tarmo},
471editor = {Vene, Varmo and Uustalu, Tarmo},
@@ -287,229 +481,147 @@ url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},
287volume = {3622},
481volume = {3622},
288year = {2005}
482year = {2005}
289}
483}
290−@misc{Resolution2012a,
484+@misc{Bloat,
291−author = {Fall, Kevin R and Stevens, W. Richard},
485+author = {Brooks, Fred},
486+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},
487+isbn = {9780321702081},
488+title = {{The Design of Design Chapter 4}}
489+}
490+@misc{Protocols2012a,
491+author = {Anderson, Ross},
292doi = {10.1093/epirev/mxr031},
492doi = {10.1093/epirev/mxr031},
293−file = {:home/edwin/Research/Papers/Mendeley/Fall, Stevens/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},
493+file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
494+isbn = {9780470068526},
294issn = {1478-6729},
495issn = {1478-6729},
295pmid = {22215642},
496pmid = {22215642},
296−title = {{TCP/IP Illustrated Volume 1 Chapter 11}}
497+title = {{Security Engineering Chapter 3}}
297−}
298−@phdthesis{Brady2005,
299−author = {Brady, Edwin},
300−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
301−keywords = {Dependent Types},
302−mendeley-tags = {Dependent Types},
303−school = {University of Durham},
304−title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},
305−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf},
306−year = {2005}
307}
498}
308−@inproceedings{Brady2011a,
499+@inproceedings{Augustsson1998,
309−address = {New York, New York, USA},
500+abstract = {Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value , and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts. Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.},
310−author = {Brady, Edwin},
501+author = {Augustsson, Lennart},
311−booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},
502+booktitle = {International Conference on Functional Programming},
312−doi = {10.1145/1929529.1929536},
503+doi = {10.1097/MEG.0b013e328342f213},
313−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},
504+file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},
314−isbn = {9781450304870},
505+issn = {14735687},
315−keywords = {Dependent Types,data description,dependent types},
506+keywords = {Depe,Dependent Types},
316−mendeley-tags = {Dependent Types},
507+mendeley-tags = {Depe,Dependent Types},
317−month = jan,
508+number = {1},
509+pages = {239--250},
510+pmid = {21139473},
318publisher = {ACM Press},
511publisher = {ACM Press},
319−title = {{Idris --- Systems Programming Meets Full Dependent Types}},
512+title = {{Cayenne - a language with dependent types}},
320−url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
513+url = {http://www.cs.chalmers.se/$\sim$augustss/cayenne/paper.ps},
514+volume = {23},
321−year = {2011}
515+year = {1998}
322}
516}
323−@misc{dagand2011transporting,
517+@book{Hunt,
324−author = {Dagand, Pierre-Evariste and McBride, Conor},
518+author = {Hunt, Andrew and Thomas, David},
325−file = {:home/edwin/Research/Papers/Mendeley/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
519+booktitle = {Design},
326−title = {{Transporting Functions across Ornaments}},
520+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
327−url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},
521+isbn = {020161622X},
328−year = {2011}
522+title = {{The Pragmatic Programmer Chapter 4}}
329}
523}
330−@inproceedings{taha2004gentle,
524+@article{burrows1990,
331−author = {Taha, W.},
525+author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
332−booktitle = {Domain-Specific Program Generation},
526+file = {:Users/edwin/Documents/Mendeley Desktop/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},
527+journal = {ACM Transactions on Computer Systems},
333−pages = {30--50},
528+pages = {18----36},
334−publisher = {Springer},
529+title = {{A logic of authentication}},
335−title = {{A gentle introduction to multi-stage programming}},
530+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569},
336−url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},
531+volume = {8},
337−year = {2004}
532+year = {1990}
338}
533}
339−@inproceedings{augustsson2008paradise,
534+@inproceedings{atkey2009unembedding,
340−author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
535+author = {Atkey, R. and Lindley, S. and Yallop, J.},
341−booktitle = {International Conference on Functional Programming},
536+booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
342−file = {:home/edwin/Research/Papers/Mendeley/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},
343−number = {9},
344−pages = {225--228},
537+pages = {37--48},
345publisher = {ACM},
538publisher = {ACM},
346−title = {{Paradise: a two-stage DSL embedded in Haskell}},
539+title = {{Unembedding domain-specific languages}},
347−url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},
540+url = {http://dl.acm.org/citation.cfm?id=1596644},
348−volume = {43},
349−year = {2008}
541+year = {2009}
350−}
351−@misc{altenkirch2005dependent,
352−author = {Altenkirch, T. and McBride, C. and McKinna, J.},
353−booktitle = {Manuscript, available online},
354−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
355−title = {{Why dependent types matter}},
356−url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},
357−year = {2005}
358}
542}
359−@article{Xi1998,
543+@inproceedings{Brady2011a,
360−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.},
544+address = {New York, New York, USA},
361−author = {Xi, Hongwei and Pfenning, Frank},
545+author = {Brady, Edwin},
546+booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},
362−doi = {10.1145/277652.277732},
547+doi = {10.1145/1929529.1929536},
363−file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},
548+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},
364−isbn = {0897919874},
549+isbn = {9781450304870},
365−issn = {03621340},
366−journal = {ACM Sigplan Notices},
367−keywords = {Dependent Types},
550+keywords = {Dependent Types,data description,dependent types},
368mendeley-tags = {Dependent Types},
551mendeley-tags = {Dependent Types},
369−number = {5},
552+month = jan,
370−pages = {249--257},
371−publisher = {ACM},
553+publisher = {ACM Press},
372−series = {PLDI '98},
554+title = {{Idris --- Systems Programming Meets Full Dependent Types}},
373−title = {{Eliminating array bound checking through dependent types}},
374−url = {http://portal.acm.org/citation.cfm?doid=277652.277732},
555+url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
375−volume = {33},
376−year = {1998}
377−}
378−@inproceedings{augustsson1999exercise,
379−author = {Augustsson, L. and Carlsson, M.},
380−booktitle = {In Workshop on Dependent Types in Programming, Gothenburg},
381−keywords = {Depe},
382−mendeley-tags = {Depe},
383−publisher = {Citeseer},
384−title = {{An exercise in dependent types: A well-typed interpreter}},
385−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2895},
386−year = {1999}
387−}
388−@article{Swierstra2011,
389−author = {Swierstra, W},
390−file = {:home/edwin/Research/Papers/Mendeley/Swierstra/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},
391−journal = {Journal of Functional Programming},
392−number = {6},
393−pages = {575----583},
394−title = {{Sorted: Verifying the Problem of the {Dutch National} Flag in {Agda}}},
395−url = {http://journals.cambridge.org/abstract_S0956796811000207},
396−volume = {21},
397year = {2011}
556year = {2011}
398}
557}
399−@inproceedings{norell2009dependently,
558+@inproceedings{gibbons2011modularising,
400−author = {Norell, Ulf},
559+author = {Gibbons, J. and Ko, H.S. and Others},
401−booktitle = {Advanced Functional Programming},
560+file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
402−file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},
561+title = {{Modularising inductive families}},
403−keywords = {Dependent Types},
562+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
404−mendeley-tags = {Dependent Types},
405−pages = {230--266},
406−publisher = {Springer},
407−title = {{Dependently typed programming in Agda}},
408−url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},
409−year = {2009}
410−}
411−@article{Mandelbaum2007,
412−abstract = {Massive amounts of useful data are stored and processed in ad hoc formats for which common tools like parsers, printers, query engines and format converters are not readily available. In this paper, we explain the design and implementation of PADS/ML , a new language and system that facilitates the generation of data processing tools for ad hoc formats. The PADS/ML design includes features such as dependent, polymorphic and recursive datatypes, which allow programmers to describe the syntax and semantics of ad hoc data in a concise, easy-to-read notation. The PADS/ML implementation compiles these descriptions into ml structures and functors that include types for parsed data, functions for parsing and printing, and auxiliary support for user-specified, format-dependent and format-independent tool generation.},
413−author = {Mandelbaum, Yitzhak and Fisher, Kathleen and Walker, David and Fernandez, Mary and Gleyzer, Artem},
414−doi = {10.1145/1190215.1190231},
415−isbn = {1595935754},
416−issn = {03621340},
417−journal = {SIGPLAN Not},
418−number = {1},
419−pages = {77--83},
420−publisher = {ACM},
421−series = {POPL '07},
422−title = {{PADS/ML: a functional data description language}},
423−url = {http://doi.acm.org/10.1145/1190216.1190231},
424−volume = {42},
425−year = {2007}
563+year = {2011}
426}
564}
427−@misc{Abadi1997,
565+@book{An2012,
428−author = {Abadi, Martin and Gordon, Andrew D},
566+author = {Fowler, Martin},
429−booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},
567+booktitle = {Carcinogenesis},
430−file = {:home/edwin/Research/Papers/Mendeley/Abadi, Gordon/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},
568+doi = {10.1093/carcin/bgs054},
431−pages = {36 -- 47},
569+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
432−title = {{A calculus for cryptographic protocols: The spi calculus}},
570+isbn = {9780132107549},
433−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},
571+issn = {1460-2180},
434−year = {1997}
572+number = {3},
573+pmid = {22383472},
574+title = {{Domain Specific Languages Chapter 1}},
575+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
576+volume = {33}
435}
577}
436−@article{Jones1999,
578+@inproceedings{coquand1986analysis,
437−abstract = {Haskell benefits from a sophisticated type system, but implementors, programmers, and researchers suffer because it has no formal description. To remedy this shortcoming, we present a Haskell program that implements a Haskell typechecker, thus providing a mathematically rigorous specification in a notation that is familiar to Haskell users. We expect this program to fill a serious gap in current descriptions of Haskell, both as a starting point for discussions about existing features of the type system, and as a platform from which to explore new proposals.},
438−author = {Jones, Mark P},
579+author = {Coquand, T.},
439−journal = {October},
580+booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},
440−publisher = {Citeseer},
581+file = {:Users/edwin/Documents/Mendeley Desktop/Coquand/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},
441−title = {{Typing Haskell in Haskell}},
582+pages = {227----246},
442−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
583+title = {{An analysis of Girard's paradox}},
584+url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},
443−year = {1999}
585+year = {1986}
444}
586}
445−@article{Altenkirch2010,
587+@misc{altenkirch2008nσ,
446−abstract = {The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high-level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the languages. However, these features complicate the metatheoretical study and are a potential source of bugs. To address these issues we introduce $\Pi$$\Sigma$, a dependently typed core language. It is small enough for metatheoretical study and the type checker is small enough to be formally verified. In this language there is only one mechanism for recursionused for types, functions and infinite objectsand an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of $\alpha$-equality for recursive definitions. We show, by translating several high-level constructions, that $\Pi$$\Sigma$ is suitable as a core language for dependently typed programming.},
447−author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L, Andres and Oury, Nicolas},
588+author = {Altenkirch, T. and Oury, N.},
448−doi = {10.1007/978-3-642-12251-4_5},
589+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
449−editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
590+title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},
450−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
591+url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},
451−isbn = {9783642122507},
452−journal = {Computing},
453−number = {Sheard 2005},
454−pages = {40--55},
455−publisher = {Springer Berlin Heidelberg},
456−series = {Lecture Notes in Computer Science},
457−title = {{Dependent Types without the Sugar}},
458−url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
459−volume = {6009},
460−year = {2010}
592+year = {2008}
461}
593}
462−@book{Bertot2004,
594+@inproceedings{barras2008implicit,
463−author = {Bertot, Yves and Cast\'{e}ran, Pierre},
595+author = {Barras, B. and Bernardo, B.},
596+booktitle = {Foundations of Software Science and Computational Structures},
597+file = {:Users/edwin/Documents/Mendeley Desktop/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},
598+pages = {365--379},
464publisher = {Springer},
599publisher = {Springer},
465−title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},
600+title = {{The implicit calculus of constructions as a programming language with dependent types}},
466−url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},
601+url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
467−year = {2004}
602+year = {2008}
468}
603}
469−@book{The2012,
604+@book{While2012,
470author = {Hunt, Andrew and Thomas, David},
605author = {Hunt, Andrew and Thomas, David},
471booktitle = {Carcinogenesis},
606booktitle = {Carcinogenesis},
472doi = {10.1093/carcin/bgs054},
607doi = {10.1093/carcin/bgs054},
473−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
608+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
474isbn = {020161622X},
609isbn = {020161622X},
475issn = {1460-2180},
610issn = {1460-2180},
476number = {3},
611number = {3},
477pmid = {22383472},
612pmid = {22383472},
478−title = {{The Pragmatic Programmer Chapter 3}},
613+title = {{The Pragmatic Programmer Chapter 6}},
479url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
614url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
480volume = {33}
615volume = {33}
481}
616}
482−@inproceedings{ko2011modularising,
617+@inproceedings{bradyresource,
483−author = {Ko, H.S. and Gibbons, J.},
618+author = {Brady, Edwin and Hammond, Kevin},
484−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
619+booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},
485−pages = {13--24},
620+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},
486−publisher = {ACM},
621+pages = {242----257},
487−title = {{Modularising inductive families}},
622+title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},
488−url = {http://dl.acm.org/citation.cfm?id=2036921},
623+url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},
489−year = {2011}
490−}
491−@article{danielsson2011parsing,
492−author = {Danielsson, N. and Norell, U.},
493−journal = {Implementation and Application of Functional Languages},
494−pages = {80--99},
495−publisher = {Springer},
496−title = {{Parsing mixfix operators}},
497−url = {http://www.springerlink.com/index/386243257W504252.pdf},
498−year = {2011}
499−}
500−@misc{Bove2008,
501−abstract = {In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is based on ideas in Martin-L\"{o}f type theory and Martin-L\"{o}fs logical framework. We begin by showing how to do simply typed functional programming, and discuss the differences between Agdas type system and the Hindley-Milner type system, which underlies mainstream typed functional programming languages like Haskell and ML. We then show how to employ dependent types for programming with functional data structures such as vectors and binary search trees. We go on to explain the Curry-Howard identification of propositions and types, and how it makes Agda not only a programming language but also a programming logic. According to Curry-Howard, we also identify programs and proofs, something which is possible only by requiring that all program terminate. However, we show in the final section a method for encoding general and possibly partial recursive functions as total functions using dependent types.},
502−author = {Bove, Ana and Dybjer, Peter},
503−booktitle = {Notes},
504−doi = {10.1007/978-3-642-03153-3_2},
505−file = {:home/edwin/Research/Papers/Mendeley/Bove, Dybjer/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},
506−number = {February},
507−pages = {57--99},
508−publisher = {Springer},
509−title = {{Dependent Types at Work}},
510−url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},
511−volume = {5520},
512−year = {2008}
624+year = {2012}
513}
625}
514@book{luo1994,
626@book{luo1994,
515author = {Luo, Z.},
627author = {Luo, Z.},
@@ -518,133 +630,148 @@ title = {{Computation and reasoning: a type theory for computer science}},
518url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},
630url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},
519year = {1994}
631year = {1994}
520}
632}
521−@misc{idristutorial,
633+@phdthesis{norell2007thesis,
522−author = {Brady, Edwin},
634+author = {Norell, Ulf},
523−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
635+file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
524−title = {{Programming in Idris : a tutorial}},
636+keywords = {Dependent Types},
525−url = {http://idris-lang.org/tutorial},
637+mendeley-tags = {Dependent Types},
526−year = {2012}
527−}
528−@inproceedings{madhavapeddy2007melange,
529−author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
530−booktitle = {ACM SIGOPS Operating Systems Review},
531−file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},
532−number = {3},
533−pages = {101--114},
534−publisher = {ACM},
638+publisher = {Citeseer},
535−title = {{Melange: creating a functional internet}},
639+school = {Chalmers University of Technology},
536−url = {http://dl.acm.org/citation.cfm?id=1273009},
640+title = {{Towards a practical programming language based on dependent type theory}},
537−volume = {41},
641+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
538year = {2007}
642year = {2007}
539}
643}
540−@inproceedings{Augustsson1998,
644+@inproceedings{Brady2006b,
541−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.},
542−author = {Augustsson, Lennart},
543−booktitle = {International Conference on Functional Programming},
544−doi = {10.1097/MEG.0b013e328342f213},
545−file = {:home/edwin/Research/Papers/Mendeley/Augustsson/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},
546−issn = {14735687},
547−keywords = {Depe,Dependent Types},
548−mendeley-tags = {Depe,Dependent Types},
549−number = {1},
550−pages = {239--250},
551−pmid = {21139473},
552−publisher = {ACM Press},
553−title = {{Cayenne - a language with dependent types}},
554−url = {http://www.cs.chalmers.se/$\sim$augustss/cayenne/paper.ps},
555−volume = {23},
556−year = {1998}
557−}
558−@inproceedings{brady2011epic,
559author = {Brady, Edwin},
645author = {Brady, Edwin},
560−booktitle = {Trends in Functional Programming ({TFP}’11)},
646+booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},
561−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},
647+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
562−title = {{Epic --- A Library for Generating Compilers}},
648+isbn = {978-3-540-74129-9},
563−url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},
649+month = sep,
564−year = {2011}
650+pages = {145----162},
565−}
651+title = {{Ivor, a proof engine}},
566−@article{Epstein2011,
652+url = {http://dl.acm.org/citation.cfm?id=1757028.1757037},
567−author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},
568−institution = {Microsoft Research},
569−journal = {researchmicrosoftcom},
570−number = {Section 8},
571−pages = {1--12},
572−title = {{Haskell for the cloud}},
573−url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf},
574−year = {2011}
653+year = {2006}
575−}
576−@book{Hunt,
577−author = {Hunt, Andrew and Thomas, David},
578−booktitle = {Design},
579−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
580−isbn = {020161622X},
581−title = {{The Pragmatic Programmer Chapter 4}}
582}
654}
583−@inproceedings{swierstra2007beauty,
655+@inproceedings{chlipala2010ur,
584−author = {Swierstra, W. and Altenkirch, T.},
656+author = {Chlipala, Adam},
585−booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
657+booktitle = {ACM SIGPLAN Notices},
586−file = {:home/edwin/Research/Papers/Mendeley/Swierstra, Altenkirch/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},
658+file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
659+number = {6},
587−pages = {25--36},
660+pages = {122--133},
588publisher = {ACM},
661publisher = {ACM},
589−title = {{Beauty in the beast}},
662+title = {{Ur: statically-typed metaprogramming with type-level record computation}},
590−url = {http://dl.acm.org/citation.cfm?id=1291206},
663+url = {http://dl.acm.org/citation.cfm?id=1806612},
664+volume = {45},
591−year = {2007}
665+year = {2010}
592}
666}
593−@inproceedings{bradyresource,
667+@misc{Abadi1997,
594−author = {Brady, Edwin and Hammond, Kevin},
668+author = {Abadi, Martin and Gordon, Andrew D},
595−booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},
669+booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},
596−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},
670+file = {:Users/edwin/Documents/Mendeley Desktop/Abadi, Gordon/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},
597−pages = {242----257},
671+pages = {36 -- 47},
598−title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},
672+title = {{A calculus for cryptographic protocols: The spi calculus}},
599−url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},
673+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},
600−year = {2012}
674+year = {1997}
601}
675}
602−@article{fisher2006next,
676+@article{Jones2003,
603−author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},
677+abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},
604−file = {:home/edwin/Research/Papers/Mendeley/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},
678+author = {Jones, Simon Peyton},
605−journal = {Journal of the ACM},
679+editor = {Jones, Simon Peyton},
680+isbn = {0521826144},
681+journal = {Language},
606−number = {2},
682+number = {1},
607−pages = {1--51},
608−publisher = {ACM},
683+publisher = {Cambridge University Press},
609−title = {{The next 700 data description languages}},
684+title = {{Haskell 98 Language and Libraries The Revised Report}},
610−url = {http://dl.acm.org/citation.cfm?id=1111039},
685+url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},
611−volume = {15},
686+volume = {13},
612−year = {2010}
687+year = {2003}
613}
688}
614−@book{Bird2010,
689+@inproceedings{Visser2008,
615−author = {Bird, Richard},
690+author = {Visser, E},
616−file = {:home/edwin/Research/Papers/Mendeley/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
691+booktitle = {Generative and Transformational Techniques in Software Engineering},
617−isbn = {9780521513388},
692+title = {{WebDSL: A case study in domain-specific language engineering}},
618−title = {{Pearls of Functional Algorithm Design}},
693+url = {http://www.springerlink.com/index/A3213003X6268032.pdf},
619−year = {2010}
694+year = {2008}
620}
695}
621−@inproceedings{stump2010resource,
696+@inproceedings{ko2011modularising,
622−author = {Stump, A. and Austin, E.},
697+author = {Ko, H.S. and Gibbons, J.},
623−booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},
698+booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
624−file = {:home/edwin/Research/Papers/Mendeley/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},
625−pages = {27--38},
699+pages = {13--24},
626publisher = {ACM},
700publisher = {ACM},
627−title = {{Resource typing in Guru}},
701+title = {{Modularising inductive families}},
628−url = {http://dl.acm.org/citation.cfm?id=1707796},
702+url = {http://dl.acm.org/citation.cfm?id=2036921},
629−year = {2010}
703+year = {2011}
630}
704}
705+@misc{Attacks2012a,
706+author = {Anderson, Ross},
707+doi = {10.1093/epirev/mxr031},
708+file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},
709+isbn = {9780470068526},
710+issn = {1478-6729},
711+number = {1},
712+pages = {NP},
713+pmid = {22215642},
714+title = {{Security Engineering Chapter 18}},
715+volume = {34}
716+}
631−@inproceedings{taha1997multi,
717+@inproceedings{l,
632−author = {Taha, W. and Sheard, T.},
718+author = {L\"{a}mmel, R. and Jones, S.P.},
633booktitle = {ACM SIGPLAN Notices},
719booktitle = {ACM SIGPLAN Notices},
720+file = {:Users/edwin/Documents/Mendeley Desktop/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},
634−number = {12},
721+number = {3},
635−pages = {203--217},
722+pages = {26--37},
636publisher = {ACM},
723publisher = {ACM},
637−title = {{Multi-stage programming with explicit annotations}},
724+title = {{Scrap your boilerplate: a practical design pattern for generic programming}},
638−url = {http://dl.acm.org/citation.cfm?id=259019},
725+url = {http://dl.acm.org/citation.cfm?id=640136.604179},
639−volume = {32},
726+volume = {38},
727+year = {2003}
728+}
729+@misc{pollack1997believe,
730+author = {Pollack, R.},
731+file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
732+title = {{How to believe a machine-checked proof}},
733+url = {http://books.google.co.uk/books?hl=en&lr=&id=pLnKggT_In4C&oi=fnd&pg=PA205&dq=how+to+believe+a+machine+checked+proof&ots=c2OI8krqqA&sig=EF3QonGFVdOpYdKO1KmW6ljCkjY},
640year = {1997}
734year = {1997}
641}
735}
736+@book{Bertot2004,
737+author = {Bertot, Yves and Cast\'{e}ran, Pierre},
738+publisher = {Springer},
739+title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},
740+url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},
741+year = {2004}
742+}
743+@inproceedings{brady2011epic,
744+author = {Brady, Edwin},
745+booktitle = {Trends in Functional Programming ({TFP}’11)},
746+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},
747+title = {{Epic --- A Library for Generating Compilers}},
748+url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},
749+year = {2011}
750+}
751+@article{dybjer1994inductive,
752+author = {Dybjer, P.},
753+journal = {Formal aspects of computing},
754+number = {4},
755+pages = {440--465},
756+publisher = {Springer},
757+title = {{Inductive families}},
758+url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
759+volume = {6},
760+year = {1994}
761+}
762+@inproceedings{McBride2004b,
763+author = {McBride, Conor and McKinna, James},
764+booktitle = {Haskell Workshop},
765+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},
766+title = {{I am not a number : I am a free variable}},
767+year = {2004}
768+}
642@article{Wadler2001,
769@article{Wadler2001,
643abstract = {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.},
770abstract = {The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.},
644author = {Wadler, Philip},
771author = {Wadler, Philip},
645doi = {10.1007/3-540-59451-5_2},
772doi = {10.1007/3-540-59451-5_2},
646editor = {Jeuring, Johan and Meijer, Erik},
773editor = {Jeuring, Johan and Meijer, Erik},
647−file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 2001 - Monads for functional programming.pdf:pdf},
774+file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 2001 - Monads for functional programming.pdf:pdf},
648isbn = {3540594515},
775isbn = {3540594515},
649issn = {03029743},
776issn = {03029743},
650journal = {Advanced Functional Programming},
777journal = {Advanced Functional Programming},
@@ -657,30 +784,34 @@ url = {http://www.springerlink.com/index/715264614rh13340.pdf},
657volume = {925},
784volume = {925},
658year = {2001}
785year = {2001}
659}
786}
660−@article{Hoare1978,
787+@inproceedings{taha1997multi,
661−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.},
788+author = {Taha, W. and Sheard, T.},
662−author = {Hoare, C A R},
789+booktitle = {ACM SIGPLAN Notices},
663−doi = {10.1016/0167-6423(87)90028-1},
664−editor = {McKeag, R M and Macnaghten, A M},
665−file = {:home/edwin/Research/Papers/Mendeley/Hoare/Hoare - 1978 - Communicating sequential processes.pdf:pdf},
666−isbn = {0131532715},
667−issn = {01676423},
668−journal = {Communications of the ACM},
669−number = {8},
790+number = {12},
670−pages = {666--677},
791+pages = {203--217},
671−pmid = {2142694823583477576},
672publisher = {ACM},
792publisher = {ACM},
673−series = {International Series in Computer Science},
793+title = {{Multi-stage programming with explicit annotations}},
674−title = {{Communicating sequential processes}},
794+url = {http://dl.acm.org/citation.cfm?id=259019},
675−url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},
795+volume = {32},
796+year = {1997}
797+}
798+@article{loh2010tutorial,
799+author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},
800+file = {:Users/edwin/Documents/Mendeley Desktop/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},
801+journal = {Fundamenta Informaticae},
802+number = {2},
803+pages = {177--207},
804+publisher = {IOS Press},
805+title = {{A tutorial implementation of a dependently typed lambda calculus}},
806+url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},
676−volume = {21},
807+volume = {102},
677−year = {1978}
808+year = {2010}
678}
809}
679@book{Philosophy2012,
810@book{Philosophy2012,
680author = {Hunt, Andrew and Thomas, David},
811author = {Hunt, Andrew and Thomas, David},
681booktitle = {Carcinogenesis},
812booktitle = {Carcinogenesis},
682doi = {10.1093/carcin/bgs054},
813doi = {10.1093/carcin/bgs054},
683−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
814+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
684isbn = {020161622X},
815isbn = {020161622X},
685issn = {1460-2180},
816issn = {1460-2180},
686number = {3},
817number = {3},
@@ -689,98 +820,41 @@ title = {{The Pragmatic Programmer Chapter 1}},
689url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
820url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
690volume = {33}
821volume = {33}
691}
822}
692−@book{While2012,
693−author = {Hunt, Andrew and Thomas, David},
694−booktitle = {Carcinogenesis},
695−doi = {10.1093/carcin/bgs054},
696−file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
697−isbn = {020161622X},
698−issn = {1460-2180},
699−number = {3},
700−pmid = {22383472},
701−title = {{The Pragmatic Programmer Chapter 6}},
702−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
703−volume = {33}
704−}
705−@inproceedings{Brady2010,
823+@inproceedings{pollack1990implicit,
706−author = {Brady, Edwin and Hammond, Kevin},
824+author = {Pollack, R.},
707−booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
825+booktitle = {Informal Proceedings of First Workshop on Logical Frameworks, Antibes},
708−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},
826+file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},
709−isbn = {9781605587943},
710−keywords = {Dependent Types,code generation gives,contrast,dependent types,efficient,harder,however,implementation,likely efficient,ness interpreter,partial evaluation,resulting implementation,un,verify its correctness},
711−mendeley-tags = {Dependent Types},
712−pages = {297--308},
713−publisher = {ACM},
827+publisher = {Citeseer},
714−title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},
828+title = {{Implicit syntax}},
715−url = {http://portal.acm.org/citation.cfm?id=1863587},
829+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
716−year = {2010}
830+year = {1990}
717}
831}
718−@inproceedings{Visser2008,
832+@article{gordon2003authenticity,
719−author = {Visser, E},
833+author = {Gordon, A.D. and Jeffrey, A.},
720−booktitle = {Generative and Transformational Techniques in Software Engineering},
834+file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},
721−title = {{WebDSL: A case study in domain-specific language engineering}},
835+journal = {Journal of computer security},
722−url = {http://www.springerlink.com/index/A3213003X6268032.pdf},
836+number = {4},
723−year = {2008}
724−}
725−@misc{TheMendeleySupportTeam2011a,
726−abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
727−address = {London},
728−author = {{The Mendeley Support Team}},
729−booktitle = {Mendeley Desktop},
730−file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
731−keywords = {Mendeley,how-to,user manual},
732−pages = {1--16},
837+pages = {451--520},
733−publisher = {Mendeley Ltd.},
838+publisher = {IOS Press},
734−title = {{Getting Started with Mendeley}},
839+title = {{Authenticity by typing for security protocols}},
735−url = {http://www.mendeley.com},
840+url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},
736−year = {2011}
841+volume = {11},
737−}
842+year = {2003}
738−@inproceedings{Brady2005a,
739−author = {Brady, E and Hammond, K},
740−booktitle = {Implementation and Application of Functional \ldots},
741−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},
742−keywords = {Dependent Types},
743−mendeley-tags = {Dependent Types},
744−title = {{A dependently typed framework for static analysis of program execution costs}},
745−url = {http://www.springerlink.com/index/P446P2HH70107759.pdf},
746−year = {2005}
747−}
748−@inproceedings{madhavapeddy2010turning,
749−author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
750−booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
751−file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},
752−publisher = {USENIX Association},
753−title = {{Turning down the LAMP: software specialisation for the cloud}},
754−url = {http://dl.acm.org/citation.cfm?id=1863114},
755−year = {2010}
756−}
757−@article{McBride2007,
758−author = {McBride, Conor and Paterson, Ross},
759−file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
760−journal = {Journal of functional programming},
761−title = {{Applicative programming with effects}},
762−url = {http://journals.cambridge.org/abstract_S0956796807006326},
763−year = {2007}
764}
843}
765−@inproceedings{bhargavan2010modular,
844+@inproceedings{Wadler1989,
766−author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},
845+abstract = {From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds' abstraction theorem for the polymorphic lambda calculus.},
767−booktitle = {ACM Sigplan Notices},
846+author = {Wadler, Philip},
847+booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
848+doi = {10.1145/99370.99404},
849+file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},
850+isbn = {0897913280},
768−number = {1},
851+number = {June},
769−pages = {445--456},
852+pages = {347--359},
770publisher = {ACM},
853publisher = {ACM},
771−title = {{Modular verification of security protocol code by typing}},
854+series = {FPCA '89},
855+title = {{Theorems for free!}},
772−url = {http://dl.acm.org/citation.cfm?id=1707801.1706350},
856+url = {http://portal.acm.org/citation.cfm?id=99404},
773−volume = {45},
774−year = {2010}
857+year = {1989}
775−}
776−@inproceedings{coquand1986analysis,
777−author = {Coquand, T.},
778−booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},
779−file = {:home/edwin/Research/Papers/Mendeley/Coquand/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},
780−pages = {227----246},
781−title = {{An analysis of Girard's paradox}},
782−url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},
783−year = {1986}
784}
858}
785@inproceedings{Augustsson1985,
859@inproceedings{Augustsson1985,
786address = {Berlin, Heidelberg},
860address = {Berlin, Heidelberg},
@@ -798,345 +872,183 @@ url = {http://www.springerlink.com/content/y647423656557505/},
798volume = {201},
872volume = {201},
799year = {1985}
873year = {1985}
800}
874}
801−@misc{Bloat,
802−author = {Brooks, Fred},
803−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},
804−isbn = {9780321702081},
805−title = {{The Design of Design Chapter 4}}
806−}
807−@inproceedings{barras2008implicit,
875+@inproceedings{Brady2005a,
808−author = {Barras, B. and Bernardo, B.},
876+author = {Brady, E and Hammond, K},
809−booktitle = {Foundations of Software Science and Computational Structures},
877+booktitle = {Implementation and Application of Functional \ldots},
810−file = {:home/edwin/Research/Papers/Mendeley/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},
878+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},
811−pages = {365--379},
879+keywords = {Dependent Types},
812−publisher = {Springer},
880+mendeley-tags = {Dependent Types},
813−title = {{The implicit calculus of constructions as a programming language with dependent types}},
881+title = {{A dependently typed framework for static analysis of program execution costs}},
814−url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
882+url = {http://www.springerlink.com/index/P446P2HH70107759.pdf},
815−year = {2008}
883+year = {2005}
816−}
817−@misc{Brady2012c,
818−author = {Brooks, Fred},
819−doi = {10.1093/epirev/mxr031},
820−file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},
821−isbn = {9780321702081},
822−issn = {1478-6729},
823−number = {1},
824−pages = {NP},
825−pmid = {22215642},
826−title = {{The Design of Design Chapter 5}},
827−volume = {34}
828−}
829−@inproceedings{Fournet2011,
830−author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},
831−booktitle = {Foundations of security analysis and design {VI}},
832−file = {:home/edwin/Research/Papers/Mendeley/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},
833−title = {{Cryptographic verification by typing for a sample protocol implementation}},
834−url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
835−year = {2010}
836−}
837−@book{Choosing2012,
838−author = {Fowler, Martin},
839−booktitle = {Carcinogenesis},
840−doi = {10.1093/carcin/bgs054},
841−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
842−isbn = {9780132107549},
843−issn = {1460-2180},
844−number = {3},
845−pmid = {22383472},
846−title = {{Domain Specific Languages Chapter 6}},
847−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
848−volume = {33}
849−}
850−@article{mcbride2008functional,
851−author = {McBride, C. and Paterson, R.},
852−file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
853−journal = {Journal of functional programming},
854−number = {1},
855−pages = {1--13},
856−publisher = {Cambridge Univ Press},
857−title = {{Functional pearl: Applicative programming with effects}},
858−url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=1457860},
859−volume = {18},
860−year = {2008}
861−}
862−@inproceedings{pollack1990implicit,
863−author = {Pollack, R.},
864−booktitle = {Informal Proceedings of First Workshop on Logical Frameworks, Antibes},
865−file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},
866−publisher = {Citeseer},
867−title = {{Implicit syntax}},
868−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
869−year = {1990}
870−}
871−@misc{altenkirch2008nσ,
872−author = {Altenkirch, T. and Oury, N.},
873−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
874−title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},
875−url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},
876−year = {2008}
877−}
878−@misc{Abel1998,
879−author = {Abel, Andreas},
880−booktitle = {Language},
881−file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
882−title = {{foetus - Termination Checker for Simple Functional Programs}},
883−year = {1998}
884}
884}
885−@misc{pollack1997believe,
885+@article{Vytiniotis2011,
886−author = {Pollack, R.},
886+author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},
887−file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
887+file = {:Users/edwin/Downloads/S0956796811000098a.pdf:pdf},
888−title = {{How to believe a machine-checked proof}},
888+journal = {{Journal of Functional Programming}},
889−url = {http://books.google.co.uk/books?hl=en&lr=&id=pLnKggT_In4C&oi=fnd&pg=PA205&dq=how+to+believe+a+machine+checked+proof&ots=c2OI8krqqA&sig=EF3QonGFVdOpYdKO1KmW6ljCkjY},
889+number = {4--5},
890+pages = {333----412},
891+title = {{\textsc{OutsideIn}(X) Modular type inference with local assumptions}},
892+url = {http://journals.cambridge.org/abstract_S0956796811000098},
893+volume = {21},
890−year = {1997}
894+year = {2011}
891}
895}
892−@inproceedings{atkey2009unembedding,
896+@article{mccann2000packet,
893−author = {Atkey, R. and Lindley, S. and Yallop, J.},
897+author = {McCann, P.J. and Chandra, S.},
894−booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
898+journal = {ACM SIGCOMM Computer Communication Review},
899+number = {4},
895−pages = {37--48},
900+pages = {321--333},
896publisher = {ACM},
901publisher = {ACM},
897−title = {{Unembedding domain-specific languages}},
902+title = {{Packet types: abstract specification of network protocol messages}},
898−url = {http://dl.acm.org/citation.cfm?id=1596644},
903+url = {http://dl.acm.org/citation.cfm?id=347563},
904+volume = {30},
899−year = {2009}
905+year = {2000}
900}
906}
907+@article{Miller1992,
908+author = {Miller, Dale},
909+file = {:Users/edwin/Documents/Papers/Miller/1992 Miller-Unification under a mixed prefix.pdf:pdf},
910+journal = {Journal of Symbolic Computation},
911+title = {{Unification under a mixed prefix}},
912+url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},
913+year = {1992}
914+}
901−@inproceedings{oury2008power,
915+@inproceedings{norell2009dependently,
902−author = {Oury, N. and Swierstra, W.},
916+author = {Norell, Ulf},
903−booktitle = {International Conference on Functional Programming},
917+booktitle = {Advanced Functional Programming},
904−file = {:home/edwin/Research/Papers/Mendeley/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
918+file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},
905keywords = {Dependent Types},
919keywords = {Dependent Types},
906mendeley-tags = {Dependent Types},
920mendeley-tags = {Dependent Types},
907−number = {9},
908−pages = {39--50},
921+pages = {230--266},
909−publisher = {ACM},
922+publisher = {Springer},
910−title = {{The power of Pi}},
923+title = {{Dependently typed programming in Agda}},
911−url = {http://dl.acm.org/citation.cfm?id=1411213},
924+url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},
912−volume = {43},
913−year = {2008}
925+year = {2009}
914}
926}
915−@article{loh2010tutorial,
927+@article{Hughes1989,
916−author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},
928+abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},
917−file = {:home/edwin/Research/Papers/Mendeley/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},
929+author = {Hughes, J},
918−journal = {Fundamenta Informaticae},
930+chapter = {2},
931+doi = {10.1093/comjnl/32.2.98},
932+editor = {Turner, David A},
933+file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
934+institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},
935+isbn = {0201172364},
936+issn = {00104620},
937+journal = {The Computer Journal},
919number = {2},
938number = {2},
920−pages = {177--207},
939+pages = {98--107},
921−publisher = {IOS Press},
940+publisher = {Br Computer Soc},
922−title = {{A tutorial implementation of a dependently typed lambda calculus}},
941+title = {{Why Functional Programming Matters}},
923−url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},
942+url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},
924−volume = {102},
943+volume = {32},
925−year = {2010}
944+year = {1989}
926−}
927−@article{gordon2003authenticity,
928−author = {Gordon, A.D. and Jeffrey, A.},
929−file = {:home/edwin/Research/Papers/Mendeley/Gordon, Jeffrey/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},
930−journal = {Journal of computer security},
931−number = {4},
932−pages = {451--520},
933−publisher = {IOS Press},
934−title = {{Authenticity by typing for security protocols}},
935−url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},
936−volume = {11},
937−year = {2003}
938−}
939−@misc{Attacks2012a,
940−author = {Anderson, Ross},
941−doi = {10.1093/epirev/mxr031},
942−file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},
943−isbn = {9780470068526},
944−issn = {1478-6729},
945−number = {1},
946−pages = {NP},
947−pmid = {22215642},
948−title = {{Security Engineering Chapter 18}},
949−volume = {34}
950}
945}
951−@inproceedings{Sheard2005,
946+@article{Steiner1988,
952−address = {New York, New York, USA},
953−author = {Sheard, Tim},
947+author = {Steiner, JG},
954−booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},
948+file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
955−doi = {10.1145/1088348.1088356},
949+journal = {Proc. Winter USENIX Conference},
956−file = {:home/edwin/Research/Papers/Mendeley/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},
950+title = {{Kerberos: An authentication service for open network systems}},
957−isbn = {159593071X},
951+url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},
958−keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},
959−month = sep,
960−pages = {74--85},
961−publisher = {ACM Press},
962−title = {{Putting curry-howard to work}},
963−url = {http://dl.acm.org/citation.cfm?id=1088348.1088356},
964−year = {2005}
952+year = {1988}
965}
953}
966−@inproceedings{NanevskiAAMorrisett2008,
954+@phdthesis{McBride1999,
967−abstract = {We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions. The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which, abstracts the implementation details and ensures that the modules properly implement the finite map abstraction. Copyright 2008 ACM.},
955+author = {McBride, Conor},
968−author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},
956+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
969−booktitle = {International Conference on Functional Programming},
970−doi = {10.1145/1411204.1411237},
971−file = {:home/edwin/Research/Papers/Mendeley/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},
972−isbn = {9781595939197},
973−issn = {15232867},
974keywords = {Dependent Types},
957keywords = {Dependent Types},
975mendeley-tags = {Dependent Types},
958mendeley-tags = {Dependent Types},
976−number = {9},
959+school = {University of Edinburgh},
977−pages = {229--240},
960+title = {{Dependently typed functional programs and their proofs}},
978−title = {{Ynot: Dependent types for imperative programs}},
961+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
979−url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},
980−volume = {43},
981−year = {2008}
962+year = {1999}
982}
963}
983−@inproceedings{fisher2005pads,
964+@inproceedings{augustsson1999exercise,
984−author = {Fisher, K. and Gruber, R.},
965+author = {Augustsson, L. and Carlsson, M.},
985−booktitle = {ACM SIGPLAN Notices},
966+booktitle = {In Workshop on Dependent Types in Programming, Gothenburg},
986−number = {6},
967+keywords = {Depe},
987−pages = {295--304},
968+mendeley-tags = {Depe},
988−publisher = {ACM},
969+publisher = {Citeseer},
989−title = {{PADS: a domain-specific language for processing ad hoc data}},
970+title = {{An exercise in dependent types: A well-typed interpreter}},
990−url = {http://dl.acm.org/citation.cfm?id=1065046},
971+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2895},
991−volume = {40},
992−year = {2005}
972+year = {1999}
993}
973}
994−@inproceedings{McBride2004b,
974+@inproceedings{taha2004gentle,
995−author = {McBride, Conor and McKinna, James},
975+author = {Taha, W.},
996−booktitle = {Haskell Workshop},
976+booktitle = {Domain-Specific Program Generation},
997−file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},
977+pages = {30--50},
998−title = {{I am not a number : I am a free variable}},
978+publisher = {Springer},
979+title = {{A gentle introduction to multi-stage programming}},
980+url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},
999year = {2004}
981year = {2004}
1000}
982}
1001−@article{marlow2006making,
1002−author = {Marlow, S. and {Peyton Jones}, S.},
1003−file = {:home/edwin/Research/Papers/Mendeley/Marlow, Peyton Jones/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},
1004−journal = {Journal of Functional Programming},
1005−number = {4-5},
1006−pages = {415--449},
1007−publisher = {Cambridge University Press},
1008−title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}},
1009−url = {http://dl.acm.org/citation.cfm?id=1166018},
1010−volume = {16},
1011−year = {2006}
1012−}
1013−@article{landin1966next,
1014−author = {Landin, P.J.},
1015−file = {:home/edwin/Research/Papers/Mendeley/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
1016−journal = {Communications of the ACM},
1017−number = {3},
1018−pages = {157--166},
1019−publisher = {ACM},
1020−title = {{The next 700 programming languages}},
1021−url = {http://dl.acm.org/citation.cfm?id=365257 )},
1022−volume = {9},
1023−year = {1966}
1024−}
1025−@misc{Protocols2012a,
1026−author = {Anderson, Ross},
1027−doi = {10.1093/epirev/mxr031},
1028−file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
1029−isbn = {9780470068526},
1030−issn = {1478-6729},
1031−pmid = {22215642},
1032−title = {{Security Engineering Chapter 3}}
1033−}
1034@inproceedings{Sculthorpe2009,
983@inproceedings{Sculthorpe2009,
1035author = {Sculthorpe, Neil and Nilsson, Henrik},
984author = {Sculthorpe, Neil and Nilsson, Henrik},
1036booktitle = {International Conference on Functional Programming ({ICFP} '09)},
985booktitle = {International Conference on Functional Programming ({ICFP} '09)},
1037−file = {:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf;:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf},
986+file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},
1038title = {{Safe functional reactive programming through dependent types}},
987title = {{Safe functional reactive programming through dependent types}},
1039url = {http://dl.acm.org/citation.cfm?id=1596558},
988url = {http://dl.acm.org/citation.cfm?id=1596558},
1040year = {2009}
989year = {2009}
1041}
990}
991+@misc{TheMendeleySupportTeam2011a,
992+abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
993+address = {London},
994+author = {{The Mendeley Support Team}},
995+booktitle = {Mendeley Desktop},
996+file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
997+keywords = {Mendeley,how-to,user manual},
998+pages = {1--16},
999+publisher = {Mendeley Ltd.},
1000+title = {{Getting Started with Mendeley}},
1001+url = {http://www.mendeley.com},
1002+year = {2011}
1003+}
1004+@article{danielsson2011parsing,
1005+author = {Danielsson, N. and Norell, U.},
1006+journal = {Implementation and Application of Functional Languages},
1007+pages = {80--99},
1008+publisher = {Springer},
1009+title = {{Parsing mixfix operators}},
1010+url = {http://www.springerlink.com/index/386243257W504252.pdf},
1011+year = {2011}
1012+}
1013+@misc{dagand2011transporting,
1014+author = {Dagand, Pierre-Evariste and McBride, Conor},
1015+file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
1016+title = {{Transporting Functions across Ornaments}},
1017+url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},
1018+year = {2011}
1019+}
1042@book{Fowler,
1020@book{Fowler,
1043author = {Fowler, Martin},
1021author = {Fowler, Martin},
1044booktitle = {Language},
1022booktitle = {Language},
1045−file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
1023+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
1046isbn = {9780132107549},
1024isbn = {9780132107549},
1047title = {{Domain Specific Languages Chapter 2}}
1025title = {{Domain Specific Languages Chapter 2}}
1048}
1026}
1049−@article{Jones2003,
1027+@misc{Bove2008,
1050−abstract = {Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support Haskell 98, so professioanls and educators have a stable base for their work.},
1028+abstract = {In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is based on ideas in Martin-L\"{o}f type theory and Martin-L\"{o}fs logical framework. We begin by showing how to do simply typed functional programming, and discuss the differences between Agdas type system and the Hindley-Milner type system, which underlies mainstream typed functional programming languages like Haskell and ML. We then show how to employ dependent types for programming with functional data structures such as vectors and binary search trees. We go on to explain the Curry-Howard identification of propositions and types, and how it makes Agda not only a programming language but also a programming logic. According to Curry-Howard, we also identify programs and proofs, something which is possible only by requiring that all program terminate. However, we show in the final section a method for encoding general and possibly partial recursive functions as total functions using dependent types.},
1051−author = {Jones, Simon Peyton},
1029+author = {Bove, Ana and Dybjer, Peter},
1052−editor = {Jones, Simon Peyton},
1030+booktitle = {Notes},
1053−isbn = {0521826144},
1031+doi = {10.1007/978-3-642-03153-3_2},
1054−journal = {Language},
1032+file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},
1055−number = {1},
1033+number = {February},
1056−publisher = {Cambridge University Press},
1057−title = {{Haskell 98 Language and Libraries The Revised Report}},
1058−url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},
1059−volume = {13},
1060−year = {2003}
1061−}
1062−@article{Brady2006a,
1063−author = {Brady, E and Hammond, K},
1064−file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},
1065−journal = {\ldots of the 5th international conference on \ldots},
1066−keywords = {Dependent Types},
1067−mendeley-tags = {Dependent Types},
1068−title = {{A verified staged interpreter is a verified compiler}},
1069−url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},
1070−year = {2006}
1071−}
1072−@article{burrows1990,
1073−author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
1074−file = {:home/edwin/Research/Papers/Mendeley/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},
1075−journal = {ACM Transactions on Computer Systems},
1076−pages = {18----36},
1034+pages = {57--99},
1077−title = {{A logic of authentication}},
1078−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569},
1079−volume = {8},
1080−year = {1990}
1081−}
1082−@phdthesis{McBride1999,
1083−author = {McBride, Conor},
1084−file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
1085−keywords = {Dependent Types},
1086−mendeley-tags = {Dependent Types},
1087−school = {University of Edinburgh},
1088−title = {{Dependently typed functional programs and their proofs}},
1089−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
1090−year = {1999}
1091−}
1092−@article{mcbride2010ornamental,
1093−author = {McBride, Conor},
1094−file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
1095−journal = {Journal of Functional Programming},
1096−title = {{Ornamental algebras, algebraic ornaments}},
1097−url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},
1098−year = {2010}
1099−}
1100−@inproceedings{czarnecki2004dsl,
1101−author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},
1102−booktitle = {Domain-Specific Program Generation},
1103−file = {:home/edwin/Research/Papers/Mendeley/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},
1104−pages = {51--72},
1105−publisher = {Springer},
1035+publisher = {Springer},
1106−title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},
1036+title = {{Dependent Types at Work}},
1107−url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},
1037+url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},
1108−year = {2004}
1038+volume = {5520},
1109−}
1110−@article{Chapman2005epigram,
1111−author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},
1112−file = {:home/edwin/Research/Papers/Mendeley/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},
1113−journal = {Trends in Functional Programming},
1114−publisher = {Intellect Books},
1115−title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
1116−url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
1117−year = {2005}
1039+year = {2008}
1118}
1040}
1119−@inproceedings{Levitation2010,
1041+@article{Okasaki1993,
1120−author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},
1042+author = {Okasaki, Chris},
1121−booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},
1043+file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
1122−doi = {10.1145/1932681.1863547},
1044+journal = {Journal of functional programming},
1123−file = {:home/edwin/Research/Papers/Mendeley/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},
1045+title = {{Red-Black Trees in A Functional Setting}},
1124−isbn = {978-1-60558-794-3},
1125−issn = {03621340},
1126−keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},
1127−mendeley-tags = {Dependent Types},
1128−month = sep,
1129−number = {9},
1130−pages = {3},
1131−title = {{The gentle art of levitation}},
1132−url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},
1133−volume = {45},
1134−year = {2010}
1046+year = {1993}
1135}
1047}
1136@inproceedings{pj2006gadts,
1048@inproceedings{pj2006gadts,
1137author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
1049author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
1138booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
1050booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
1139−file = {:home/edwin/Research/Papers/Mendeley/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
1051+file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
1140number = {9},
1052number = {9},
1141pages = {50--61},
1053pages = {50--61},
1142publisher = {ACM},
1054publisher = {ACM},
@@ -1145,11 +1057,56 @@ url = {http://dl.acm.org/citation.cfm?id=1159811},
1145volume = {41},
1057volume = {41},
1146year = {2006}
1058year = {2006}
1147}
1059}
1060+@misc{altenkirch2005dependent,
1061+author = {Altenkirch, T. and McBride, C. and McKinna, J.},
1062+booktitle = {Manuscript, available online},
1063+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
1064+title = {{Why dependent types matter}},
1065+url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},
1066+year = {2005}
1067+}
1068+@misc{The2012c,
1069+author = {Robbins, A and Hannah, E and Lamb, L},
1070+doi = {10.1093/epirev/mxr031},
1071+file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
1072+isbn = {9780596529833},
1073+issn = {1478-6729},
1074+pmid = {22215642},
1075+title = {{Learning the vi and Vim Editors}}
1076+}
1077+@misc{Resolution2012a,
1078+author = {Fall, Kevin R and Stevens, W. Richard},
1079+doi = {10.1093/epirev/mxr031},
1080+file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},
1081+issn = {1478-6729},
1082+pmid = {22215642},
1083+title = {{TCP/IP Illustrated Volume 1 Chapter 11}}
1084+}
1085+@article{Brady2006a,
1086+author = {Brady, E and Hammond, K},
1087+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},
1088+journal = {\ldots of the 5th international conference on \ldots},
1089+keywords = {Dependent Types},
1090+mendeley-tags = {Dependent Types},
1091+title = {{A verified staged interpreter is a verified compiler}},
1092+url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},
1093+year = {2006}
1094+}
1095+@inproceedings{swierstra2007beauty,
1096+author = {Swierstra, W. and Altenkirch, T.},
1097+booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
1098+file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra, Altenkirch/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},
1099+pages = {25--36},
1100+publisher = {ACM},
1101+title = {{Beauty in the beast}},
1102+url = {http://dl.acm.org/citation.cfm?id=1291206},
1103+year = {2007}
1104+}
1148@article{McBride2004a,
1105@article{McBride2004a,
1149abstract = {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.},
1106abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.},
1150author = {McBride, Conor and McKinna, James},
1107author = {McBride, Conor and McKinna, James},
1151doi = {10.1017/S0956796803004829},
1108doi = {10.1017/S0956796803004829},
1152−file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
1109+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
1153issn = {09567968},
1110issn = {09567968},
1154journal = {Journal of Functional Programming},
1111journal = {Journal of Functional Programming},
1155keywords = {Dependent Types},
1112keywords = {Dependent Types},
@@ -1162,80 +1119,153 @@ url = {http://www.journals.cambridge.org/abstract_S0956796803004829},
1162volume = {14},
1119volume = {14},
1163year = {2004}
1120year = {2004}
1164}
1121}
1165−@article{Altenkirch2010a,
1122+@misc{Nodes2012a,
1166−abstract = {We begin by revisiting the idea of using a universe of types to write generic programs in a dependently typed setting by constructing a universe for Strictly Positive Types (SPTs). Here we extend this construction to cover dependent types, i.e. Strictly Positive Families (SPFs), thereby fixing a gap left open in previous work. Using the approach presented here we are able to represent all of Epigrams datatypes within Epigram including the universe of datatypes itself.},
1123+author = {Brooks, Fred},
1167−author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},
1124+doi = {10.1093/epirev/mxr031},
1168−file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
1125+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
1126+isbn = {9780321702081},
1127+issn = {1478-6729},
1128+pmid = {22215642},
1129+title = {{The Design of Design Chapter 3}}
1130+}
1131+@inproceedings{augustsson2008paradise,
1132+author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
1133+booktitle = {International Conference on Functional Programming},
1134+file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},
1135+number = {9},
1136+pages = {225--228},
1137+publisher = {ACM},
1138+title = {{Paradise: a two-stage DSL embedded in Haskell}},
1139+url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},
1140+volume = {43},
1141+year = {2008}
1142+}
1143+@misc{Abel1998,
1144+author = {Abel, Andreas},
1145+booktitle = {Language},
1146+file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
1147+title = {{foetus - Termination Checker for Simple Functional Programs}},
1148+year = {1998}
1149+}
1150+@article{Jones1999,
1151+abstract = {Haskell benefits from a sophisticated type system, but implementors, programmers, and researchers suffer because it has no formal description. To remedy this shortcoming, we present a Haskell program that implements a Haskell typechecker, thus providing a mathematically rigorous specification in a notation that is familiar to Haskell users. We expect this program to fill a serious gap in current descriptions of Haskell, both as a starting point for discussions about existing features of the type system, and as a platform from which to explore new proposals.},
1152+author = {Jones, Mark P},
1169−journal = {Citeseer},
1153+journal = {October},
1170publisher = {Citeseer},
1154publisher = {Citeseer},
1171−title = {{Generic Programming with Dependent Types}},
1155+title = {{Typing Haskell in Haskell}},
1172−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf},
1156+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
1173−year = {2010}
1157+year = {1999}
1174}
1158}
1175−@article{Steiner1988,
1159+@inproceedings{morris2006exploring,
1176−author = {Steiner, JG},
1160+author = {Morris, P. and Altenkirch, T. and McBride, C.},
1177−file = {:home/edwin/Research/Papers/Mendeley/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
1161+booktitle = {Types for Proofs and Programs},
1178−journal = {Proc. Winter USENIX Conference},
1162+file = {:Users/edwin/Documents/Mendeley Desktop/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},
1179−title = {{Kerberos: An authentication service for open network systems}},
1163+pages = {252--267},
1180−url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},
1164+publisher = {Springer},
1165+title = {{Exploring the regular tree types}},
1166+url = {http://www.springerlink.com/index/f9p1317716614834.pdf},
1181−year = {1988}
1167+year = {2006}
1182}
1168}
1183−@phdthesis{Okasaki1996,
1169+@inproceedings{Sheard2005,
1184−author = {Okasaki, Chris},
1170+address = {New York, New York, USA},
1185−file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
1171+author = {Sheard, Tim},
1186−school = {Carnegie Mellon University},
1172+booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},
1187−title = {{Purely Functional Data Structures}},
1173+doi = {10.1145/1088348.1088356},
1174+file = {:Users/edwin/Documents/Mendeley Desktop/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},
1175+isbn = {159593071X},
1176+keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},
1177+month = sep,
1178+pages = {74--85},
1179+publisher = {ACM Press},
1180+title = {{Putting curry-howard to work}},
1181+url = {http://dl.acm.org/citation.cfm?id=1088348.1088356},
1188−year = {1996}
1182+year = {2005}
1189}
1183}
1190−@article{Abel2010,
1184+@misc{Interface2012a,
1191−abstract = {Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism. To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language, MiniAgda, with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by concepts such as inaccessible patterns and parametric function spaces. This paper provides an introduction to MiniAgda by example and informal explanations of the underlying principles.},
1185+author = {Kreibich, Jay A.},
1192−author = {Abel, Andreas},
1186+doi = {10.1093/epirev/mxr031},
1193−file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
1187+file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
1194−journal = {EPTCS},
1188+isbn = {9781449394592},
1195−pages = {1--15},
1189+issn = {1478-6729},
1196−title = {{MiniAgda: Integrating Sized and Dependent Types}},
1190+pmid = {22215642},
1197−url = {http://arxiv.org/abs/1012.4896},
1191+title = {{Using SQLite Chapter 7}}
1198−volume = {43},
1199−year = {2010}
1200}
1192}
1193+@book{The2012,
1194+author = {Hunt, Andrew and Thomas, David},
1195+booktitle = {Carcinogenesis},
1196+doi = {10.1093/carcin/bgs054},
1197+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
1198+isbn = {020161622X},
1199+issn = {1460-2180},
1200+number = {3},
1201+pmid = {22383472},
1202+title = {{The Pragmatic Programmer Chapter 3}},
1203+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
1204+volume = {33}
1205+}
1206+@misc{Brady2012b,
1207+author = {Brooks, Fred},
1208+doi = {10.1093/epirev/mxr031},
1209+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
1210+isbn = {9780321702081},
1211+issn = {1478-6729},
1212+pmid = {22215642},
1213+title = {{The Design of Design Chapter 2}}
1214+}
1201−@inproceedings{Brady2006b,
1215+@inproceedings{Levitation2010,
1202−author = {Brady, Edwin},
1216+author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},
1203−booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},
1217+booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},
1204−file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
1218+doi = {10.1145/1932681.1863547},
1219+file = {:Users/edwin/Documents/Mendeley Desktop/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},
1205−isbn = {978-3-540-74129-9},
1220+isbn = {978-1-60558-794-3},
1221+issn = {03621340},
1222+keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},
1223+mendeley-tags = {Dependent Types},
1206month = sep,
1224month = sep,
1225+number = {9},
1207−pages = {145----162},
1226+pages = {3},
1208−title = {{Ivor, a proof engine}},
1227+title = {{The gentle art of levitation}},
1209−url = {http://dl.acm.org/citation.cfm?id=1757028.1757037},
1228+url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},
1229+volume = {45},
1210−year = {2006}
1230+year = {2010}
1211}
1231}
1212−@article{Hughes1989,
1232+@inproceedings{Xi1999,
1213−abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},
1233+abstract = {Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.},
1214−author = {Hughes, J},
1234+author = {Xi, Hongwei and Pfenning, Frank},
1215−chapter = {2},
1235+booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},
1216−doi = {10.1093/comjnl/32.2.98},
1236+doi = {10.1145/292540.292560},
1217−editor = {Turner, David A},
1237+file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},
1218−file = {:home/edwin/Research/Papers/Mendeley/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
1238+isbn = {1581130953},
1219−institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},
1239+issn = {07439016},
1220−isbn = {0201172364},
1240+keywords = {Dependent Types},
1221−issn = {00104620},
1241+mendeley-tags = {Dependent Types},
1222−journal = {The Computer Journal},
1242+organization = {Carnegie Mellon University},
1223−number = {2},
1224−pages = {98--107},
1243+pages = {214--227},
1225−publisher = {Br Computer Soc},
1244+publisher = {ACM Press},
1226−title = {{Why Functional Programming Matters}},
1245+series = {POPL '99},
1227−url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},
1246+title = {{Dependent types in practical programming}},
1247+url = {http://portal.acm.org/citation.cfm?doid=292540.292560},
1228−volume = {32},
1248+volume = {26},
1229−year = {1989}
1249+year = {1999}
1230}
1250}
1231−@article{mccann2000packet,
1251+@inproceedings{Brady2003,
1232−author = {McCann, P.J. and Chandra, S.},
1252+author = {Brady, Edwin and McBride, Conor and McKinna, James},
1233−journal = {ACM SIGCOMM Computer Communication Review},
1253+booktitle = {Types for Proofs and Programs},
1254+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},
1255+keywords = {Dependent Types},
1256+mendeley-tags = {Dependent Types},
1257+title = {{Inductive families need not store their indices}},
1258+url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},
1259+year = {2003}
1260+}
1261+@inproceedings{fisher2005pads,
1262+author = {Fisher, K. and Gruber, R.},
1263+booktitle = {ACM SIGPLAN Notices},
1234−number = {4},
1264+number = {6},
1235−pages = {321--333},
1265+pages = {295--304},
1236publisher = {ACM},
1266publisher = {ACM},
1237−title = {{Packet types: abstract specification of network protocol messages}},
1267+title = {{PADS: a domain-specific language for processing ad hoc data}},
1238−url = {http://dl.acm.org/citation.cfm?id=347563},
1268+url = {http://dl.acm.org/citation.cfm?id=1065046},
1239−volume = {30},
1269+volume = {40},
1240−year = {2000}
1270+year = {2005}
1241}
1271}