@@ -1,40 +1,54 @@
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.
4−@inproceedings{gibbons2011modularising,
4+@book{Cryptography2012,
5−author = {Gibbons, J. and Ko, H.S. and Others},
5+author = {Anderson, Ross},
6−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Proceedings of the seventh ACM SIGPLAN workshop on Generic programming/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
6+doi = {10.1093/intimm/dxs023},
7−title = {{Modularising inductive families}},
7+file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 5.pdf:pdf},
8−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
8+isbn = {9780470068526},
9−year = {2011}
9+issn = {1460-2377},
11−@inproceedings{czarnecki2004dsl,
11+pmid = {22451589},
12−author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},
12+title = {{Security Engineering Chapter 5}},
13−booktitle = {Domain-Specific Program Generation},
13+url = {http://www.ncbi.nlm.nih.gov/pubmed/22451589},
14−file = {:Users/edwin/Documents/Mendeley Desktop/Czarnecki et al/Domain-Specific Program Generation/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},
14+volume = {24}
16−publisher = {Springer},
17−title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},
18−url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},
21−@phdthesis{Brady2005,
16+@inproceedings{norell2009dependently,
22−author = {Brady, Edwin},
17+author = {Norell, Ulf},
23−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Unknown/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
18+booktitle = {Advanced Functional Programming},
19+file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},
24keywords = {Dependent Types},
20keywords = {Dependent Types},
25mendeley-tags = {Dependent Types},
21mendeley-tags = {Dependent Types},
26−school = {University of Durham},
22+pages = {230--266},
27−title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},
23+publisher = {Springer},
28−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf},
24+title = {{Dependently typed programming in Agda}},
25+url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},
29−year = {2005}
26+year = {2009}
31−@inproceedings{Kimmell2012,
28+@article{Mandelbaum2007,
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},
29+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.},
33−booktitle = {Programming Languages meets Program Verification},
30+author = {Mandelbaum, Yitzhak and Fisher, Kathleen and Walker, David and Fernandez, Mary and Gleyzer, Artem},
34−file = {:Users/edwin/Documents/Mendeley Desktop/Kimmell et al/Programming Languages meets Program Verification/Kimmell et al. - 2012 - Equational reasoning about programs with general recursion and call-by-value semantics.pdf:pdf},
31+doi = {10.1145/1190215.1190231},
35−title = {{Equational reasoning about programs with general recursion and call-by-value semantics}},
32+isbn = {1595935754},
36−url = {http://dl.acm.org/citation.cfm?id=2103780},
33+issn = {03621340},
34+journal = {SIGPLAN Not},
39+title = {{PADS/ML: a functional data description language}},
40+url = {http://doi.acm.org/10.1145/1190216.1190231},
45+author = {Abadi, Martin and Gordon, Andrew D},
46+booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},
47+file = {:home/edwin/Research/Papers/Mendeley/Abadi, Gordon/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},
49+title = {{A calculus for cryptographic protocols: The spi calculus}},
50+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},
37−year = {2012}
51+year = {1997}
39@article{Epstein2011,
53@article{Epstein2011,
40author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},
54author = {Epstein, Jeff and Black, Andrew P and Peyton-jones, Simon},
@@ -46,52 +60,12 @@ title = {{Haskell for the cloud}},
46url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf},
60url = {http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/remote.pdf},
47year = {2011}
61year = {2011}
49−@article{Altenkirch2010a,
63+@misc{TheMendeleySupportTeam2011a,
50−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.},
51−author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},
52−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Mcbride, Morris/Citeseer/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
54−publisher = {Citeseer},
55−title = {{Generic Programming with Dependent Types}},
56−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf},
59−@article{fisher2006next,
60−author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},
61−file = {:Users/edwin/Documents/Mendeley Desktop/Fisher, Mandelbaum, Walker/Journal of the ACM/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},
62−journal = {Journal of the ACM},
66−title = {{The next 700 data description languages}},
67−url = {http://dl.acm.org/citation.cfm?id=1111039},
72−author = {Brooks, Fred},
73−doi = {10.1093/epirev/mxr031},
74−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
75−isbn = {9780321702081},
78−title = {{The Design of Design Chapter 1}}
80−@article{Chapman2005epigram,
81−author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},
82−file = {:Users/edwin/Documents/Mendeley Desktop/Chapman, Altenkirch, McBride/Trends in Functional Programming/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},
83−journal = {Trends in Functional Programming},
84−publisher = {Intellect Books},
85−title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
86−url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
89−@misc{TheMendeleySupportTeam2011,
90abstract = {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.},
64abstract = {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.},
91address = {London},
65address = {London},
92author = {{The Mendeley Support Team}},
66author = {{The Mendeley Support Team}},
93booktitle = {Mendeley Desktop},
67booktitle = {Mendeley Desktop},
94−file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/Mendeley Desktop/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
68+file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
95keywords = {Mendeley,how-to,user manual},
69keywords = {Mendeley,how-to,user manual},
96pages = {1--16},
70pages = {1--16},
97publisher = {Mendeley Ltd.},
71publisher = {Mendeley Ltd.},
@@ -99,102 +73,20 @@ title = {{Getting Started with Mendeley}},
99url = {http://www.mendeley.com},
73url = {http://www.mendeley.com},
100year = {2011}
74year = {2011}
102−@phdthesis{Okasaki1996,
76+@article{Jones1999,
103−author = {Okasaki, Chris},
77+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.},
104−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Unknown/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
78+author = {Jones, Mark P},
105−school = {Carnegie Mellon University},
79+journal = {October},
106−title = {{Purely Functional Data Structures}},
109−@article{mcbride2008functional,
110−author = {McBride, C. and Paterson, R.},
111−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Journal of functional programming/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
112−journal = {Journal of functional programming},
115−publisher = {Cambridge Univ Press},
116−title = {{Functional pearl: Applicative programming with effects}},
117−url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=1457860},
121−@inproceedings{madhavapeddy2007melange,
122−author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
123−booktitle = {ACM SIGOPS Operating Systems Review},
124−file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/ACM SIGOPS Operating Systems Review/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},
128−title = {{Melange: creating a functional internet}},
129−url = {http://dl.acm.org/citation.cfm?id=1273009},
133−@inproceedings{lempsink2009type,
134−author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},
135−booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},
136−file = {:Users/edwin/Documents/Mendeley Desktop/Lempsink, Leather, L\"{o}h/Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},
138−publisher = {ACM},
80+publisher = {Citeseer},
139−title = {{Type-safe diff for families of datatypes}},
81+title = {{Typing Haskell in Haskell}},
140−url = {http://dl.acm.org/citation.cfm?id=1596624},
82+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
144−author = {Hunt, Andrew and Thomas, David},
145−booktitle = {Carcinogenesis},
146−doi = {10.1093/carcin/bgs054},
147−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
152−title = {{The Pragmatic Programmer Chapter 2}},
153−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
156−@inproceedings{stump2010resource,
157−author = {Stump, A. and Austin, E.},
158−booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},
159−file = {:Users/edwin/Documents/Mendeley Desktop/Stump, Austin/Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},
162−title = {{Resource typing in Guru}},
163−url = {http://dl.acm.org/citation.cfm?id=1707796},
164−year = {2010}
83+year = {1999}
166−@article{mcbride2010ornamental,
167−author = {McBride, Conor},
168−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Journal of Functional Programming/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
169−journal = {Journal of Functional Programming},
170−title = {{Ornamental algebras, algebraic ornaments}},
171−url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},
174−@article{Swierstra2011,
175−author = {Swierstra, W},
176−file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra/Journal of Functional Programming/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},
177−journal = {Journal of Functional Programming},
179−pages = {575----583},
180−title = {{Sorted: Verifying the Problem of the {Dutch National} Flag in {Agda}}},
181−url = {http://journals.cambridge.org/abstract_S0956796811000207},
185−@article{McBride2002,
186−author = {McBride, C},
187−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Types for proofs and programs ({TYPES 2000})/McBride - 2000 - Elimination with a Motive.pdf:pdf},
188−journal = {Types for proofs and programs ({TYPES 2000})},
189−title = {{Elimination with a Motive}},
190−url = {http://www.springerlink.com/index/vbpg19305t46f6dm.pdf},
193@article{Xi1998,
85@article{Xi1998,
194abstract = {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.},
86abstract = {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.},
195author = {Xi, Hongwei and Pfenning, Frank},
87author = {Xi, Hongwei and Pfenning, Frank},
196doi = {10.1145/277652.277732},
88doi = {10.1145/277652.277732},
197−file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/ACM Sigplan Notices/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},
89+file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},
198isbn = {0897919874},
90isbn = {0897919874},
199issn = {03621340},
91issn = {03621340},
200journal = {ACM Sigplan Notices},
92journal = {ACM Sigplan Notices},
@@ -209,102 +101,250 @@ url = {http://portal.acm.org/citation.cfm?doid=277652.277732},
209volume = {33},
101volume = {33},
210year = {1998}
102year = {1998}
212−@misc{idristutorial,
104+@book{The2012,
213−author = {Brady, Edwin},
105+author = {Hunt, Andrew and Thomas, David},
214−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Unknown/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
215−title = {{Programming in Idris : a tutorial}},
216−url = {http://idris-lang.org/tutorial},
219−@inproceedings{NanevskiAAMorrisett2008,
220−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.},
221−author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},
222−booktitle = {International Conference on Functional Programming},
223−doi = {10.1145/1411204.1411237},
224−file = {:Users/edwin/Documents/Mendeley Desktop/Nanevski A A Morrisett/International Conference on Functional Programming/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},
225−isbn = {9781595939197},
227−keywords = {Dependent Types},
228−mendeley-tags = {Dependent Types},
231−title = {{Ynot: Dependent types for imperative programs}},
232−url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},
237−author = {Brooks, Fred},
238−doi = {10.1093/epirev/mxr031},
239−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},
240−isbn = {9780321702081},
245−title = {{The Design of Design Chapter 5}},
248−@inproceedings{ko2011modularising,
249−author = {Ko, H.S. and Gibbons, J.},
250−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
251−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Proceedings of the seventh ACM SIGPLAN workshop on Generic programming/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
254−title = {{Modularising inductive families}},
255−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},
259−author = {Fowler, Martin},
260booktitle = {Carcinogenesis},
106booktitle = {Carcinogenesis},
261doi = {10.1093/carcin/bgs054},
107doi = {10.1093/carcin/bgs054},
262−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Carcinogenesis/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
108+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
263−isbn = {9780132107549},
109+isbn = {020161622X},
264issn = {1460-2180},
110issn = {1460-2180},
265number = {3},
111number = {3},
266pmid = {22383472},
112pmid = {22383472},
267−title = {{Domain Specific Languages Chapter 6}},
113+title = {{The Pragmatic Programmer Chapter 3}},
268url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
114url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
269volume = {33}
115volume = {33}
271−@article{marlow2006making,
117+@article{danielsson2011parsing,
272−author = {Marlow, S. and {Peyton Jones}, S.},
118+author = {Danielsson, N. and Norell, U.},
273−file = {:Users/edwin/Documents/Mendeley Desktop/Marlow, Peyton Jones/Journal of Functional Programming/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},
119+journal = {Implementation and Application of Functional Languages},
274−journal = {Journal of Functional Programming},
276−pages = {415--449},
120+pages = {80--99},
277−publisher = {Cambridge University Press},
121+publisher = {Springer},
278−title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}},
122+title = {{Parsing mixfix operators}},
279−url = {http://dl.acm.org/citation.cfm?id=1166018},
123+url = {http://www.springerlink.com/index/386243257W504252.pdf},
281−year = {2006}
124+year = {2011}
283−@article{Mandelbaum2007,
126+@misc{Bove2008,
284−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.},
127+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.},
285−author = {Mandelbaum, Yitzhak and Fisher, Kathleen and Walker, David and Fernandez, Mary and Gleyzer, Artem},
128+author = {Bove, Ana and Dybjer, Peter},
286−doi = {10.1145/1190215.1190231},
129+booktitle = {Notes},
287−isbn = {1595935754},
130+doi = {10.1007/978-3-642-03153-3_2},
288−issn = {03621340},
131+file = {:home/edwin/Research/Papers/Mendeley/Bove, Dybjer/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},
289−journal = {SIGPLAN Not},
132+number = {February},
134+publisher = {Springer},
135+title = {{Dependent Types at Work}},
136+url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},
142+publisher = {Oxford University Press, Inc.},
143+title = {{Computation and reasoning: a type theory for computer science}},
144+url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},
147+@inproceedings{Delahaye2000,
148+author = {Delahaye, D},
149+booktitle = {Logic for Programming and Automated Reasoning},
150+file = {:home/edwin/Research/Papers/Mendeley/Delahaye/Delahaye - 2000 - A tactic language for the system Coq.pdf:pdf;:home/edwin/Research/Papers/Mendeley/Delahaye/Delahaye - 2000 - A tactic language for the system Coq(2).pdf:pdf},
152+publisher = {Springer},
153+title = {{A tactic language for the system Coq}},
154+url = {http://www.springerlink.com/index/EFQAH8J88K42VN8T.pdf},
158+author = {Brady, Edwin},
159+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
160+title = {{Programming in Idris : a tutorial}},
161+url = {http://idris-lang.org/tutorial},
164+@inproceedings{madhavapeddy2007melange,
165+author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
166+booktitle = {ACM SIGOPS Operating Systems Review},
167+file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},
171+title = {{Melange: creating a functional internet}},
172+url = {http://dl.acm.org/citation.cfm?id=1273009},
176+@inproceedings{ko2011modularising,
177+author = {Ko, H.S. and Gibbons, J.},
178+booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
179+file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
182+title = {{Modularising inductive families}},
183+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html http://dl.acm.org/citation.cfm?id=2036921},
186+@inproceedings{Augustsson1998,
187+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.},
188+author = {Augustsson, Lennart},
189+booktitle = {International Conference on Functional Programming},
190+doi = {10.1097/MEG.0b013e328342f213},
191+file = {:home/edwin/Research/Papers/Mendeley/Augustsson/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},
193+keywords = {Depe,Dependent Types},
194+mendeley-tags = {Depe,Dependent Types},
290number = {1},
195number = {1},
291−pages = {77--83},
196+pages = {239--250},
198+publisher = {ACM Press},
199+title = {{Cayenne - a language with dependent types}},
200+url = {http://www.cs.chalmers.se/$\sim$augustss/cayenne/paper.ps},
204+@inproceedings{Altenkirch2010,
205+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.},
206+author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
207+booktitle = {{FLOPS 2010}},
208+doi = {10.1007/978-3-642-12251-4_5},
209+editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
210+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
211+isbn = {9783642122507},
213+publisher = {Springer Berlin Heidelberg},
214+series = {Lecture Notes in Computer Science},
215+title = {{Dependent Types without the Sugar}},
216+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
219+@inproceedings{brady2011epic,
220+author = {Brady, Edwin},
221+booktitle = {Trends in Functional Programming ({TFP}’11)},
222+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},
223+title = {{Epic --- A Library for Generating Compilers}},
224+url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},
228+author = {Bertot, Yves and Cast\'{e}ran, Pierre},
229+publisher = {Springer},
230+title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},
231+url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},
234+@inproceedings{ko2011modularising,
235+author = {Ko, H.S. and Gibbons, J.},
236+booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
292publisher = {ACM},
238publisher = {ACM},
293−series = {POPL '07},
239+title = {{Modularising inductive families}},
294−title = {{PADS/ML: a functional data description language}},
240+url = {http://dl.acm.org/citation.cfm?id=2036921},
295−url = {http://doi.acm.org/10.1145/1190216.1190231},
241+year = {2011}
243+@misc{altenkirch2008nσ,
244+author = {Altenkirch, T. and Oury, N.},
245+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
246+title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},
247+url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},
250+@inproceedings{taha1997multi,
251+author = {Taha, W. and Sheard, T.},
252+booktitle = {ACM SIGPLAN Notices},
256+title = {{Multi-stage programming with explicit annotations}},
257+url = {http://dl.acm.org/citation.cfm?id=259019},
296−volume = {42},
258+volume = {32},
262+author = {Hunt, Andrew and Thomas, David},
263+booktitle = {Design},
264+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
266+title = {{The Pragmatic Programmer Chapter 4}}
268+@inproceedings{bradyresource,
269+author = {Brady, Edwin and Hammond, Kevin},
270+booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},
271+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},
272+pages = {242----257},
273+title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},
274+url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},
277+@article{McBride2007,
278+author = {McBride, Conor and Paterson, Ross},
279+file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
280+journal = {Journal of functional programming},
281+title = {{Applicative programming with effects}},
282+url = {http://journals.cambridge.org/abstract_S0956796807006326},
297year = {2007}
283year = {2007}
299−@article{Abel2010,
285+@article{fisher2006next,
300−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.},
286+author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},
301−author = {Abel, Andreas},
287+file = {:home/edwin/Research/Papers/Mendeley/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},
302−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/EPTCS/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
288+journal = {Journal of the ACM},
303−journal = {EPTCS},
289+number = {2},
292+title = {{The next 700 data description languages}},
293+url = {http://dl.acm.org/citation.cfm?id=1111039},
298+author = {Bird, Richard},
299+file = {:home/edwin/Research/Papers/Mendeley/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
300+isbn = {9780521513388},
301+title = {{Pearls of Functional Algorithm Design}},
304+@inproceedings{stump2010resource,
305+author = {Stump, A. and Austin, E.},
306+booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},
307+file = {:home/edwin/Research/Papers/Mendeley/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},
310+title = {{Resource typing in Guru}},
311+url = {http://dl.acm.org/citation.cfm?id=1707796},
314+@inproceedings{barras2008implicit,
315+author = {Barras, B. and Bernardo, B.},
316+booktitle = {Foundations of Software Science and Computational Structures},
317+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},
319+publisher = {Springer},
320+title = {{The implicit calculus of constructions as a programming language with dependent types}},
321+url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
325+abstract = {The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.},
326+author = {Wadler, Philip},
327+doi = {10.1007/3-540-59451-5_2},
328+editor = {Jeuring, Johan and Meijer, Erik},
329+file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 2001 - Monads for functional programming.pdf:pdf},
332+journal = {Advanced Functional Programming},
333+number = {August 1992},
304−pages = {1--15},
334+pages = {24--52},
305−title = {{MiniAgda: Integrating Sized and Dependent Types}},
335+publisher = {Springer},
306−url = {http://arxiv.org/abs/1012.4896},
336+series = {Lecture Notes in Computer Science},
337+title = {{Monads for functional programming}},
338+url = {http://www.springerlink.com/index/715264614rh13340.pdf},
307−volume = {43},
339+volume = {925},
342+@inproceedings{Fournet2011,
343+author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},
344+booktitle = {Foundations of security analysis and design {VI}},
345+file = {:home/edwin/Research/Papers/Mendeley/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},
346+title = {{Cryptographic verification by typing for a sample protocol implementation}},
347+url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
308year = {2010}
348year = {2010}
310@article{Hoare1978,
350@article{Hoare1978,
@@ -312,7 +352,7 @@ abstract = {This paper suggests that input and output are basic primitives of pr
312author = {Hoare, C A R},
352author = {Hoare, C A R},
313doi = {10.1016/0167-6423(87)90028-1},
353doi = {10.1016/0167-6423(87)90028-1},
314editor = {McKeag, R M and Macnaghten, A M},
354editor = {McKeag, R M and Macnaghten, A M},
315−file = {:Users/edwin/Documents/Mendeley Desktop/Hoare/Communications of the ACM/Hoare - 1978 - Communicating sequential processes.pdf:pdf},
355+file = {:home/edwin/Research/Papers/Mendeley/Hoare/Hoare - 1978 - Communicating sequential processes.pdf:pdf},
316isbn = {0131532715},
356isbn = {0131532715},
317issn = {01676423},
357issn = {01676423},
318journal = {Communications of the ACM},
358journal = {Communications of the ACM},
@@ -326,17 +366,174 @@ url = {http://linkinghub.elsevier.com/retrieve/pii/0167642387900281},
326volume = {21},
366volume = {21},
327year = {1978}
367year = {1978}
329−@book{Bird2010,
369+@book{While2012,
330−author = {Bird, Richard},
370+author = {Hunt, Andrew and Thomas, David},
331−file = {:Users/edwin/Documents/Mendeley Desktop/Bird/Unknown/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
371+booktitle = {Carcinogenesis},
332−isbn = {9780521513388},
372+doi = {10.1093/carcin/bgs054},
333−title = {{Pearls of Functional Algorithm Design}},
373+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
334−year = {2010}
374+isbn = {020161622X},
378+title = {{The Pragmatic Programmer Chapter 6}},
379+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
382+@inproceedings{Brady2010,
383+author = {Brady, Edwin and Hammond, Kevin},
384+booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
385+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},
386+isbn = {9781605587943},
387+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},
388+mendeley-tags = {Dependent Types},
391+title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},
392+url = {http://portal.acm.org/citation.cfm?id=1863587},
395+@inproceedings{Visser2008,
396+author = {Visser, E},
397+booktitle = {Generative and Transformational Techniques in Software Engineering},
398+title = {{WebDSL: A case study in domain-specific language engineering}},
399+url = {http://www.springerlink.com/index/A3213003X6268032.pdf},
402+@inproceedings{Brady2005a,
403+author = {Brady, E and Hammond, K},
404+booktitle = {Implementation and Application of Functional \ldots},
405+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},
406+keywords = {Dependent Types},
407+mendeley-tags = {Dependent Types},
408+title = {{A dependently typed framework for static analysis of program execution costs}},
409+url = {http://www.springerlink.com/index/P446P2HH70107759.pdf},
412+@inproceedings{madhavapeddy2010turning,
413+author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
414+booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
415+file = {:home/edwin/Research/Papers/Mendeley/Madhavapeddy et al/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},
416+publisher = {USENIX Association},
417+title = {{Turning down the LAMP: software specialisation for the cloud}},
418+url = {http://dl.acm.org/citation.cfm?id=1863114},
421+@inproceedings{bhargavan2010modular,
422+author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},
423+booktitle = {ACM Sigplan Notices},
427+title = {{Modular verification of security protocol code by typing}},
428+url = {http://dl.acm.org/citation.cfm?id=1707801.1706350},
434+file = {:home/edwin/Research/Papers/Mendeley/Huet/Huet - 1997 - The zipper.pdf:pdf},
435+journal = {{Journal of Functional Programming}},
437+pages = {549----554},
438+title = {{The zipper}},
439+url = {http://journals.cambridge.org/abstract_S0956796897002864},
443+@book{Philosophy2012,
444+author = {Hunt, Andrew and Thomas, David},
445+booktitle = {Carcinogenesis},
446+doi = {10.1093/carcin/bgs054},
447+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
452+title = {{The Pragmatic Programmer Chapter 1}},
453+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
456+@inproceedings{coquand1986analysis,
457+author = {Coquand, T.},
458+booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},
459+file = {:home/edwin/Research/Papers/Mendeley/Coquand/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},
460+pages = {227----246},
461+title = {{An analysis of Girard's paradox}},
462+url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},
465+@inproceedings{Augustsson1985,
466+address = {Berlin, Heidelberg},
467+author = {Augustsson, Lennart},
468+booktitle = {Functional Programming Languages and Computer Architecture},
469+doi = {10.1007/3-540-15975-4},
470+editor = {Jouannaud, Jean-Pierre},
471+isbn = {978-3-540-15975-9},
472+keywords = {Computer Science},
473+pages = {368----381},
474+publisher = {Springer Berlin Heidelberg},
475+series = {Lecture Notes in Computer Science},
476+title = {{Compiling Pattern Matching}},
477+url = {http://www.springerlink.com/content/y647423656557505/},
482+author = {Brooks, Fred},
483+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},
484+isbn = {9780321702081},
485+title = {{The Design of Design Chapter 4}}
488+author = {Brooks, Fred},
489+doi = {10.1093/epirev/mxr031},
490+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},
491+isbn = {9780321702081},
496+title = {{The Design of Design Chapter 5}},
500+author = {Fowler, Martin},
501+booktitle = {Carcinogenesis},
502+doi = {10.1093/carcin/bgs054},
503+file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
504+isbn = {9780132107549},
508+title = {{Domain Specific Languages Chapter 6}},
509+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
512+@article{mcbride2008functional,
513+author = {McBride, C. and Paterson, R.},
514+file = {:home/edwin/Research/Papers/Mendeley/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
515+journal = {Journal of functional programming},
518+publisher = {Cambridge Univ Press},
519+title = {{Functional pearl: Applicative programming with effects}},
520+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=1457860},
524+@inproceedings{pollack1990implicit,
525+author = {Pollack, R.},
526+booktitle = {{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}},
527+file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},
528+publisher = {Citeseer},
529+title = {{Implicit syntax}},
530+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
336@inproceedings{oury2008power,
533@inproceedings{oury2008power,
337author = {Oury, N. and Swierstra, W.},
534author = {Oury, N. and Swierstra, W.},
338booktitle = {International Conference on Functional Programming},
535booktitle = {International Conference on Functional Programming},
339−file = {:Users/edwin/Documents/Mendeley Desktop/Oury, Swierstra/International Conference on Functional Programming/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
536+file = {:home/edwin/Research/Papers/Mendeley/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
340keywords = {Dependent Types},
537keywords = {Dependent Types},
341mendeley-tags = {Dependent Types},
538mendeley-tags = {Dependent Types},
342number = {9},
539number = {9},
@@ -347,196 +544,195 @@ url = {http://dl.acm.org/citation.cfm?id=1411213},
347volume = {43},
544volume = {43},
348year = {2008}
545year = {2008}
350−@inproceedings{madhavapeddy2010turning,
547+@article{gordon2003authenticity,
351−author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
548+author = {Gordon, A.D. and Jeffrey, A.},
352−booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
549+file = {:home/edwin/Research/Papers/Mendeley/Gordon, Jeffrey/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},
353−file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Proceedings of the 2nd USENIX conference on Hot topics in cloud computing/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},
550+journal = {Journal of computer security},
354−publisher = {USENIX Association},
553+publisher = {IOS Press},
355−title = {{Turning down the LAMP: software specialisation for the cloud}},
554+title = {{Authenticity by typing for security protocols}},
356−url = {http://dl.acm.org/citation.cfm?id=1863114},
555+url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},
357−year = {2010}
557+year = {2003}
359−@book{peyton1987implementation,
559+@misc{pollack1997believe,
360−author = {{Peyton Jones}, S.L.},
560+author = {Pollack, R.},
361−publisher = {Prentice-Hall, Inc.},
561+file = {:home/edwin/Research/Papers/Mendeley/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
362−title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}},
562+title = {{How to believe a machine-checked proof}},
363−url = {http://dl.acm.org/citation.cfm?id=1096899},
563+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},
364−year = {1987}
564+year = {1997}
366−@inproceedings{Pasalic2002,
566+@misc{Attacks2012a,
367−author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},
567+author = {Anderson, Ross},
368−booktitle = {International Conference on Functional Programming},
568+doi = {10.1093/epirev/mxr031},
369−doi = {10.1145/583852.581499},
569+file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},
370−file = {:Users/edwin/Documents/Mendeley Desktop/Pa\v{s}alic, Taha, Sheard/International Conference on Functional Programming/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},
570+isbn = {9780470068526},
371−isbn = {1-58113-487-8},
571+issn = {1478-6729},
373−keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},
375−number = {9},
572+number = {1},
376−pages = {218--229},
573+pages = {NP},
377−title = {{Tagless staged interpreters for typed languages}},
574+pmid = {22215642},
378−url = {http://dl.acm.org/citation.cfm?id=583852.581499},
575+title = {{Security Engineering Chapter 18}},
379−volume = {37},
576+volume = {34}
382−@inproceedings{Brady2010,
578+@inproceedings{atkey2009unembedding,
383−author = {Brady, Edwin and Hammond, Kevin},
579+author = {Atkey, R. and Lindley, S. and Yallop, J.},
384−booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
580+booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
385−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Proceedings of the 15th ACM SIGPLAN international conference on Functional programming/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},
386−isbn = {9781605587943},
387−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},
388−mendeley-tags = {Dependent Types},
389−pages = {297--308},
581+pages = {37--48},
390publisher = {ACM},
582publisher = {ACM},
391−title = {{Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation}},
583+title = {{Unembedding domain-specific languages}},
392−url = {http://portal.acm.org/citation.cfm?id=1863587},
584+url = {http://dl.acm.org/citation.cfm?id=1596644},
393−year = {2010}
585+year = {2009}
395−@inproceedings{Fournet2011,
587+@article{loh2010tutorial,
396−author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},
588+author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},
397−booktitle = {Foundations of security analysis and design {VI}},
589+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},
398−file = {:Users/edwin/Documents/Mendeley Desktop/Fournet, Bhargavan, Gordon/Foundations of security analysis and design {VI}/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},
590+journal = {Fundamenta Informaticae},
399−title = {{Cryptographic verification by typing for a sample protocol implementation}},
591+number = {2},
400−url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
592+pages = {177--207},
593+publisher = {IOS Press},
594+title = {{A tutorial implementation of a dependently typed lambda calculus}},
595+url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},
401year = {2010}
597year = {2010}
403−@article{landin1966next,
599+@inproceedings{czarnecki2004dsl,
404−author = {Landin, P.J.},
600+author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},
405−file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Communications of the ACM/Landin - 1966 - The next 700 programming languages.pdf:pdf},
601+booktitle = {Domain-Specific Program Generation},
406−journal = {Communications of the ACM},
602+file = {:home/edwin/Research/Papers/Mendeley/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},
408−pages = {157--166},
603+pages = {51--72},
409−publisher = {ACM},
604+publisher = {Springer},
410−title = {{The next 700 programming languages}},
605+title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},
411−url = {http://dl.acm.org/citation.cfm?id=365257 )},
606+url = {http://www.springerlink.com/index/NL620EL7N94M161H.pdf},
413−year = {1966}
607+year = {2004}
415−@inproceedings{bhargavan2010modular,
609+@inproceedings{NanevskiAAMorrisett2008,
416−author = {Bhargavan, K. and Fournet, C. and Gordon, A.D.},
610+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.},
611+author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},
612+booktitle = {International Conference on Functional Programming},
613+doi = {10.1145/1411204.1411237},
614+file = {:home/edwin/Research/Papers/Mendeley/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},
615+isbn = {9781595939197},
617+keywords = {Dependent Types},
618+mendeley-tags = {Dependent Types},
621+title = {{Ynot: Dependent types for imperative programs}},
622+url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=40&md5=7a5be3083878399cebafda33b1affa6b},
626+@inproceedings{fisher2005pads,
627+author = {Fisher, K. and Gruber, R.},
417−booktitle = {ACM Sigplan Notices},
628+booktitle = {ACM SIGPLAN Notices},
418−number = {1},
629+number = {6},
419−pages = {445--456},
630+pages = {295--304},
420publisher = {ACM},
631publisher = {ACM},
421−title = {{Modular verification of security protocol code by typing}},
632+title = {{PADS: a domain-specific language for processing ad hoc data}},
422−url = {http://dl.acm.org/citation.cfm?id=1707801.1706350},
633+url = {http://dl.acm.org/citation.cfm?id=1065046},
423−volume = {45},
634+volume = {40},
424−year = {2010}
635+year = {2005}
426−@article{Haskell2012a,
637+@inproceedings{McBride2004b,
427−author = {Biancuzzi, F and Warden, S},
638+author = {McBride, Conor and McKinna, James},
639+booktitle = {Haskell Workshop},
640+file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},
641+title = {{I am not a number : I am a free variable}},
644+@article{marlow2006making,
645+author = {Marlow, S. and {Peyton Jones}, S.},
646+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},
647+journal = {Journal of Functional Programming},
650+publisher = {Cambridge University Press},
651+title = {{Making a fast curry: push/enter vs. eval/apply for higher-order languages}},
652+url = {http://dl.acm.org/citation.cfm?id=1166018},
656+@misc{Protocols2012a,
657+author = {Anderson, Ross},
428doi = {10.1093/epirev/mxr031},
658doi = {10.1093/epirev/mxr031},
429−file = {:Users/edwin/Documents/Mendeley Desktop/Biancuzzi, Warden/Unknown/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
659+file = {:home/edwin/Research/Papers/Mendeley/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
430−isbn = {9780596801670},
660+isbn = {9780470068526},
431issn = {1478-6729},
661issn = {1478-6729},
432pmid = {22215642},
662pmid = {22215642},
433−title = {{Masterminds of Programming Chapter 8}}
663+title = {{Security Engineering Chapter 3}}
436−author = {Hunt, Andrew and Thomas, David},
437−booktitle = {Carcinogenesis},
438−doi = {10.1093/carcin/bgs054},
439−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
444−title = {{The Pragmatic Programmer Chapter 5}},
445−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
448−@article{McBride2007,
449−author = {McBride, Conor and Paterson, Ross},
450−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Journal of functional programming/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
451−journal = {Journal of functional programming},
452−title = {{Applicative programming with effects}},
453−url = {http://journals.cambridge.org/abstract_S0956796807006326},
456−@inproceedings{Altenkirch2010,
665+@inproceedings{McBride2006,
457−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.},
666+author = {McBride, C and Goguen, H and McKinna, J},
458−author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres and Oury, Nicolas},
667+booktitle = {Types for Proofs and Programs {(TYPES 2006)}},
459−booktitle = {{FLOPS 2010}},
668+title = {{A few constructions on constructors}},
460−doi = {10.1007/978-3-642-12251-4_5},
461−editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
462−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch et al/{FLOPS 2010}/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
463−isbn = {9783642122507},
465−publisher = {Springer Berlin Heidelberg},
466−series = {Lecture Notes in Computer Science},
467−title = {{Dependent Types without the Sugar}},
468−url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
669+url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
469−year = {2010}
670+year = {2006}
471−@article{McBride2005,
672+@article{McBride2002,
472−author = {McBride, Conor},
673+author = {McBride, C},
473−editor = {Vene, Varmo and Uustalu, Tarmo},
674+file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2000 - Elimination with a Motive.pdf:pdf},
474−isbn = {3540285407},
675+journal = {Types for proofs and programs ({TYPES 2000})},
475−journal = {Advanced Functional Programming},
676+title = {{Elimination with a Motive}},
476−keywords = {Dependent Types},
477−mendeley-tags = {Dependent Types},
479−publisher = {Springer},
480−series = {Lecture Notes in Computer Science},
481−title = {{Epigram: Practical programming with dependent types}},
482−url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},
677+url = {http://www.springerlink.com/index/vbpg19305t46f6dm.pdf},
484−year = {2005}
678+year = {2000}
486−@article{Huet1997,
680+@inproceedings{Sculthorpe2009,
487−author = {Huet, G},
681+author = {Sculthorpe, Neil and Nilsson, Henrik},
488−file = {:Users/edwin/Documents/Mendeley Desktop/Huet/{Journal of Functional Programming}/Huet - 1997 - The zipper.pdf:pdf},
682+booktitle = {International Conference on Functional Programming ({ICFP} '09)},
489−journal = {{Journal of Functional Programming}},
683+file = {:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:home/edwin/Research/Papers/Mendeley/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},
490−number = {5},
684+title = {{Safe functional reactive programming through dependent types}},
491−pages = {549----554},
685+url = {http://dl.acm.org/citation.cfm?id=1596558},
492−title = {{The zipper}},
493−url = {http://journals.cambridge.org/abstract_S0956796897002864},
495−year = {1997}
686+year = {2009}
497−@misc{Bloat,
688+@book{Fowler,
498−author = {Brooks, Fred},
689+author = {Fowler, Martin},
499−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},
690+booktitle = {Language},
500−isbn = {9780321702081},
691+file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
501−title = {{The Design of Design Chapter 4}}
692+isbn = {9780132107549},
693+title = {{Domain Specific Languages Chapter 2}}
503−@misc{Protocols2012a,
695+@inproceedings{Sheard2005,
504−author = {Anderson, Ross},
696+address = {New York, New York, USA},
505−doi = {10.1093/epirev/mxr031},
697+author = {Sheard, Tim},
506−file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Unknown/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
698+booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},
507−isbn = {9780470068526},
699+doi = {10.1145/1088348.1088356},
508−issn = {1478-6729},
700+file = {:home/edwin/Research/Papers/Mendeley/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},
509−pmid = {22215642},
701+isbn = {159593071X},
510−title = {{Security Engineering Chapter 3}}
702+keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},
705+publisher = {ACM Press},
706+title = {{Putting curry-howard to work}},
707+url = {http://dl.acm.org/citation.cfm?id=1088348.1088356},
512−@inproceedings{Augustsson1998,
710+@article{Jones2003,
513−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.},
711+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.},
514−author = {Augustsson, Lennart},
712+author = {Jones, Simon Peyton},
515−booktitle = {International Conference on Functional Programming},
713+editor = {Jones, Simon Peyton},
516−doi = {10.1097/MEG.0b013e328342f213},
714+isbn = {0521826144},
517−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/International Conference on Functional Programming/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},
715+journal = {Language},
519−keywords = {Depe,Dependent Types},
520−mendeley-tags = {Depe,Dependent Types},
521number = {1},
716number = {1},
524−publisher = {ACM Press},
717+publisher = {Cambridge University Press},
525−title = {{Cayenne - a language with dependent types}},
718+title = {{Haskell 98 Language and Libraries The Revised Report}},
526−url = {http://www.cs.chalmers.se/$\sim$augustss/cayenne/paper.ps},
719+url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},
527−volume = {23},
720+volume = {13},
528−year = {1998}
721+year = {2003}
530−@book{Hunt,
723+@article{Brady2006a,
531−author = {Hunt, Andrew and Thomas, David},
724+author = {Brady, E and Hammond, K},
532−booktitle = {Design},
725+file = {:home/edwin/Research/Papers/Mendeley/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},
533−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Design/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
726+journal = {\ldots of the 5th international conference on \ldots},
534−isbn = {020161622X},
727+keywords = {Dependent Types},
535−title = {{The Pragmatic Programmer Chapter 4}}
728+mendeley-tags = {Dependent Types},
729+title = {{A verified staged interpreter is a verified compiler}},
730+url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},
537@article{burrows1990,
733@article{burrows1990,
538author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
734author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
539−file = {:Users/edwin/Documents/Mendeley Desktop/Burrows, Abadi, Needham/ACM Transactions on Computer Systems/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},
735+file = {:home/edwin/Research/Papers/Mendeley/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},
540journal = {ACM Transactions on Computer Systems},
736journal = {ACM Transactions on Computer Systems},
541pages = {18----36},
737pages = {18----36},
542title = {{A logic of authentication}},
738title = {{A logic of authentication}},
@@ -544,113 +740,98 @@ url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.115.3569},
544volume = {8},
740volume = {8},
545year = {1990}
741year = {1990}
547−@inproceedings{atkey2009unembedding,
743+@phdthesis{McBride1999,
548−author = {Atkey, R. and Lindley, S. and Yallop, J.},
744+author = {McBride, Conor},
549−booktitle = {Proceedings of the 2nd ACM SIGPLAN symposium on Haskell},
745+file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
552−title = {{Unembedding domain-specific languages}},
553−url = {http://dl.acm.org/citation.cfm?id=1596644},
556−@inproceedings{Brady2011a,
557−address = {New York, New York, USA},
558−author = {Brady, Edwin},
559−booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},
560−doi = {10.1145/1929529.1929536},
561−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},
562−isbn = {9781450304870},
563−keywords = {Dependent Types,data description,dependent types},
746+keywords = {Dependent Types},
564mendeley-tags = {Dependent Types},
747mendeley-tags = {Dependent Types},
565−month = jan,
748+school = {University of Edinburgh},
566−publisher = {ACM Press},
749+title = {{Dependently typed functional programs and their proofs}},
567−title = {{Idris --- Systems Programming Meets Full Dependent Types}},
750+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
568−url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
572−author = {Fowler, Martin},
573−booktitle = {Carcinogenesis},
574−doi = {10.1093/carcin/bgs054},
575−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Carcinogenesis/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
576−isbn = {9780132107549},
580−title = {{Domain Specific Languages Chapter 1}},
581−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
584−@inproceedings{coquand1986analysis,
585−author = {Coquand, T.},
586−booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},
587−file = {:Users/edwin/Documents/Mendeley Desktop/Coquand/{Proceedings of the First IEEE Symposium on Logic in Computer Science}/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},
588−pages = {227----246},
589−title = {{An analysis of Girard's paradox}},
590−url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},
591−year = {1986}
751+year = {1999}
593−@misc{altenkirch2008nσ,
594−author = {Altenkirch, T. and Oury, N.},
595−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Oury/Unknown/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
596−title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},
597−url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},
600−@inproceedings{barras2008implicit,
601−author = {Barras, B. and Bernardo, B.},
602−booktitle = {Foundations of Software Science and Computational Structures},
603−file = {:Users/edwin/Documents/Mendeley Desktop/Barras, Bernardo/Foundations of Software Science and Computational Structures/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},
605−publisher = {Springer},
606−title = {{The implicit calculus of constructions as a programming language with dependent types}},
607−url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
610−@book{While2012,
753+@article{mcbride2010ornamental,
611−author = {Hunt, Andrew and Thomas, David},
754+author = {McBride, Conor},
612−booktitle = {Carcinogenesis},
755+file = {:home/edwin/Research/Papers/Mendeley/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
613−doi = {10.1093/carcin/bgs054},
756+journal = {Journal of Functional Programming},
614−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
757+title = {{Ornamental algebras, algebraic ornaments}},
615−isbn = {020161622X},
758+url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},
616−issn = {1460-2180},
759+year = {2010}
619−title = {{The Pragmatic Programmer Chapter 6}},
620−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
623−@inproceedings{bradyresource,
761+@article{Chapman2005epigram,
624−author = {Brady, Edwin and Hammond, Kevin},
762+author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},
625−booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},
763+file = {:home/edwin/Research/Papers/Mendeley/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},
626−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Practical Applications of Declarative Languages ({PADL} 2012)/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},
764+journal = {Trends in Functional Programming},
627−pages = {242----257},
765+publisher = {Intellect Books},
628−title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},
766+title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
629−url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},
767+url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
630−year = {2012}
768+year = {2005}
632−@book{luo1994,
770+@inproceedings{Levitation2010,
633−author = {Luo, Z.},
771+author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},
634−publisher = {Oxford University Press, Inc.},
772+booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},
635−title = {{Computation and reasoning: a type theory for computer science}},
773+doi = {10.1145/1932681.1863547},
774+file = {:home/edwin/Research/Papers/Mendeley/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},
775+isbn = {978-1-60558-794-3},
777+keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},
778+mendeley-tags = {Dependent Types},
781+title = {{The gentle art of levitation}},
636−url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},
782+url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},
637−year = {1994}
784+year = {2010}
639−@phdthesis{norell2007thesis,
786+@article{McBride2004a,
640−author = {Norell, Ulf},
787+abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.},
641−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Unknown/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
788+author = {McBride, Conor and McKinna, James},
789+doi = {10.1017/S0956796803004829},
790+file = {:home/edwin/Research/Papers/Mendeley/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
792+journal = {Journal of Functional Programming},
642keywords = {Dependent Types},
793keywords = {Dependent Types},
643mendeley-tags = {Dependent Types},
794mendeley-tags = {Dependent Types},
797+publisher = {Cambridge University Press},
798+title = {{The view from the left}},
799+url = {http://www.journals.cambridge.org/abstract_S0956796803004829},
803+@article{Altenkirch2010a,
804+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.},
805+author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},
806+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
807+journal = {Citeseer},
644publisher = {Citeseer},
808publisher = {Citeseer},
645−school = {Chalmers University of Technology},
809+title = {{Generic Programming with Dependent Types}},
646−title = {{Towards a practical programming language based on dependent type theory}},
647−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
810+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.129.2926&rep=rep1&type=pdf},
648−year = {2007}
811+year = {2010}
813+@phdthesis{Okasaki1996,
814+author = {Okasaki, Chris},
815+file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
816+school = {Carnegie Mellon University},
817+title = {{Purely Functional Data Structures}},
821+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.},
822+author = {Abel, Andreas},
823+file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
826+title = {{MiniAgda: Integrating Sized and Dependent Types}},
827+url = {http://arxiv.org/abs/1012.4896},
650@inproceedings{Brady2006b,
831@inproceedings{Brady2006b,
651author = {Brady, Edwin},
832author = {Brady, Edwin},
652booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},
833booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},
653−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Implementation and Application of Functional Languages ({IFL}'06)/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
834+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
654isbn = {978-3-540-74129-9},
835isbn = {978-3-540-74129-9},
655month = sep,
836month = sep,
656pages = {145----162},
837pages = {145----162},
@@ -658,79 +839,110 @@ title = {{Ivor, a proof engine}},
658url = {http://dl.acm.org/citation.cfm?id=1757028.1757037},
839url = {http://dl.acm.org/citation.cfm?id=1757028.1757037},
659year = {2006}
840year = {2006}
661−@inproceedings{chlipala2010ur,
842+@misc{TheMendeleySupportTeam2011,
662−author = {Chlipala, Adam},
843+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.},
663−booktitle = {ACM SIGPLAN Notices},
844+address = {London},
664−file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/ACM SIGPLAN Notices/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
845+author = {{The Mendeley Support Team}},
665−number = {6},
846+booktitle = {Mendeley Desktop},
847+file = {:home/edwin/Research/Papers/Mendeley/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
848+keywords = {Mendeley,how-to,user manual},
666−pages = {122--133},
849+pages = {1--16},
667−publisher = {ACM},
850+publisher = {Mendeley Ltd.},
668−title = {{Ur: statically-typed metaprogramming with type-level record computation}},
851+title = {{Getting Started with Mendeley}},
669−url = {http://dl.acm.org/citation.cfm?id=1806612},
852+url = {http://www.mendeley.com},
674−author = {Abadi, Martin and Gordon, Andrew D},
675−booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},
676−file = {:Users/edwin/Documents/Mendeley Desktop/Abadi, Gordon/4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},
678−title = {{A calculus for cryptographic protocols: The spi calculus}},
679−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},
680−year = {1997}
853+year = {2011}
682−@inproceedings{McBride2006,
855+@article{mccann2000packet,
683−author = {McBride, C and Goguen, H and McKinna, J},
856+author = {McCann, P.J. and Chandra, S.},
684−booktitle = {Types for Proofs and Programs {(TYPES 2006)}},
857+journal = {ACM SIGCOMM Computer Communication Review},
685−title = {{A few constructions on constructors}},
858+number = {4},
686−url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
859+pages = {321--333},
861+title = {{Packet types: abstract specification of network protocol messages}},
862+url = {http://dl.acm.org/citation.cfm?id=347563},
687−year = {2006}
864+year = {2000}
689−@article{Jones2003,
866+@article{Steiner1988,
690−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.},
867+author = {Steiner, JG},
691−author = {Jones, Simon Peyton},
868+file = {:home/edwin/Research/Papers/Mendeley/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
692−editor = {Jones, Simon Peyton},
869+journal = {Proc. Winter USENIX Conference},
693−isbn = {0521826144},
870+title = {{Kerberos: An authentication service for open network systems}},
694−journal = {Language},
871+url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},
696−publisher = {Cambridge University Press},
697−title = {{Haskell 98 Language and Libraries The Revised Report}},
698−url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0521826144},
700−year = {2003}
872+year = {1988}
702−@inproceedings{Visser2008,
874+@article{Hughes1989,
875+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.},
703−author = {Visser, E},
876+author = {Hughes, J},
704−booktitle = {Generative and Transformational Techniques in Software Engineering},
877+chapter = {2},
705−title = {{WebDSL: A case study in domain-specific language engineering}},
878+doi = {10.1093/comjnl/32.2.98},
706−url = {http://www.springerlink.com/index/A3213003X6268032.pdf},
879+editor = {Turner, David A},
880+file = {:home/edwin/Research/Papers/Mendeley/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
881+institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},
884+journal = {The Computer Journal},
887+publisher = {Br Computer Soc},
888+title = {{Why Functional Programming Matters}},
889+url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},
707−year = {2008}
891+year = {1989}
709−@inproceedings{ko2011modularising,
893+@inproceedings{gibbons2011modularising,
710−author = {Ko, H.S. and Gibbons, J.},
894+author = {Gibbons, J. and Ko, H.S. and Others},
711−booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
895+file = {:home/edwin/Research/Papers/Mendeley/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
714title = {{Modularising inductive families}},
896title = {{Modularising inductive families}},
715−url = {http://dl.acm.org/citation.cfm?id=2036921},
897+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
716year = {2011}
898year = {2011}
718−@misc{Attacks2012a,
900+@article{Okasaki1993,
719−author = {Anderson, Ross},
901+author = {Okasaki, Chris},
902+file = {:home/edwin/Research/Papers/Mendeley/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
903+journal = {Journal of functional programming},
904+title = {{Red-Black Trees in A Functional Setting}},
908+author = {Brooks, Fred},
720doi = {10.1093/epirev/mxr031},
909doi = {10.1093/epirev/mxr031},
721−file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Unknown/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},
910+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
722−isbn = {9780470068526},
911+isbn = {9780321702081},
723issn = {1478-6729},
912issn = {1478-6729},
726pmid = {22215642},
913pmid = {22215642},
727−title = {{Security Engineering Chapter 18}},
914+title = {{The Design of Design Chapter 2}}
916+@inproceedings{Wadler1989,
917+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.},
918+author = {Wadler, Philip},
919+booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
920+doi = {10.1145/99370.99404},
921+file = {:home/edwin/Research/Papers/Mendeley/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},
927+title = {{Theorems for free!}},
928+url = {http://portal.acm.org/citation.cfm?id=99404},
931+@inproceedings{Hancock2000,
932+author = {Hancock, Peter and Setzer, Anton},
933+booktitle = {{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}},
934+file = {:home/edwin/Research/Papers/Mendeley/Hancock, Setzer/Hancock, Setzer - 2000 - Interactive Programs in Dependent Type Theory.pdf:pdf},
935+isbn = {3-540-67895-6},
938+title = {{Interactive Programs in Dependent Type Theory}},
939+url = {http://dl.acm.org/citation.cfm?id=647850.737221},
730@inproceedings{l,
942@inproceedings{l,
731author = {L\"{a}mmel, R. and Jones, S.P.},
943author = {L\"{a}mmel, R. and Jones, S.P.},
732booktitle = {ACM SIGPLAN Notices},
944booktitle = {ACM SIGPLAN Notices},
733−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{a}mmel, Jones/ACM SIGPLAN Notices/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},
945+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},
734number = {3},
946number = {3},
735pages = {26--37},
947pages = {26--37},
736publisher = {ACM},
948publisher = {ACM},
@@ -739,175 +951,75 @@ url = {http://dl.acm.org/citation.cfm?id=640136.604179},
739volume = {38},
951volume = {38},
740year = {2003}
952year = {2003}
742−@inproceedings{Delahaye2000,
954+@inproceedings{Xi1999,
743−author = {Delahaye, D},
955+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.},
744−booktitle = {Logic for Programming and Automated Reasoning},
956+author = {Xi, Hongwei and Pfenning, Frank},
745−file = {:Users/edwin/Documents/Mendeley Desktop/Delahaye/Logic for Programming and Automated Reasoning/Delahaye - 2000 - A tactic language for the system Coq.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Delahaye/Logic for Programming and Automated Reasoning/Delahaye - 2000 - A tactic language for the system Coq(2).pdf:pdf},
957+booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},
746−pages = {85----95},
958+doi = {10.1145/292540.292560},
747−publisher = {Springer},
959+file = {:home/edwin/Research/Papers/Mendeley/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},
748−title = {{A tactic language for the system Coq}},
960+isbn = {1581130953},
749−url = {http://www.springerlink.com/index/EFQAH8J88K42VN8T.pdf},
961+issn = {07439016},
750−year = {2000}
962+keywords = {Dependent Types},
751−}
963+mendeley-tags = {Dependent Types},
752−@misc{pollack1997believe,
964+organization = {Carnegie Mellon University},
753−author = {Pollack, R.},
754−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Unknown/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
755−title = {{How to believe a machine-checked proof}},
756−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},
760−author = {Bertot, Yves and Cast\'{e}ran, Pierre},
761−publisher = {Springer},
762−title = {{Interactive theorem proving and program development: {Coq'Art}: the {Calculus of Inductive Constructions}}},
763−url = {http://books.google.co.uk/books?hl=en&lr=&id=m5w5PRj5Nj4C&oi=fnd&pg=PA1&dq=coq+theorem+prover&ots=VHny1IYV0h&sig=-K0FC67cdkhMDkAocFla8cZyRT4},
766−@inproceedings{brady2011epic,
767−author = {Brady, Edwin},
768−booktitle = {Trends in Functional Programming ({TFP}’11)},
769−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Trends in Functional Programming ({TFP}’11)/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},
770−title = {{Epic --- A Library for Generating Compilers}},
771−url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},
774−@article{dybjer1994inductive,
775−author = {Dybjer, P.},
776−journal = {Formal aspects of computing},
778−pages = {440--465},
965+pages = {214--227},
779−publisher = {Springer},
966+publisher = {ACM Press},
780−title = {{Inductive families}},
967+series = {POPL '99},
781−url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
968+title = {{Dependent types in practical programming}},
969+url = {http://portal.acm.org/citation.cfm?doid=292540.292560},
782−volume = {6},
970+volume = {26},
785−@inproceedings{McBride2004b,
786−author = {McBride, Conor and McKinna, James},
787−booktitle = {Haskell Workshop},
788−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/Haskell Workshop/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},
789−title = {{I am not a number : I am a free variable}},
790−year = {2004}
971+year = {1999}
792−@article{Wadler2001,
973+@inproceedings{morris2006exploring,
793−abstract = {The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effects found in other languages, such as global state, exception handling, output, or non-determinism. Three case studies are looked at in detail: how monads ease the modification of a simple evaluator; how monads act as the basis of a datatype of arrays subject to in-place update; and how monads can be used to build parsers.},
974+author = {Morris, P. and Altenkirch, T. and McBride, C.},
794−author = {Wadler, Philip},
975+booktitle = {Types for Proofs and Programs},
795−doi = {10.1007/3-540-59451-5_2},
976+file = {:home/edwin/Research/Papers/Mendeley/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},
796−editor = {Jeuring, Johan and Meijer, Erik},
797−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Advanced Functional Programming/Wadler - 2001 - Monads for functional programming.pdf:pdf},
800−journal = {Advanced Functional Programming},
801−number = {August 1992},
802−pages = {24--52},
977+pages = {252--267},
803publisher = {Springer},
978publisher = {Springer},
804−series = {Lecture Notes in Computer Science},
979+title = {{Exploring the regular tree types}},
805−title = {{Monads for functional programming}},
806−url = {http://www.springerlink.com/index/715264614rh13340.pdf},
980+url = {http://www.springerlink.com/index/f9p1317716614834.pdf},
810−@inproceedings{taha1997multi,
811−author = {Taha, W. and Sheard, T.},
812−booktitle = {ACM SIGPLAN Notices},
816−title = {{Multi-stage programming with explicit annotations}},
817−url = {http://dl.acm.org/citation.cfm?id=259019},
821−@article{loh2010tutorial,
822−author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},
823−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{o}h, McBride, Swierstra/Fundamenta Informaticae/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},
824−journal = {Fundamenta Informaticae},
827−publisher = {IOS Press},
828−title = {{A tutorial implementation of a dependently typed lambda calculus}},
829−url = {http://iospress.metapress.com/index/976W4716TM79M6U8.pdf},
831−year = {2010}
981+year = {2006}
833−@book{Philosophy2012,
983+@book{Approach2012,
834author = {Hunt, Andrew and Thomas, David},
984author = {Hunt, Andrew and Thomas, David},
835booktitle = {Carcinogenesis},
985booktitle = {Carcinogenesis},
836doi = {10.1093/carcin/bgs054},
986doi = {10.1093/carcin/bgs054},
837−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
987+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
838isbn = {020161622X},
988isbn = {020161622X},
839issn = {1460-2180},
989issn = {1460-2180},
840number = {3},
990number = {3},
841pmid = {22383472},
991pmid = {22383472},
842−title = {{The Pragmatic Programmer Chapter 1}},
992+title = {{The Pragmatic Programmer Chapter 2}},
843url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
993url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
844volume = {33}
994volume = {33}
846−@inproceedings{pollack1990implicit,
996+@misc{Abel1998,
847−author = {Pollack, R.},
997+author = {Abel, Andreas},
848−booktitle = {{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}},
998+booktitle = {Language},
849−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}/Pollack - 1990 - Implicit syntax.pdf:pdf},
999+file = {:home/edwin/Research/Papers/Mendeley/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
850−publisher = {Citeseer},
1000+title = {{foetus - Termination Checker for Simple Functional Programs}},
851−title = {{Implicit syntax}},
1001+year = {1998}
852−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
855−@article{gordon2003authenticity,
856−author = {Gordon, A.D. and Jeffrey, A.},
857−file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Journal of computer security/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},
858−journal = {Journal of computer security},
861−publisher = {IOS Press},
862−title = {{Authenticity by typing for security protocols}},
863−url = {http://iospress.metapress.com/index/BHQQUFRA1C7W8TLY.pdf},
867−@inproceedings{Wadler1989,
868−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.},
869−author = {Wadler, Philip},
870−booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
871−doi = {10.1145/99370.99404},
872−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Proceedings of the fourth international conference on Functional programming languages and computer architecture/Wadler - 1989 - Theorems for free!.pdf:pdf},
878−title = {{Theorems for free!}},
879−url = {http://portal.acm.org/citation.cfm?id=99404},
882−@inproceedings{Augustsson1985,
883−address = {Berlin, Heidelberg},
884−author = {Augustsson, Lennart},
885−booktitle = {Functional Programming Languages and Computer Architecture},
886−doi = {10.1007/3-540-15975-4},
887−editor = {Jouannaud, Jean-Pierre},
888−isbn = {978-3-540-15975-9},
889−keywords = {Computer Science},
890−pages = {368----381},
891−publisher = {Springer Berlin Heidelberg},
892−series = {Lecture Notes in Computer Science},
893−title = {{Compiling Pattern Matching}},
894−url = {http://www.springerlink.com/content/y647423656557505/},
898−@inproceedings{Brady2005a,
1003+@article{Miller1992,
899−author = {Brady, E and Hammond, K},
1004+author = {Miller, Dale},
900−booktitle = {Implementation and Application of Functional \ldots},
1005+file = {:home/edwin/Research/Papers/Mendeley/Miller/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},
901−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Implementation and Application of Functional \ldots/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},
1006+journal = {Journal of Symbolic Computation},
902−keywords = {Dependent Types},
1007+title = {{Unification under a mixed prefix}},
903−mendeley-tags = {Dependent Types},
1008+url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},
904−title = {{A dependently typed framework for static analysis of program execution costs}},
905−url = {http://www.springerlink.com/index/P446P2HH70107759.pdf},
906−year = {2005}
1009+year = {1992}
1011+@misc{Interface2012a,
1012+author = {Kreibich, Jay A.},
1013+doi = {10.1093/epirev/mxr031},
1014+file = {:home/edwin/Research/Papers/Mendeley/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
1015+isbn = {9781449394592},
1018+title = {{Using SQLite Chapter 7}}
908@article{Vytiniotis2011,
1020@article{Vytiniotis2011,
909author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},
1021author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},
910−file = {:Users/edwin/Documents/Mendeley Desktop/Vytiniotis et al/{Journal of Functional Programming}/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Vytiniotis et al/{Journal of Functional Programming}/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions(2).pdf:pdf},
1022+file = {:home/edwin/Research/Papers/Mendeley/Vytiniotis et al/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions.pdf:pdf;:home/edwin/Research/Papers/Mendeley/Vytiniotis et al/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions(2).pdf:pdf},
911journal = {{Journal of Functional Programming}},
1023journal = {{Journal of Functional Programming}},
912number = {4--5},
1024number = {4--5},
913pages = {333----412},
1025pages = {333----412},
@@ -916,162 +1028,104 @@ url = {http://journals.cambridge.org/abstract_S0956796811000098},
916volume = {21},
1028volume = {21},
917year = {2011}
1029year = {2011}
919−@article{mccann2000packet,
920−author = {McCann, P.J. and Chandra, S.},
921−journal = {ACM SIGCOMM Computer Communication Review},
925−title = {{Packet types: abstract specification of network protocol messages}},
926−url = {http://dl.acm.org/citation.cfm?id=347563},
931−author = {Miller, Dale},
932−file = {:Users/edwin/Documents/Mendeley Desktop/Miller/Journal of Symbolic Computation/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},
933−journal = {Journal of Symbolic Computation},
934−title = {{Unification under a mixed prefix}},
935−url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},
938−@inproceedings{norell2009dependently,
1031+@inproceedings{Brady2003,
939−author = {Norell, Ulf},
1032+author = {Brady, Edwin and McBride, Conor and McKinna, James},
940−booktitle = {Advanced Functional Programming},
1033+booktitle = {Types for Proofs and Programs {(TYPES 2003)}},
941−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Advanced Functional Programming/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},
1034+file = {:home/edwin/Research/Papers/Mendeley/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},
942keywords = {Dependent Types},
1035keywords = {Dependent Types},
943mendeley-tags = {Dependent Types},
1036mendeley-tags = {Dependent Types},
944−pages = {230--266},
1037+title = {{Inductive families need not store their indices}},
945−publisher = {Springer},
946−title = {{Dependently typed programming in Agda}},
947−url = {http://www.springerlink.com/index/8X0H38858233VN26.pdf},
1038+url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},
948−year = {2009}
1039+year = {2003}
951−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.},
952−author = {Hughes, J},
954−doi = {10.1093/comjnl/32.2.98},
955−editor = {Turner, David A},
956−file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/The Computer Journal/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
957−institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},
960−journal = {The Computer Journal},
963−publisher = {Br Computer Soc},
964−title = {{Why Functional Programming Matters}},
965−url = {http://comjnl.oupjournals.org/cgi/doi/10.1093/comjnl/32.2.98},
969−@article{Steiner1988,
970−author = {Steiner, JG},
971−file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Proc. Winter USENIX Conference/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
972−journal = {Proc. Winter USENIX Conference},
973−title = {{Kerberos: An authentication service for open network systems}},
974−url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},
977−@phdthesis{McBride1999,
1041+@inproceedings{swierstra2007beauty,
978−author = {McBride, Conor},
1042+author = {Swierstra, W. and Altenkirch, T.},
979−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Unknown/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
1043+booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
980−keywords = {Dependent Types},
1044+file = {:home/edwin/Research/Papers/Mendeley/Swierstra, Altenkirch/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},
981−mendeley-tags = {Dependent Types},
1045+pages = {25--36},
982−school = {University of Edinburgh},
1046+publisher = {ACM},
983−title = {{Dependently typed functional programs and their proofs}},
1047+title = {{Beauty in the beast}},
984−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
1048+url = {http://dl.acm.org/citation.cfm?id=1291206},
985−year = {1999}
1049+year = {2007}
987−@inproceedings{augustsson1999exercise,
1051+@book{peyton1987implementation,
988−author = {Augustsson, L. and Carlsson, M.},
1052+author = {{Peyton Jones}, S.L.},
989−booktitle = {In Workshop on Dependent Types in Programming, Gothenburg},
991−mendeley-tags = {Depe},
992−publisher = {Citeseer},
1053+publisher = {Prentice-Hall, Inc.},
993−title = {{An exercise in dependent types: A well-typed interpreter}},
1054+title = {{The implementation of functional programming languages (prentice-hall international series in computer science)}},
994−url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2895},
1055+url = {http://dl.acm.org/citation.cfm?id=1096899},
995−year = {1999}
1056+year = {1987}
997−@inproceedings{taha2004gentle,
1058+@article{dybjer1994inductive,
998−author = {Taha, W.},
1059+author = {Dybjer, P.},
999−booktitle = {Domain-Specific Program Generation},
1060+journal = {Formal aspects of computing},
1000−pages = {30--50},
1062+pages = {440--465},
1001publisher = {Springer},
1063publisher = {Springer},
1002−title = {{A gentle introduction to multi-stage programming}},
1064+title = {{Inductive families}},
1003−url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},
1065+url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
1004−year = {2004}
1067+year = {1994}
1006−@inproceedings{Sculthorpe2009,
1069+@inproceedings{lempsink2009type,
1007−author = {Sculthorpe, Neil and Nilsson, Henrik},
1070+author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},
1008−booktitle = {International Conference on Functional Programming ({ICFP} '09)},
1071+booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},
1009−file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/International Conference on Functional Programming ({ICFP} '09)/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/International Conference on Functional Programming ({ICFP} '09)/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},
1072+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},
1010−title = {{Safe functional reactive programming through dependent types}},
1073+pages = {61--72},
1075+title = {{Type-safe diff for families of datatypes}},
1011−url = {http://dl.acm.org/citation.cfm?id=1596558},
1076+url = {http://dl.acm.org/citation.cfm?id=1596624},
1012year = {2009}
1077year = {2009}
1014−@misc{TheMendeleySupportTeam2011a,
1079+@misc{The2012b,
1015−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.},
1080+author = {Brooks, Fred},
1016−address = {London},
1081+doi = {10.1093/epirev/mxr031},
1017−author = {{The Mendeley Support Team}},
1082+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
1018−booktitle = {Mendeley Desktop},
1083+isbn = {9780321702081},
1019−file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/Mendeley Desktop/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
1084+issn = {1478-6729},
1020−keywords = {Mendeley,how-to,user manual},
1085+pmid = {22215642},
1021−pages = {1--16},
1086+title = {{The Design of Design Chapter 1}}
1022−publisher = {Mendeley Ltd.},
1023−title = {{Getting Started with Mendeley}},
1024−url = {http://www.mendeley.com},
1027−@article{danielsson2011parsing,
1088+@misc{The2012c,
1028−author = {Danielsson, N. and Norell, U.},
1089+author = {Robbins, A and Hannah, E and Lamb, L},
1029−journal = {Implementation and Application of Functional Languages},
1090+doi = {10.1093/epirev/mxr031},
1091+file = {:home/edwin/Research/Papers/Mendeley/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
1092+isbn = {9780596529833},
1095+title = {{Learning the vi and Vim Editors}}
1097+@inproceedings{chlipala2010ur,
1098+author = {Chlipala, Adam},
1099+booktitle = {ACM SIGPLAN Notices},
1100+file = {:home/edwin/Research/Papers/Mendeley/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
1030−pages = {80--99},
1102+pages = {122--133},
1031−publisher = {Springer},
1103+publisher = {ACM},
1032−title = {{Parsing mixfix operators}},
1104+title = {{Ur: statically-typed metaprogramming with type-level record computation}},
1033−url = {http://www.springerlink.com/index/386243257W504252.pdf},
1105+url = {http://dl.acm.org/citation.cfm?id=1806612},
1034−year = {2011}
1107+year = {2010}
1036@misc{dagand2011transporting,
1109@misc{dagand2011transporting,
1037author = {Dagand, Pierre-Evariste and McBride, Conor},
1110author = {Dagand, Pierre-Evariste and McBride, Conor},
1038−file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Unknown/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
1111+file = {:home/edwin/Research/Papers/Mendeley/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
1039title = {{Transporting Functions across Ornaments}},
1112title = {{Transporting Functions across Ornaments}},
1040url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},
1113url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},
1041year = {2011}
1114year = {2011}
1043−@book{Fowler,
1116+@inproceedings{taha2004gentle,
1044−author = {Fowler, Martin},
1117+author = {Taha, W.},
1045−booktitle = {Language},
1118+booktitle = {Domain-Specific Program Generation},
1046−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Language/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
1047−isbn = {9780132107549},
1048−title = {{Domain Specific Languages Chapter 2}}
1051−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.},
1052−author = {Bove, Ana and Dybjer, Peter},
1053−booktitle = {Notes},
1054−doi = {10.1007/978-3-642-03153-3_2},
1055−file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Notes/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},
1056−number = {February},
1057−pages = {57--99},
1119+pages = {30--50},
1058publisher = {Springer},
1120publisher = {Springer},
1059−title = {{Dependent Types at Work}},
1121+title = {{A gentle introduction to multi-stage programming}},
1060−url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},
1122+url = {http://www.springerlink.com/index/JEMT0D8VYN5JB2L8.pdf},
1064−@article{Okasaki1993,
1065−author = {Okasaki, Chris},
1066−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Journal of functional programming/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
1067−journal = {Journal of functional programming},
1068−title = {{Red-Black Trees in A Functional Setting}},
1069−year = {1993}
1123+year = {2004}
1071@inproceedings{pj2006gadts,
1125@inproceedings{pj2006gadts,
1072author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
1126author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
1073booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
1127booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
1074−file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/{International Conference on Functional Programming} ({ICFP} '06)/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
1128+file = {:home/edwin/Research/Papers/Mendeley/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
1075number = {9},
1129number = {9},
1076pages = {50--61},
1130pages = {50--61},
1077publisher = {ACM},
1131publisher = {ACM},
@@ -1080,92 +1134,149 @@ url = {http://dl.acm.org/citation.cfm?id=1159811},
1080volume = {41},
1134volume = {41},
1081year = {2006}
1135year = {2006}
1083−@misc{altenkirch2005dependent,
1137+@book{Brady2012,
1084−author = {Altenkirch, T. and McBride, C. and McKinna, J.},
1138+author = {Hunt, Andrew and Thomas, David},
1085−booktitle = {Manuscript, available online},
1139+booktitle = {Carcinogenesis},
1086−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Manuscript, available online/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
1140+doi = {10.1093/carcin/bgs054},
1087−title = {{Why dependent types matter}},
1141+file = {:home/edwin/Research/Papers/Mendeley/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
1088−url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},
1142+isbn = {020161622X},
1146+title = {{The Pragmatic Programmer Chapter 5}},
1147+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
1150+@inproceedings{Pasalic2002,
1151+author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},
1152+booktitle = {International Conference on Functional Programming},
1153+doi = {10.1145/583852.581499},
1154+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},
1155+isbn = {1-58113-487-8},
1157+keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},
1161+title = {{Tagless staged interpreters for typed languages}},
1162+url = {http://dl.acm.org/citation.cfm?id=583852.581499},
1089−year = {2005}
1164+year = {2002}
1167+author = {Brooks, Fred},
1168+doi = {10.1093/epirev/mxr031},
1169+file = {:home/edwin/Research/Papers/Mendeley/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
1170+isbn = {9780321702081},
1173+title = {{The Design of Design Chapter 3}}
1091−@misc{The2012c,
1175+@book{An2012,
1092−author = {Robbins, A and Hannah, E and Lamb, L},
1176+author = {Fowler, Martin},
1177+booktitle = {Carcinogenesis},
1178+doi = {10.1093/carcin/bgs054},
1179+file = {:home/edwin/Research/Papers/Mendeley/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
1180+isbn = {9780132107549},
1184+title = {{Domain Specific Languages Chapter 1}},
1185+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
1188+@article{Haskell2012a,
1189+author = {Biancuzzi, F and Warden, S},
1093doi = {10.1093/epirev/mxr031},
1190doi = {10.1093/epirev/mxr031},
1094−file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Unknown/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
1191+file = {:home/edwin/Research/Papers/Mendeley/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
1095−isbn = {9780596529833},
1192+isbn = {9780596801670},
1096issn = {1478-6729},
1193issn = {1478-6729},
1097pmid = {22215642},
1194pmid = {22215642},
1098−title = {{Learning the vi and Vim Editors}}
1195+title = {{Masterminds of Programming Chapter 8}}
1197+@article{McBride2005,
1198+author = {McBride, Conor},
1199+editor = {Vene, Varmo and Uustalu, Tarmo},
1200+isbn = {3540285407},
1201+journal = {Advanced Functional Programming},
1202+keywords = {Dependent Types},
1203+mendeley-tags = {Dependent Types},
1205+publisher = {Springer},
1206+series = {Lecture Notes in Computer Science},
1207+title = {{Epigram: Practical programming with dependent types}},
1208+url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},
1212+@article{landin1966next,
1213+author = {Landin, P.J.},
1214+file = {:home/edwin/Research/Papers/Mendeley/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
1215+journal = {Communications of the ACM},
1219+title = {{The next 700 programming languages}},
1220+url = {http://dl.acm.org/citation.cfm?id=365257 )},
1100@misc{Resolution2012a,
1224@misc{Resolution2012a,
1101author = {Fall, Kevin R and Stevens, W. Richard},
1225author = {Fall, Kevin R and Stevens, W. Richard},
1102doi = {10.1093/epirev/mxr031},
1226doi = {10.1093/epirev/mxr031},
1103−file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Unknown/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},
1227+file = {:home/edwin/Research/Papers/Mendeley/Fall, Stevens/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},
1104issn = {1478-6729},
1228issn = {1478-6729},
1105pmid = {22215642},
1229pmid = {22215642},
1106title = {{TCP/IP Illustrated Volume 1 Chapter 11}}
1230title = {{TCP/IP Illustrated Volume 1 Chapter 11}}
1108−@article{Brady2006a,
1232+@phdthesis{Brady2005,
1109−author = {Brady, E and Hammond, K},
1233+author = {Brady, Edwin},
1110−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/\ldots of the 5th international conference on \ldots/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},
1234+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
1111−journal = {\ldots of the 5th international conference on \ldots},
1112keywords = {Dependent Types},
1235keywords = {Dependent Types},
1113mendeley-tags = {Dependent Types},
1236mendeley-tags = {Dependent Types},
1114−title = {{A verified staged interpreter is a verified compiler}},
1237+school = {University of Durham},
1115−url = {http://portal.acm.org/citation.cfm?id=1173706.1173724},
1238+title = {{Practical Implementation of a Dependently Typed Functional Programming Language}},
1116−year = {2006}
1239+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.150.8284&rep=rep1&type=pdf},
1118−@inproceedings{swierstra2007beauty,
1119−author = {Swierstra, W. and Altenkirch, T.},
1120−booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
1121−file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra, Altenkirch/Proceedings of the ACM SIGPLAN workshop on Haskell workshop/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},
1124−title = {{Beauty in the beast}},
1125−url = {http://dl.acm.org/citation.cfm?id=1291206},
1126−year = {2007}
1240+year = {2005}
1128−@article{McBride2004a,
1242+@phdthesis{norell2007thesis,
1129−abstract = {ABSTRACT Pattern matching has proved an extremely powerful and durable notion in functional programming. This paper contributes a new programming notation for type theory which elaborates the notion in various ways. First, as is by now quite well-known in the type theory community, definition by pattern matching becomes a more discriminating tool in the presence of dependent types, since it refines the explanation of types as well as values. This becomes all the more true in the presence of the rich class of datatypes known as inductive families (Dybjer, 1991). Secondly, as proposed by Peyton Jones (1997) for Haskell, and independently rediscovered by us, subsidiary case analyses on the results of intermediate computations, which commonly take place on the right-hand side of definitions by pattern matching, should rather be handled on the left. In simply-typed languages, this subsumes the trivial case of Boolean guards; in our setting it becomes yet more powerful. Thirdly, elementary pattern matching decompositions have a well-defined interface given by a dependent type; they correspond to the statement of an induction principle for the datatype. More general, user-definable decompositions may be defined which also have types of the same general form. Elementary pattern matching may therefore be recast in abstract form, with a semantics given by translation. Such abstract decompositions of data generalize Wadler's (1987) notion of ‘view’. The programmer wishing to introduce a new view of a type mathitT, and exploit it directly in pattern matching, may do so via a standard programming idiom. The type theorist, looking through the Curry–Howard lens, may see this as proving a theorem, one which establishes the validity of a new induction principle for mathitT. We develop enough syntax and semantics to account for this high-level style of programming in dependent type theory. We close with the development of a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is ipso facto a proof that typechecking is decidable.},
1243+author = {Norell, Ulf},
1130−author = {McBride, Conor and McKinna, James},
1244+file = {:home/edwin/Research/Papers/Mendeley/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
1131−doi = {10.1017/S0956796803004829},
1132−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/Journal of Functional Programming/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
1134−journal = {Journal of Functional Programming},
1135keywords = {Dependent Types},
1245keywords = {Dependent Types},
1136mendeley-tags = {Dependent Types},
1246mendeley-tags = {Dependent Types},
1137−number = {1},
1247+publisher = {Citeseer},
1138−pages = {69--111},
1248+school = {Chalmers University of Technology},
1139−publisher = {Cambridge University Press},
1249+title = {{Towards a practical programming language based on dependent type theory}},
1140−title = {{The view from the left}},
1250+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7934&rep=rep1&type=pdf},
1141−url = {http://www.journals.cambridge.org/abstract_S0956796803004829},
1143−year = {2004}
1251+year = {2007}
1145−@misc{Nodes2012a,
1253+@inproceedings{Brady2011a,
1146−author = {Brooks, Fred},
1254+address = {New York, New York, USA},
1147−doi = {10.1093/epirev/mxr031},
1255+author = {Brady, Edwin},
1148−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
1256+booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},
1149−isbn = {9780321702081},
1257+doi = {10.1145/1929529.1929536},
1150−issn = {1478-6729},
1258+file = {:home/edwin/Research/Papers/Mendeley/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},
1151−pmid = {22215642},
1259+isbn = {9781450304870},
1152−title = {{The Design of Design Chapter 3}}
1260+keywords = {Dependent Types,data description,dependent types},
1261+mendeley-tags = {Dependent Types},
1263+publisher = {ACM Press},
1264+title = {{Idris --- Systems Programming Meets Full Dependent Types}},
1265+url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
1154−@inproceedings{Hancock2000,
1268+@inproceedings{Kimmell2012,
1155−author = {Hancock, Peter and Setzer, Anton},
1269+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},
1156−booktitle = {{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}},
1270+booktitle = {Programming Languages meets Program Verification},
1157−file = {:Users/edwin/Documents/Mendeley Desktop/Hancock, Setzer/{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}/Hancock, Setzer - 2000 - Interactive Programs in Dependent Type Theory.pdf:pdf},
1271+file = {:home/edwin/Research/Papers/Mendeley/Kimmell et al/Kimmell et al. - 2012 - Equational reasoning about programs with general recursion and call-by-value semantics.pdf:pdf},
1158−isbn = {3-540-67895-6},
1272+title = {{Equational reasoning about programs with general recursion and call-by-value semantics}},
1161−title = {{Interactive Programs in Dependent Type Theory}},
1162−url = {http://dl.acm.org/citation.cfm?id=647850.737221},
1273+url = {http://dl.acm.org/citation.cfm?id=2103780},
1163−year = {2000}
1274+year = {2012}
1165@inproceedings{augustsson2008paradise,
1276@inproceedings{augustsson2008paradise,
1166author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
1277author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
1167booktitle = {International Conference on Functional Programming},
1278booktitle = {International Conference on Functional Programming},
1168−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson, Mansell, Sittampalam/International Conference on Functional Programming/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},
1279+file = {:home/edwin/Research/Papers/Mendeley/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},
1169number = {9},
1280number = {9},
1170pages = {225--228},
1281pages = {225--228},
1171publisher = {ACM},
1282publisher = {ACM},
@@ -1174,131 +1285,32 @@ url = {http://dl.acm.org/citation.cfm?id=1411203.1411236},
1174volume = {43},
1285volume = {43},
1175year = {2008}
1286year = {2008}
1177−@misc{Abel1998,
1288+@misc{altenkirch2005dependent,
1178−author = {Abel, Andreas},
1179−booktitle = {Language},
1180−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Language/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
1181−title = {{foetus - Termination Checker for Simple Functional Programs}},
1185−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.},
1186−author = {Jones, Mark P},
1187−journal = {October},
1188−publisher = {Citeseer},
1189−title = {{Typing Haskell in Haskell}},
1190−url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.134.7274&rep=rep1&type=pdf},
1193−@inproceedings{morris2006exploring,
1194−author = {Morris, P. and Altenkirch, T. and McBride, C.},
1289+author = {Altenkirch, T. and McBride, C. and McKinna, J.},
1195−booktitle = {Types for Proofs and Programs},
1290+booktitle = {Manuscript, available online},
1196−file = {:Users/edwin/Documents/Mendeley Desktop/Morris, Altenkirch, McBride/Types for Proofs and Programs/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},
1291+file = {:home/edwin/Research/Papers/Mendeley/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
1197−pages = {252--267},
1292+title = {{Why dependent types matter}},
1198−publisher = {Springer},
1293+url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},
1199−title = {{Exploring the regular tree types}},
1200−url = {http://www.springerlink.com/index/f9p1317716614834.pdf},
1203−@inproceedings{Sheard2005,
1204−address = {New York, New York, USA},
1205−author = {Sheard, Tim},
1206−booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},
1207−doi = {10.1145/1088348.1088356},
1208−file = {:Users/edwin/Documents/Mendeley Desktop/Sheard/Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},
1209−isbn = {159593071X},
1210−keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},
1213−publisher = {ACM Press},
1214−title = {{Putting curry-howard to work}},
1215−url = {http://dl.acm.org/citation.cfm?id=1088348.1088356},
1216year = {2005}
1294year = {2005}
1218−@misc{Interface2012a,
1219−author = {Kreibich, Jay A.},
1220−doi = {10.1093/epirev/mxr031},
1221−file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Unknown/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
1222−isbn = {9781449394592},
1225−title = {{Using SQLite Chapter 7}}
1228−author = {Hunt, Andrew and Thomas, David},
1229−booktitle = {Carcinogenesis},
1230−doi = {10.1093/carcin/bgs054},
1231−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
1232−isbn = {020161622X},
1236−title = {{The Pragmatic Programmer Chapter 3}},
1237−url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
1241−author = {Brooks, Fred},
1242−doi = {10.1093/epirev/mxr031},
1243−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
1244−isbn = {9780321702081},
1247−title = {{The Design of Design Chapter 2}}
1249−@inproceedings{Levitation2010,
1250−author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},
1251−booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},
1252−doi = {10.1145/1932681.1863547},
1253−file = {:Users/edwin/Documents/Mendeley Desktop/Chapman et al/{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},
1254−isbn = {978-1-60558-794-3},
1256−keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},
1257−mendeley-tags = {Dependent Types},
1260−title = {{The gentle art of levitation}},
1261−url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},
1265−@inproceedings{Xi1999,
1296+@inproceedings{augustsson1999exercise,
1266−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.},
1297+author = {Augustsson, L. and Carlsson, M.},
1267−author = {Xi, Hongwei and Pfenning, Frank},
1298+booktitle = {In Workshop on Dependent Types in Programming, Gothenburg},
1268−booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},
1269−doi = {10.1145/292540.292560},
1270−file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},
1271−isbn = {1581130953},
1273−keywords = {Dependent Types},
1299+keywords = {Depe},
1274−mendeley-tags = {Dependent Types},
1300+mendeley-tags = {Depe},
1275−organization = {Carnegie Mellon University},
1277−publisher = {ACM Press},
1301+publisher = {Citeseer},
1278−series = {POPL '99},
1302+title = {{An exercise in dependent types: A well-typed interpreter}},
1279−title = {{Dependent types in practical programming}},
1303+url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2895},
1280−url = {http://portal.acm.org/citation.cfm?doid=292540.292560},
1282year = {1999}
1304year = {1999}
1284−@inproceedings{Brady2003,
1306+@article{Swierstra2011,
1285−author = {Brady, Edwin and McBride, Conor and McKinna, James},
1307+author = {Swierstra, W},
1286−booktitle = {Types for Proofs and Programs {(TYPES 2003)}},
1308+file = {:home/edwin/Research/Papers/Mendeley/Swierstra/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},
1287−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, McBride, McKinna/Types for Proofs and Programs {(TYPES 2003)}/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},
1309+journal = {Journal of Functional Programming},
1288−keywords = {Dependent Types},
1289−mendeley-tags = {Dependent Types},
1290−title = {{Inductive families need not store their indices}},
1291−url = {http://www.springerlink.com/index/WBXJJG717N2W3NU2.pdf},
1294−@inproceedings{fisher2005pads,
1295−author = {Fisher, K. and Gruber, R.},
1296−booktitle = {ACM SIGPLAN Notices},
1297number = {6},
1310number = {6},
1298−pages = {295--304},
1311+pages = {575----583},
1299−publisher = {ACM},
1312+title = {{Sorted: Verifying the Problem of the {Dutch National} Flag in {Agda}}},
1300−title = {{PADS: a domain-specific language for processing ad hoc data}},
1313+url = {http://journals.cambridge.org/abstract_S0956796811000207},
1301−url = {http://dl.acm.org/citation.cfm?id=1065046},
1302−volume = {40},
1314+volume = {21},
1303−year = {2005}
1315+year = {2011}