@@ -1,17 +1,17 @@
11Automatically generated by Mendeley 1.3.1
22Any changes to this file will be lost if it is regenerated by Mendeley.
33
4−@inproceedings{McBride2006,
5−author = {McBride, C and Goguen, H and McKinna, J},
6−booktitle = {Types for Proofs and Programs},
7−title = {{A few constructions on constructors}},
8−url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
9−year = {2006}
4+@inproceedings{gibbons2011modularising,
5+author = {Gibbons, J. and Ko, H.S. and Others},
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},
7+title = {{Modularising inductive families}},
8+url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
9+year = {2011}
1010}
1111@inproceedings{czarnecki2004dsl,
1212author = {Czarnecki, K. and O’Donnell, J. and Striegnitz, J. and Taha, W.},
1313booktitle = {Domain-Specific Program Generation},
14−file = {:Users/edwin/Documents/Mendeley Desktop/Czarnecki et al/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},
14+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},
1515pages = {51--72},
1616publisher = {Springer},
1717title = {{DSL implementation in MetaOCaml, Template Haskell, and C++}},
@@ -20,7 +20,7 @@ year = {2004}
2020}
2121@phdthesis{Brady2005,
2222author = {Brady, Edwin},
23−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
23+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Unknown/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},
2424keywords = {Dependent Types},
2525mendeley-tags = {Dependent Types},
2626school = {University of Durham},
@@ -31,6 +31,7 @@ year = {2005}
3131@inproceedings{Kimmell2012,
3232author = {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},
3333booktitle = {Programming Languages meets Program Verification},
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},
3435title = {{Equational reasoning about programs with general recursion and call-by-value semantics}},
3536url = {http://dl.acm.org/citation.cfm?id=2103780},
3637year = {2012}
@@ -48,7 +49,7 @@ year = {2011}
4849@article{Altenkirch2010a,
4950abstract = {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.},
5051author = {Altenkirch, Thorsten and Mcbride, Conor and Morris, Peter},
51−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Mcbride, Morris/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
52+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Mcbride, Morris/Citeseer/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},
5253journal = {Citeseer},
5354publisher = {Citeseer},
5455title = {{Generic Programming with Dependent Types}},
@@ -57,7 +58,7 @@ year = {2010}
5758}
5859@article{fisher2006next,
5960author = {Fisher, K. and Mandelbaum, Y. and Walker, D.},
60−file = {:Users/edwin/Documents/Mendeley Desktop/Fisher, Mandelbaum, Walker/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},
61+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},
6162journal = {Journal of the ACM},
6263number = {2},
6364pages = {1--51},
@@ -70,7 +71,7 @@ year = {2010}
7071@misc{The2012b,
7172author = {Brooks, Fred},
7273doi = {10.1093/epirev/mxr031},
73−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
74+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},
7475isbn = {9780321702081},
7576issn = {1478-6729},
7677pmid = {22215642},
@@ -78,7 +79,7 @@ title = {{The Design of Design Chapter 1}}
7879}
7980@article{Chapman2005epigram,
8081author = {Chapman, James and Altenkirch, Thorsten and McBride, Conor},
81−file = {:Users/edwin/Documents/Mendeley Desktop/Chapman, Altenkirch, McBride/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},
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},
8283journal = {Trends in Functional Programming},
8384publisher = {Intellect Books},
8485title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
@@ -90,7 +91,7 @@ abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your pe
9091address = {London},
9192author = {{The Mendeley Support Team}},
9293booktitle = {Mendeley Desktop},
93−file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
94+file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/Mendeley Desktop/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
9495keywords = {Mendeley,how-to,user manual},
9596pages = {1--16},
9697publisher = {Mendeley Ltd.},
@@ -100,14 +101,14 @@ year = {2011}
100101}
101102@phdthesis{Okasaki1996,
102103author = {Okasaki, Chris},
103−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
104+file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Unknown/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},
104105school = {Carnegie Mellon University},
105106title = {{Purely Functional Data Structures}},
106107year = {1996}
107108}
108109@article{mcbride2008functional,
109110author = {McBride, C. and Paterson, R.},
110−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
111+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Journal of functional programming/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},
111112journal = {Journal of functional programming},
112113number = {1},
113114pages = {1--13},
@@ -120,7 +121,7 @@ year = {2008}
120121@inproceedings{madhavapeddy2007melange,
121122author = {Madhavapeddy, A. and Ho, A. and Deegan, T. and Scott, D. and Sohan, R.},
122123booktitle = {ACM SIGOPS Operating Systems Review},
123−file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},
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},
124125number = {3},
125126pages = {101--114},
126127publisher = {ACM},
@@ -132,7 +133,7 @@ year = {2007}
132133@inproceedings{lempsink2009type,
133134author = {Lempsink, E. and Leather, S. and L\"{o}h, A.},
134135booktitle = {Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming},
135−file = {:Users/edwin/Documents/Mendeley Desktop/Lempsink, Leather, L\"{o}h/Lempsink, Leather, L\"{o}h - 2009 - Type-safe diff for families of datatypes.pdf:pdf},
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},
136137pages = {61--72},
137138publisher = {ACM},
138139title = {{Type-safe diff for families of datatypes}},
@@ -143,7 +144,7 @@ year = {2009}
143144author = {Hunt, Andrew and Thomas, David},
144145booktitle = {Carcinogenesis},
145146doi = {10.1093/carcin/bgs054},
146−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
147+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
147148isbn = {020161622X},
148149issn = {1460-2180},
149150number = {3},
@@ -155,7 +156,7 @@ volume = {33}
155156@inproceedings{stump2010resource,
156157author = {Stump, A. and Austin, E.},
157158booktitle = {Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification},
158−file = {:Users/edwin/Documents/Mendeley Desktop/Stump, Austin/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},
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},
159160pages = {27--38},
160161publisher = {ACM},
161162title = {{Resource typing in Guru}},
@@ -164,7 +165,7 @@ year = {2010}
164165}
165166@article{mcbride2010ornamental,
166167author = {McBride, Conor},
167−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
168+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Journal of Functional Programming/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},
168169journal = {Journal of Functional Programming},
169170title = {{Ornamental algebras, algebraic ornaments}},
170171url = {http://personal.cis.strath.ac.uk/$\sim$conor/pub/OAAO/Ornament.pdf},
@@ -172,7 +173,7 @@ year = {2010}
172173}
173174@article{Swierstra2011,
174175author = {Swierstra, W},
175−file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},
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},
176177journal = {Journal of Functional Programming},
177178number = {6},
178179pages = {575----583},
@@ -183,7 +184,8 @@ year = {2011}
183184}
184185@article{McBride2002,
185186author = {McBride, C},
186−journal = {Types for proofs and programs},
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})},
187189title = {{Elimination with a Motive}},
188190url = {http://www.springerlink.com/index/vbpg19305t46f6dm.pdf},
189191year = {2000}
@@ -192,7 +194,7 @@ year = {2000}
192194abstract = {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.},
193195author = {Xi, Hongwei and Pfenning, Frank},
194196doi = {10.1145/277652.277732},
195−file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},
197+file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/ACM Sigplan Notices/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},
196198isbn = {0897919874},
197199issn = {03621340},
198200journal = {ACM Sigplan Notices},
@@ -209,7 +211,7 @@ year = {1998}
209211}
210212@misc{idristutorial,
211213author = {Brady, Edwin},
212−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
214+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Unknown/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
213215title = {{Programming in Idris : a tutorial}},
214216url = {http://idris-lang.org/tutorial},
215217year = {2012}
@@ -219,7 +221,7 @@ abstract = {We describe an axiomatic extension to the Coq proof assistant, that
219221author = {{Nanevski A A Morrisett}, G B Shinnar A B Govereau P B Birkedal L C},
220222booktitle = {International Conference on Functional Programming},
221223doi = {10.1145/1411204.1411237},
222−file = {:Users/edwin/Documents/Mendeley Desktop/Nanevski A A Morrisett/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},
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},
223225isbn = {9781595939197},
224226issn = {15232867},
225227keywords = {Dependent Types},
@@ -234,7 +236,7 @@ year = {2008}
234236@misc{Brady2012c,
235237author = {Brooks, Fred},
236238doi = {10.1093/epirev/mxr031},
237−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},
239+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},
238240isbn = {9780321702081},
239241issn = {1478-6729},
240242number = {1},
@@ -246,7 +248,7 @@ volume = {34}
246248@inproceedings{ko2011modularising,
247249author = {Ko, H.S. and Gibbons, J.},
248250booktitle = {Proceedings of the seventh ACM SIGPLAN workshop on Generic programming},
249−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
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},
250252pages = {13--24},
251253publisher = {ACM},
252254title = {{Modularising inductive families}},
@@ -257,7 +259,7 @@ year = {2011}
257259author = {Fowler, Martin},
258260booktitle = {Carcinogenesis},
259261doi = {10.1093/carcin/bgs054},
260−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
262+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Carcinogenesis/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
261263isbn = {9780132107549},
262264issn = {1460-2180},
263265number = {3},
@@ -268,7 +270,7 @@ volume = {33}
268270}
269271@article{marlow2006making,
270272author = {Marlow, S. and {Peyton Jones}, S.},
271−file = {:Users/edwin/Documents/Mendeley Desktop/Marlow, Peyton Jones/Marlow, Peyton Jones - 2006 - Making a fast curry pushenter vs. evalapply for higher-order languages.pdf:pdf},
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},
272274journal = {Journal of Functional Programming},
273275number = {4-5},
274276pages = {415--449},
@@ -297,7 +299,7 @@ year = {2007}
297299@article{Abel2010,
298300abstract = {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.},
299301author = {Abel, Andreas},
300−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
302+file = {:Users/edwin/Documents/Mendeley Desktop/Abel/EPTCS/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},
301303journal = {EPTCS},
302304pages = {1--15},
303305title = {{MiniAgda: Integrating Sized and Dependent Types}},
@@ -310,7 +312,7 @@ abstract = {This paper suggests that input and output are basic primitives of pr
310312author = {Hoare, C A R},
311313doi = {10.1016/0167-6423(87)90028-1},
312314editor = {McKeag, R M and Macnaghten, A M},
313−file = {:Users/edwin/Documents/Mendeley Desktop/Hoare/Hoare - 1978 - Communicating sequential processes.pdf:pdf},
315+file = {:Users/edwin/Documents/Mendeley Desktop/Hoare/Communications of the ACM/Hoare - 1978 - Communicating sequential processes.pdf:pdf},
314316isbn = {0131532715},
315317issn = {01676423},
316318journal = {Communications of the ACM},
@@ -326,7 +328,7 @@ year = {1978}
326328}
327329@book{Bird2010,
328330author = {Bird, Richard},
329−file = {:Users/edwin/Documents/Mendeley Desktop/Bird/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
331+file = {:Users/edwin/Documents/Mendeley Desktop/Bird/Unknown/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},
330332isbn = {9780521513388},
331333title = {{Pearls of Functional Algorithm Design}},
332334year = {2010}
@@ -334,7 +336,7 @@ year = {2010}
334336@inproceedings{oury2008power,
335337author = {Oury, N. and Swierstra, W.},
336338booktitle = {International Conference on Functional Programming},
337−file = {:Users/edwin/Documents/Mendeley Desktop/Oury, Swierstra/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
339+file = {:Users/edwin/Documents/Mendeley Desktop/Oury, Swierstra/International Conference on Functional Programming/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},
338340keywords = {Dependent Types},
339341mendeley-tags = {Dependent Types},
340342number = {9},
@@ -348,7 +350,7 @@ year = {2008}
348350@inproceedings{madhavapeddy2010turning,
349351author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
350352booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
351−file = {:Users/edwin/Documents/Mendeley Desktop/Madhavapeddy et al/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},
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},
352354publisher = {USENIX Association},
353355title = {{Turning down the LAMP: software specialisation for the cloud}},
354356url = {http://dl.acm.org/citation.cfm?id=1863114},
@@ -365,7 +367,7 @@ year = {1987}
365367author = {Pa\v{s}alic, Emir and Taha, Walid and Sheard, Tim},
366368booktitle = {International Conference on Functional Programming},
367369doi = {10.1145/583852.581499},
368−file = {:Users/edwin/Documents/Mendeley Desktop/Pa\v{s}alic, Taha, Sheard/Pa\v{s}alic, Taha, Sheard - 2002 - Tagless staged interpreters for typed languages.pdf:pdf},
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},
369371isbn = {1-58113-487-8},
370372issn = {03621340},
371373keywords = {calculus of constructions,definitional interpreters,domain-specific languages,multi-stage programming},
@@ -380,7 +382,7 @@ year = {2002}
380382@inproceedings{Brady2010,
381383author = {Brady, Edwin and Hammond, Kevin},
382384booktitle = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming},
383−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2010 - Scrapping your inefficient engine using partial evaluation to improve domain-specific language implementation.pdf:pdf},
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},
384386isbn = {9781605587943},
385387keywords = {Dependent Types,code generation gives,contrast,dependent types,efficient,harder,however,implementation,likely efficient,ness interpreter,partial evaluation,resulting implementation,un,verify its correctness},
386388mendeley-tags = {Dependent Types},
@@ -393,14 +395,14 @@ year = {2010}
393395@inproceedings{Fournet2011,
394396author = {Fournet, Cedric and Bhargavan, Karthikeyan and Gordon, Andrew D},
395397booktitle = {Foundations of security analysis and design {VI}},
396−file = {:Users/edwin/Documents/Mendeley Desktop/Fournet, Bhargavan, Gordon/Fournet, Bhargavan, Gordon - 2010 - Cryptographic verification by typing for a sample protocol implementation.pdf:pdf},
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},
397399title = {{Cryptographic verification by typing for a sample protocol implementation}},
398400url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
399401year = {2010}
400402}
401403@article{landin1966next,
402404author = {Landin, P.J.},
403−file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
405+file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Communications of the ACM/Landin - 1966 - The next 700 programming languages.pdf:pdf},
404406journal = {Communications of the ACM},
405407number = {3},
406408pages = {157--166},
@@ -424,7 +426,7 @@ year = {2010}
424426@article{Haskell2012a,
425427author = {Biancuzzi, F and Warden, S},
426428doi = {10.1093/epirev/mxr031},
427−file = {:Users/edwin/Documents/Mendeley Desktop/Biancuzzi, Warden/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
429+file = {:Users/edwin/Documents/Mendeley Desktop/Biancuzzi, Warden/Unknown/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},
428430isbn = {9780596801670},
429431issn = {1478-6729},
430432pmid = {22215642},
@@ -434,7 +436,7 @@ title = {{Masterminds of Programming Chapter 8}}
434436author = {Hunt, Andrew and Thomas, David},
435437booktitle = {Carcinogenesis},
436438doi = {10.1093/carcin/bgs054},
437−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
439+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
438440isbn = {020161622X},
439441issn = {1460-2180},
440442number = {3},
@@ -445,7 +447,7 @@ volume = {33}
445447}
446448@article{McBride2007,
447449author = {McBride, Conor and Paterson, Ross},
448−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
450+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, Paterson/Journal of functional programming/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},
449451journal = {Journal of functional programming},
450452title = {{Applicative programming with effects}},
451453url = {http://journals.cambridge.org/abstract_S0956796807006326},
@@ -457,7 +459,7 @@ author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres a
457459booktitle = {{FLOPS 2010}},
458460doi = {10.1007/978-3-642-12251-4_5},
459461editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ\'{a}n},
460−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch et al/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
462+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch et al/{FLOPS 2010}/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},
461463isbn = {9783642122507},
462464pages = {40----55},
463465publisher = {Springer Berlin Heidelberg},
@@ -481,16 +483,27 @@ url = {http://www.springerlink.com/index/96j7v5vn8tyebeky.pdf},
481483volume = {3622},
482484year = {2005}
483485}
486+@article{Huet1997,
487+author = {Huet, G},
488+file = {:Users/edwin/Documents/Mendeley Desktop/Huet/{Journal of Functional Programming}/Huet - 1997 - The zipper.pdf:pdf},
489+journal = {{Journal of Functional Programming}},
490+number = {5},
491+pages = {549----554},
492+title = {{The zipper}},
493+url = {http://journals.cambridge.org/abstract_S0956796897002864},
494+volume = {7},
495+year = {1997}
496+}
484497@misc{Bloat,
485498author = {Brooks, Fred},
486−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},
499+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},
487500isbn = {9780321702081},
488501title = {{The Design of Design Chapter 4}}
489502}
490503@misc{Protocols2012a,
491504author = {Anderson, Ross},
492505doi = {10.1093/epirev/mxr031},
493−file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
506+file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Unknown/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},
494507isbn = {9780470068526},
495508issn = {1478-6729},
496509pmid = {22215642},
@@ -501,7 +514,7 @@ abstract = {Cayenne is a Haskell-like language. The main difference between Hask
501514author = {Augustsson, Lennart},
502515booktitle = {International Conference on Functional Programming},
503516doi = {10.1097/MEG.0b013e328342f213},
504−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},
517+file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson/International Conference on Functional Programming/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},
505518issn = {14735687},
506519keywords = {Depe,Dependent Types},
507520mendeley-tags = {Depe,Dependent Types},
@@ -517,13 +530,13 @@ year = {1998}
517530@book{Hunt,
518531author = {Hunt, Andrew and Thomas, David},
519532booktitle = {Design},
520−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
533+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Design/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
521534isbn = {020161622X},
522535title = {{The Pragmatic Programmer Chapter 4}}
523536}
524537@article{burrows1990,
525538author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
526−file = {:Users/edwin/Documents/Mendeley Desktop/Burrows, Abadi, Needham/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},
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},
527540journal = {ACM Transactions on Computer Systems},
528541pages = {18----36},
529542title = {{A logic of authentication}},
@@ -545,7 +558,7 @@ address = {New York, New York, USA},
545558author = {Brady, Edwin},
546559booktitle = {Proceedings of the 5th {ACM} workshop on Programming languages meets program verification - {PLPV} '11},
547560doi = {10.1145/1929529.1929536},
548−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},
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},
549562isbn = {9781450304870},
550563keywords = {Dependent Types,data description,dependent types},
551564mendeley-tags = {Dependent Types},
@@ -555,18 +568,11 @@ title = {{Idris --- Systems Programming Meets Full Dependent Types}},
555568url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
556569year = {2011}
557570}
558−@inproceedings{gibbons2011modularising,
559−author = {Gibbons, J. and Ko, H.S. and Others},
560−file = {:Users/edwin/Documents/Mendeley Desktop/Ko, Gibbons/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},
561−title = {{Modularising inductive families}},
562−url = {http://www.cs.ox.ac.uk/publications/publication5008-abstract.html},
563−year = {2011}
564−}
565571@book{An2012,
566572author = {Fowler, Martin},
567573booktitle = {Carcinogenesis},
568574doi = {10.1093/carcin/bgs054},
569−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
575+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Carcinogenesis/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
570576isbn = {9780132107549},
571577issn = {1460-2180},
572578number = {3},
@@ -578,7 +584,7 @@ volume = {33}
578584@inproceedings{coquand1986analysis,
579585author = {Coquand, T.},
580586booktitle = {{Proceedings of the First IEEE Symposium on Logic in Computer Science}},
581−file = {:Users/edwin/Documents/Mendeley Desktop/Coquand/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},
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},
582588pages = {227----246},
583589title = {{An analysis of Girard's paradox}},
584590url = {http://hal.inria.fr/docs/00/07/60/23/PDF/RR-0531.pdf},
@@ -586,7 +592,7 @@ year = {1986}
586592}
587593@misc{altenkirch2008nσ,
588594author = {Altenkirch, T. and Oury, N.},
589−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Oury/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
595+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, Oury/Unknown/Altenkirch, Oury - 2008 - $Pi$$Sigma$ A Core Language for Dependently Typed Programming.pdf:pdf},
590596title = {{$\Pi$$\Sigma$: A Core Language for Dependently Typed Programming}},
591597url = {http://verse.aasemoon.com/images/6/6f/PiSigma.pdf},
592598year = {2008}
@@ -594,7 +600,7 @@ year = {2008}
594600@inproceedings{barras2008implicit,
595601author = {Barras, B. and Bernardo, B.},
596602booktitle = {Foundations of Software Science and Computational Structures},
597−file = {:Users/edwin/Documents/Mendeley Desktop/Barras, Bernardo/Barras, Bernardo - 2008 - The implicit calculus of constructions as a programming language with dependent types.pdf:pdf},
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},
598604pages = {365--379},
599605publisher = {Springer},
600606title = {{The implicit calculus of constructions as a programming language with dependent types}},
@@ -605,7 +611,7 @@ year = {2008}
605611author = {Hunt, Andrew and Thomas, David},
606612booktitle = {Carcinogenesis},
607613doi = {10.1093/carcin/bgs054},
608−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
614+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
609615isbn = {020161622X},
610616issn = {1460-2180},
611617number = {3},
@@ -617,7 +623,7 @@ volume = {33}
617623@inproceedings{bradyresource,
618624author = {Brady, Edwin and Hammond, Kevin},
619625booktitle = {Practical Applications of Declarative Languages ({PADL} 2012)},
620−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.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},
621627pages = {242----257},
622628title = {{Resource-safe Systems Programming with Embedded Domain Specific Languages}},
623629url = {http://www.cs.st-andrews.ac.uk/$\sim$eb/drafts/dsl-idris.pdf},
@@ -632,7 +638,7 @@ year = {1994}
632638}
633639@phdthesis{norell2007thesis,
634640author = {Norell, Ulf},
635−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
641+file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Unknown/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},
636642keywords = {Dependent Types},
637643mendeley-tags = {Dependent Types},
638644publisher = {Citeseer},
@@ -644,7 +650,7 @@ year = {2007}
644650@inproceedings{Brady2006b,
645651author = {Brady, Edwin},
646652booktitle = {Implementation and Application of Functional Languages ({IFL}'06)},
647−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
653+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Implementation and Application of Functional Languages ({IFL}'06)/Brady - 2006 - Ivor, a proof engine.pdf:pdf},
648654isbn = {978-3-540-74129-9},
649655month = sep,
650656pages = {145----162},
@@ -655,7 +661,7 @@ year = {2006}
655661@inproceedings{chlipala2010ur,
656662author = {Chlipala, Adam},
657663booktitle = {ACM SIGPLAN Notices},
658−file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
664+file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/ACM SIGPLAN Notices/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},
659665number = {6},
660666pages = {122--133},
661667publisher = {ACM},
@@ -667,12 +673,19 @@ year = {2010}
667673@misc{Abadi1997,
668674author = {Abadi, Martin and Gordon, Andrew D},
669675booktitle = {4TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY},
670−file = {:Users/edwin/Documents/Mendeley Desktop/Abadi, Gordon/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},
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},
671677pages = {36 -- 47},
672678title = {{A calculus for cryptographic protocols: The spi calculus}},
673679url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.2176},
674680year = {1997}
675681}
682+@inproceedings{McBride2006,
683+author = {McBride, C and Goguen, H and McKinna, J},
684+booktitle = {Types for Proofs and Programs {(TYPES 2006)}},
685+title = {{A few constructions on constructors}},
686+url = {http://www.springerlink.com/index/P4863U0M41396254.pdf},
687+year = {2006}
688+}
676689@article{Jones2003,
677690abstract = {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.},
678691author = {Jones, Simon Peyton},
@@ -705,7 +718,7 @@ year = {2011}
705718@misc{Attacks2012a,
706719author = {Anderson, Ross},
707720doi = {10.1093/epirev/mxr031},
708−file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},
721+file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Unknown/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},
709722isbn = {9780470068526},
710723issn = {1478-6729},
711724number = {1},
@@ -717,7 +730,7 @@ volume = {34}
717730@inproceedings{l,
718731author = {L\"{a}mmel, R. and Jones, S.P.},
719732booktitle = {ACM SIGPLAN Notices},
720−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{a}mmel, Jones/L\"{a}mmel, Jones - 2003 - Scrap your boilerplate a practical design pattern for generic programming.pdf:pdf},
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},
721734number = {3},
722735pages = {26--37},
723736publisher = {ACM},
@@ -726,9 +739,19 @@ url = {http://dl.acm.org/citation.cfm?id=640136.604179},
726739volume = {38},
727740year = {2003}
728741}
742+@inproceedings{Delahaye2000,
743+author = {Delahaye, D},
744+booktitle = {Logic for Programming and Automated Reasoning},
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},
746+pages = {85----95},
747+publisher = {Springer},
748+title = {{A tactic language for the system Coq}},
749+url = {http://www.springerlink.com/index/EFQAH8J88K42VN8T.pdf},
750+year = {2000}
751+}
729752@misc{pollack1997believe,
730753author = {Pollack, R.},
731−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
754+file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Unknown/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},
732755title = {{How to believe a machine-checked proof}},
733756url = {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},
734757year = {1997}
@@ -743,7 +766,7 @@ year = {2004}
743766@inproceedings{brady2011epic,
744767author = {Brady, Edwin},
745768booktitle = {Trends in Functional Programming ({TFP}’11)},
746−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},
769+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Trends in Functional Programming ({TFP}’11)/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},
747770title = {{Epic --- A Library for Generating Compilers}},
748771url = {http://scholar.google.co.uk/scholar?cites=2588300990390214449&as_sdt=2005&sciodt=0,5&hl=en#1},
749772year = {2011}
@@ -762,7 +785,7 @@ year = {1994}
762785@inproceedings{McBride2004b,
763786author = {McBride, Conor and McKinna, James},
764787booktitle = {Haskell Workshop},
765−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},
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},
766789title = {{I am not a number : I am a free variable}},
767790year = {2004}
768791}
@@ -771,7 +794,7 @@ abstract = {The use of monads to structure functional programs is described. Mon
771794author = {Wadler, Philip},
772795doi = {10.1007/3-540-59451-5_2},
773796editor = {Jeuring, Johan and Meijer, Erik},
774−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 2001 - Monads for functional programming.pdf:pdf},
797+file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Advanced Functional Programming/Wadler - 2001 - Monads for functional programming.pdf:pdf},
775798isbn = {3540594515},
776799issn = {03029743},
777800journal = {Advanced Functional Programming},
@@ -797,7 +820,7 @@ year = {1997}
797820}
798821@article{loh2010tutorial,
799822author = {L\"{o}h, A. and McBride, C. and Swierstra, W.},
800−file = {:Users/edwin/Documents/Mendeley Desktop/L\"{o}h, McBride, Swierstra/L\"{o}h, McBride, Swierstra - 2010 - A tutorial implementation of a dependently typed lambda calculus.pdf:pdf},
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},
801824journal = {Fundamenta Informaticae},
802825number = {2},
803826pages = {177--207},
@@ -811,7 +834,7 @@ year = {2010}
811834author = {Hunt, Andrew and Thomas, David},
812835booktitle = {Carcinogenesis},
813836doi = {10.1093/carcin/bgs054},
814−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
837+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
815838isbn = {020161622X},
816839issn = {1460-2180},
817840number = {3},
@@ -822,8 +845,8 @@ volume = {33}
822845}
823846@inproceedings{pollack1990implicit,
824847author = {Pollack, R.},
825−booktitle = {Informal Proceedings of First Workshop on Logical Frameworks, Antibes},
826−file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},
848+booktitle = {{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}},
849+file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/{Informal Proceedings of First Workshop on Logical Frameworks, Antibes}/Pollack - 1990 - Implicit syntax.pdf:pdf},
827850publisher = {Citeseer},
828851title = {{Implicit syntax}},
829852url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
@@ -831,7 +854,7 @@ year = {1990}
831854}
832855@article{gordon2003authenticity,
833856author = {Gordon, A.D. and Jeffrey, A.},
834−file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},
857+file = {:Users/edwin/Documents/Mendeley Desktop/Gordon, Jeffrey/Journal of computer security/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},
835858journal = {Journal of computer security},
836859number = {4},
837860pages = {451--520},
@@ -846,7 +869,7 @@ abstract = {From the type of a polymorphic function we can derive a theorem that
846869author = {Wadler, Philip},
847870booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture},
848871doi = {10.1145/99370.99404},
849−file = {:Users/edwin/Documents/Mendeley Desktop/Wadler/Wadler - 1989 - Theorems for free!.pdf:pdf},
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},
850873isbn = {0897913280},
851874number = {June},
852875pages = {347--359},
@@ -875,7 +898,7 @@ year = {1985}
875898@inproceedings{Brady2005a,
876899author = {Brady, E and Hammond, K},
877900booktitle = {Implementation and Application of Functional \ldots},
878−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},
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},
879902keywords = {Dependent Types},
880903mendeley-tags = {Dependent Types},
881904title = {{A dependently typed framework for static analysis of program execution costs}},
@@ -884,7 +907,7 @@ year = {2005}
884907}
885908@article{Vytiniotis2011,
886909author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},
887−file = {:Users/edwin/Downloads/S0956796811000098a.pdf:pdf},
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},
888911journal = {{Journal of Functional Programming}},
889912number = {4--5},
890913pages = {333----412},
@@ -906,7 +929,7 @@ year = {2000}
906929}
907930@article{Miller1992,
908931author = {Miller, Dale},
909−file = {:Users/edwin/Documents/Papers/Miller/1992 Miller-Unification under a mixed prefix.pdf:pdf},
932+file = {:Users/edwin/Documents/Mendeley Desktop/Miller/Journal of Symbolic Computation/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},
910933journal = {Journal of Symbolic Computation},
911934title = {{Unification under a mixed prefix}},
912935url = {http://www.sciencedirect.com/science/article/pii/074771719290011R},
@@ -915,7 +938,7 @@ year = {1992}
915938@inproceedings{norell2009dependently,
916939author = {Norell, Ulf},
917940booktitle = {Advanced Functional Programming},
918−file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},
941+file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Advanced Functional Programming/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},
919942keywords = {Dependent Types},
920943mendeley-tags = {Dependent Types},
921944pages = {230--266},
@@ -930,7 +953,7 @@ author = {Hughes, J},
930953chapter = {2},
931954doi = {10.1093/comjnl/32.2.98},
932955editor = {Turner, David A},
933−file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
956+file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/The Computer Journal/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},
934957institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},
935958isbn = {0201172364},
936959issn = {00104620},
@@ -945,7 +968,7 @@ year = {1989}
945968}
946969@article{Steiner1988,
947970author = {Steiner, JG},
948−file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
971+file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Proc. Winter USENIX Conference/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
949972journal = {Proc. Winter USENIX Conference},
950973title = {{Kerberos: An authentication service for open network systems}},
951974url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},
@@ -953,7 +976,7 @@ year = {1988}
953976}
954977@phdthesis{McBride1999,
955978author = {McBride, Conor},
956−file = {:Users/edwin/Documents/Mendeley Desktop/McBride/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
979+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Unknown/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},
957980keywords = {Dependent Types},
958981mendeley-tags = {Dependent Types},
959982school = {University of Edinburgh},
@@ -983,7 +1006,7 @@ year = {2004}
9831006@inproceedings{Sculthorpe2009,
9841007author = {Sculthorpe, Neil and Nilsson, Henrik},
9851008booktitle = {International Conference on Functional Programming ({ICFP} '09)},
986−file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},
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},
9871010title = {{Safe functional reactive programming through dependent types}},
9881011url = {http://dl.acm.org/citation.cfm?id=1596558},
9891012year = {2009}
@@ -993,7 +1016,7 @@ abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your pe
9931016address = {London},
9941017author = {{The Mendeley Support Team}},
9951018booktitle = {Mendeley Desktop},
996−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
1019+file = {:Users/edwin/Documents/Mendeley Desktop/The Mendeley Support Team/Mendeley Desktop/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},
9971020keywords = {Mendeley,how-to,user manual},
9981021pages = {1--16},
9991022publisher = {Mendeley Ltd.},
@@ -1012,7 +1035,7 @@ year = {2011}
10121035}
10131036@misc{dagand2011transporting,
10141037author = {Dagand, Pierre-Evariste and McBride, Conor},
1015−file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
1038+file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Unknown/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},
10161039title = {{Transporting Functions across Ornaments}},
10171040url = {http://personal.cis.strath.ac.uk/$\sim$dagand/stuffs/paper-2011-patch/paper.pdf},
10181041year = {2011}
@@ -1020,7 +1043,7 @@ year = {2011}
10201043@book{Fowler,
10211044author = {Fowler, Martin},
10221045booktitle = {Language},
1023−file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
1046+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Language/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
10241047isbn = {9780132107549},
10251048title = {{Domain Specific Languages Chapter 2}}
10261049}
@@ -1029,7 +1052,7 @@ abstract = {In these lecture notes we give an introduction to functional program
10291052author = {Bove, Ana and Dybjer, Peter},
10301053booktitle = {Notes},
10311054doi = {10.1007/978-3-642-03153-3_2},
1032−file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},
1055+file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Notes/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},
10331056number = {February},
10341057pages = {57--99},
10351058publisher = {Springer},
@@ -1040,7 +1063,7 @@ year = {2008}
10401063}
10411064@article{Okasaki1993,
10421065author = {Okasaki, Chris},
1043−file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
1066+file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Journal of functional programming/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},
10441067journal = {Journal of functional programming},
10451068title = {{Red-Black Trees in A Functional Setting}},
10461069year = {1993}
@@ -1048,7 +1071,7 @@ year = {1993}
10481071@inproceedings{pj2006gadts,
10491072author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
10501073booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
1051−file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
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},
10521075number = {9},
10531076pages = {50--61},
10541077publisher = {ACM},
@@ -1060,7 +1083,7 @@ year = {2006}
10601083@misc{altenkirch2005dependent,
10611084author = {Altenkirch, T. and McBride, C. and McKinna, J.},
10621085booktitle = {Manuscript, available online},
1063−file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
1086+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Manuscript, available online/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},
10641087title = {{Why dependent types matter}},
10651088url = {http://www.cs.nott.ac.uk/$\sim$txa/talks/splst11.pdf},
10661089year = {2005}
@@ -1068,7 +1091,7 @@ year = {2005}
10681091@misc{The2012c,
10691092author = {Robbins, A and Hannah, E and Lamb, L},
10701093doi = {10.1093/epirev/mxr031},
1071−file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
1094+file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Unknown/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},
10721095isbn = {9780596529833},
10731096issn = {1478-6729},
10741097pmid = {22215642},
@@ -1077,14 +1100,14 @@ title = {{Learning the vi and Vim Editors}}
10771100@misc{Resolution2012a,
10781101author = {Fall, Kevin R and Stevens, W. Richard},
10791102doi = {10.1093/epirev/mxr031},
1080−file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},
1103+file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/Unknown/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},
10811104issn = {1478-6729},
10821105pmid = {22215642},
10831106title = {{TCP/IP Illustrated Volume 1 Chapter 11}}
10841107}
10851108@article{Brady2006a,
10861109author = {Brady, E and Hammond, K},
1087−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},
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},
10881111journal = {\ldots of the 5th international conference on \ldots},
10891112keywords = {Dependent Types},
10901113mendeley-tags = {Dependent Types},
@@ -1095,7 +1118,7 @@ year = {2006}
10951118@inproceedings{swierstra2007beauty,
10961119author = {Swierstra, W. and Altenkirch, T.},
10971120booktitle = {Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
1098−file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra, Altenkirch/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},
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},
10991122pages = {25--36},
11001123publisher = {ACM},
11011124title = {{Beauty in the beast}},
@@ -1106,7 +1129,7 @@ year = {2007}
11061129abstract = {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.},
11071130author = {McBride, Conor and McKinna, James},
11081131doi = {10.1017/S0956796803004829},
1109−file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
1132+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/Journal of Functional Programming/McBride, McKinna - 2004 - The view from the left.pdf:pdf},
11101133issn = {09567968},
11111134journal = {Journal of Functional Programming},
11121135keywords = {Dependent Types},
@@ -1122,16 +1145,27 @@ year = {2004}
11221145@misc{Nodes2012a,
11231146author = {Brooks, Fred},
11241147doi = {10.1093/epirev/mxr031},
1125−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
1148+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},
11261149isbn = {9780321702081},
11271150issn = {1478-6729},
11281151pmid = {22215642},
11291152title = {{The Design of Design Chapter 3}}
11301153}
1154+@inproceedings{Hancock2000,
1155+author = {Hancock, Peter and Setzer, Anton},
1156+booktitle = {{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}},
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},
1158+isbn = {3-540-67895-6},
1159+month = aug,
1160+pages = {317--331},
1161+title = {{Interactive Programs in Dependent Type Theory}},
1162+url = {http://dl.acm.org/citation.cfm?id=647850.737221},
1163+year = {2000}
1164+}
11311165@inproceedings{augustsson2008paradise,
11321166author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
11331167booktitle = {International Conference on Functional Programming},
1134−file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson, Mansell, Sittampalam/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},
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},
11351169number = {9},
11361170pages = {225--228},
11371171publisher = {ACM},
@@ -1143,7 +1177,7 @@ year = {2008}
11431177@misc{Abel1998,
11441178author = {Abel, Andreas},
11451179booktitle = {Language},
1146−file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
1180+file = {:Users/edwin/Documents/Mendeley Desktop/Abel/Language/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},
11471181title = {{foetus - Termination Checker for Simple Functional Programs}},
11481182year = {1998}
11491183}
@@ -1159,7 +1193,7 @@ year = {1999}
11591193@inproceedings{morris2006exploring,
11601194author = {Morris, P. and Altenkirch, T. and McBride, C.},
11611195booktitle = {Types for Proofs and Programs},
1162−file = {:Users/edwin/Documents/Mendeley Desktop/Morris, Altenkirch, McBride/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},
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},
11631197pages = {252--267},
11641198publisher = {Springer},
11651199title = {{Exploring the regular tree types}},
@@ -1171,7 +1205,7 @@ address = {New York, New York, USA},
11711205author = {Sheard, Tim},
11721206booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},
11731207doi = {10.1145/1088348.1088356},
1174−file = {:Users/edwin/Documents/Mendeley Desktop/Sheard/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},
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},
11751209isbn = {159593071X},
11761210keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},
11771211month = sep,
@@ -1184,7 +1218,7 @@ year = {2005}
11841218@misc{Interface2012a,
11851219author = {Kreibich, Jay A.},
11861220doi = {10.1093/epirev/mxr031},
1187−file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
1221+file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Unknown/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},
11881222isbn = {9781449394592},
11891223issn = {1478-6729},
11901224pmid = {22215642},
@@ -1194,7 +1228,7 @@ title = {{Using SQLite Chapter 7}}
11941228author = {Hunt, Andrew and Thomas, David},
11951229booktitle = {Carcinogenesis},
11961230doi = {10.1093/carcin/bgs054},
1197−file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
1231+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Carcinogenesis/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
11981232isbn = {020161622X},
11991233issn = {1460-2180},
12001234number = {3},
@@ -1206,7 +1240,7 @@ volume = {33}
12061240@misc{Brady2012b,
12071241author = {Brooks, Fred},
12081242doi = {10.1093/epirev/mxr031},
1209−file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
1243+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/Unknown/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},
12101244isbn = {9780321702081},
12111245issn = {1478-6729},
12121246pmid = {22215642},
@@ -1214,16 +1248,15 @@ title = {{The Design of Design Chapter 2}}
12141248}
12151249@inproceedings{Levitation2010,
12161250author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},
1217−booktitle = {ICFP15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)},
1251+booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},
12181252doi = {10.1145/1932681.1863547},
1219−file = {:Users/edwin/Documents/Mendeley Desktop/Chapman et al/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},
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},
12201254isbn = {978-1-60558-794-3},
12211255issn = {03621340},
12221256keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},
12231257mendeley-tags = {Dependent Types},
12241258month = sep,
12251259number = {9},
1226−pages = {3},
12271260title = {{The gentle art of levitation}},
12281261url = {http://dl.acm.org/citation.cfm?id=1932681.1863547},
12291262volume = {45},
@@ -1234,7 +1267,7 @@ abstract = {Note: OCR errors may be found in this Reference List extracted from
12341267author = {Xi, Hongwei and Pfenning, Frank},
12351268booktitle = {Proceedings of the 26th ACM SIGPLANSIGACT symposium on Principles of programming languages POPL 99},
12361269doi = {10.1145/292540.292560},
1237−file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},
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},
12381271isbn = {1581130953},
12391272issn = {07439016},
12401273keywords = {Dependent Types},
@@ -1250,8 +1283,8 @@ year = {1999}
12501283}
12511284@inproceedings{Brady2003,
12521285author = {Brady, Edwin and McBride, Conor and McKinna, James},
1253−booktitle = {Types for Proofs and Programs},
1254−file = {:Users/edwin/Documents/Mendeley Desktop/Brady, McBride, McKinna/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},
1286+booktitle = {Types for Proofs and Programs {(TYPES 2003)}},
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},
12551288keywords = {Dependent Types},
12561289mendeley-tags = {Dependent Types},
12571290title = {{Inductive families need not store their indices}},