8843539 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tinkering with related work

commit8843539c43b7f907d6181eb28ef58093675c5489 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 9 Feb 2013, 11:49 (14 years ago) parent22316d9

3 files changed+217−197

compare with master

unifiedsplit

papers/impl-paper/conclusions.tex+24−13 papers/impl-paper/impldtp.tex+5−4 papers/impl-paper/library.bib+188−180

papers/impl-paper/conclusions.tex+24−13

@@ -4,21 +4,32 @@

55Dependently typed programming languages have becoming more prominent in recent

66years as tools for verifying software correctness, and several experimental

7−languages are being developed, in particular Agda \cite{norell2007thesis}, Epigram

8−\cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.

7+languages are being developed, in particular Agda \cite{norell2007thesis},

8+Epigram \cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.

9+The problem of refining high level syntax to a core type theory also applies

10+to theorem provers based on dependent types such as Coq~\cite{Bertot2004}

11+and Matita~\cite{Asperti2011}.

912

10−[Talk about~\cite{Asperti}, ~\cite{OutsideIn}, ~\cite{Sozeau2008}]

11−

12−An earlier implementation of \Idris{} was built on the \Ivor{} proof engine

13+An earlier implementation of \Idris{} was built on the \Ivor{} proof engine

1314\cite{Brady2006b}. This implementation differed in one important way --- unlike

14−the present implementation, there was limited separation between the type theory

15−and the high level language. The type theory itself supported implicit syntax and

16−unification, with high level constructs such as the \texttt{with} rule implemented

17−directly. Two important disadvantages were found with this approach, however:

18−firstly, the type checker is much more complicated when combined with

19−unification, making it harder to maintain; secondly, adding new high level features

20−requires the type checker to support those features directly. In contrast, elaboration

21−by tactics gives a clean separation between the low level and high level languages.

15+the present implementation, there was limited separation between the type

16+theory and the high level language. The type theory itself supported implicit

17+syntax and unification, with high level constructs such as the \texttt{with}

18+rule implemented directly. Two important disadvantages were found with this

19+approach, however: firstly, the type checker is much more complicated when

20+combined with unification, making it harder to maintain; secondly, adding new

21+high level features requires the type checker to support those features

22+directly. In contrast, elaboration by tactics gives a clean separation between

23+the low level and high level languages.

24+

25+Matita uses a bi-directional refinement algorithm~\cite{Asperti}. This is a

26+type directed approach, maintaining a set of yet to be solved unification

27+problems and relying on a small kernel, similar to the approach we now take

28+with \Idris{}, However, their approach uses refinement rules rather than

29+actics. This leads to good error messages though it is not clear how

30+easy it would be to extend to additional high level language features, unlike

31+the tactic based approach.

32+Similarly, the new GHC type checker~\cite{Vytiniotis2011} \ldots \textbf{TODO}

2233

2334The Agda implementation is based on a type theory with

2435implicit syntax and pattern matching --- Norell gives an algorithm for type checking

papers/impl-paper/impldtp.tex+5−4

@@ -131,10 +131,11 @@ implementation of new high level language constructs.

131131

132132\section*{Acknowledgements}

133133

134−This work was funded by the Scottish Informatics and Computer Science

135−Alliance (SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE).

136−My thanks to Kevin Hammond and Vilhelm Sj\"{o}berg for their comments

137−on an earlier draft of this paper.

134+This work was funded by the Scottish Informatics and Computer Science Alliance

135+(SICSA) and by EU Framework 7 Project No. 248828 (ADVANCE). My thanks to

136+Philip H\"{o}lzenspies, Kevin Hammond and Vilhelm Sj\"{o}berg for their

137+comments on an earlier draft of this paper, and to the anonymous referees for

138+their many insightful and constructive comments.

138139

139140\bibliographystyle{jfp}

140141\bibliography{library.bib}

papers/impl-paper/library.bib+188−180

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

11Automatically generated by Mendeley 1.6

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

4−@inproceedings{Sozeau2008,

5−author = {Sozeau, Matthieu and Oury, Nicolas},

6−booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs 2008})},

7−file = {:Users/edwin/Downloads/10.1.1.175.9556.pdf:pdf},

8−pages = {278----293},

9−title = {{First-Class Type Classes}},

10−year = {2008}

4+@inproceedings{Asperti2011,

5+author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

6+booktitle = {Automated Deduction --- CADE-23},

7+file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/The Matita Interactive Theorem Prover/Asperti et al. - The Matita Interactive Theorem Prover - 2011.pdf:pdf},

8+pages = {64----69},

9+title = {{The Matita Interactive Theorem Prover}},

10+year = {2011}

1111}

1212@inproceedings{McBride2006,

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

@@ -33,7 +33,7 @@ year = {2005}

3333}

3434@article{Okasaki1993,

3535author = {Okasaki, Chris},

36−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Okasaki - 1993 - Red-Black Trees in A Functional Setting.pdf:pdf},

36+file = {:Users/edwin/Documents/Mendeley Desktop/Okasaki/Red-Black Trees in A Functional Setting/Okasaki - Red-Black Trees in A Functional Setting - 1993.pdf:pdf},

3737journal = {Journal of functional programming},

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

3939year = {1993}

@@ -41,7 +41,7 @@ year = {1993}

4141@inproceedings{Hancock2000,

4242author = {Hancock, Peter and Setzer, Anton},

4343booktitle = {{Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic}},

44−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hancock, Setzer - 2000 - Interactive Programs in Dependent Type Theory.pdf:pdf},

44+file = {:Users/edwin/Documents/Mendeley Desktop/Hancock, Setzer/Interactive Programs in Dependent Type Theory/Hancock, Setzer - Interactive Programs in Dependent Type Theory - 2000.pdf:pdf},

4545isbn = {3-540-67895-6},

4646month = aug,

4747pages = {317--331},

@@ -51,7 +51,7 @@ year = {2000}

5151}

5252@article{Turner2004,

5353author = {Turner, D A},

54−file = {:Users/edwin/Downloads/10.1.1.106.364.pdf:pdf},

54+file = {:Users/edwin/Documents/Mendeley Desktop/Turner/Total Functional Programming/Turner - Total Functional Programming - 2004.pdf:pdf},

5555journal = {Journal of Universal Computer Science},

5656keywords = {functional programming},

5757number = {7},

@@ -62,7 +62,7 @@ year = {2004}

6262}

6363@phdthesis{norell2007thesis,

6464author = {Norell, Ulf},

65−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Norell - 2007 - Towards a practical programming language based on dependent type theory.pdf:pdf},

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

6666keywords = {Dependent Types},

6767mendeley-tags = {Dependent Types},

6868publisher = {Citeseer},

@@ -82,7 +82,7 @@ My main concern with the paper is that it reads as if the reader is already fami

8282

8383 },

8484author = {Wu, Nicolas and Magalh\~{a}es, Jos\'{e} Pedro and Bransen, Jeroen and Swierstra, Wouter},

85−file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_14.pdf:pdf},

85+file = {:Users/edwin/Documents/Mendeley Desktop/Wu et al/Pure and Lazy Lambda Mining/Wu et al. - Pure and Lazy Lambda Mining - Unknown.pdf:pdf},

8686title = {{Pure and Lazy Lambda Mining}}

8787}

8888@inproceedings{NanevskiAAMorrisett2008,

@@ -90,7 +90,7 @@ abstract = {We describe an axiomatic extension to the Coq proof assistant, that

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

9191booktitle = {International Conference on Functional Programming},

9292doi = {10.1145/1411204.1411237},

93−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Nanevski A A Morrisett - 2008 - Ynot Dependent types for imperative programs.pdf:pdf},

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

9494isbn = {9781595939197},

9595issn = {15232867},

9696keywords = {Dependent Types},

@@ -138,7 +138,7 @@ p5 "Other terms are rejected" - what does it mean for a term to be rejected? i.e

138138

139139p8 I'm not sure I'd go as far as to say it's "trivial" to show that (1) is a tautology, but I agree it should be easy, if tedious.},

140140author = {Walt, Paul Van Der and Swierstra, Wouter},

141−file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_22.pdf:pdf},

141+file = {:Users/edwin/Documents/Mendeley Desktop/Walt, Swierstra/Engineering Proof by Reflection in Agda/Walt, Swierstra - Engineering Proof by Reflection in Agda - Unknown.pdf:pdf},

142142title = {{Engineering Proof by Reflection in Agda}}

143143}

144144@article{Jones2003,

@@ -157,7 +157,7 @@ year = {2003}

157157@inproceedings{madhavapeddy2007melange,

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

159159booktitle = {ACM SIGOPS Operating Systems Review},

160−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Madhavapeddy et al. - 2007 - Melange creating a functional internet.pdf:pdf},

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

161161number = {3},

162162pages = {101--114},

163163publisher = {ACM},

@@ -169,7 +169,7 @@ year = {2007}

169169@inproceedings{czarnecki2004dsl,

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

171171booktitle = {Domain-Specific Program Generation},

172−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Czarnecki et al. - 2004 - DSL implementation in MetaOCaml, Template Haskell, and C.pdf:pdf},

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

173173pages = {51--72},

174174publisher = {Springer},

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

@@ -181,7 +181,7 @@ abstract = {The use of monads to structure functional programs is described. Mon

181181author = {Wadler, Philip},

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

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

184−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Wadler - 2001 - Monads for functional programming.pdf:pdf},

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

185185isbn = {3540594515},

186186issn = {03029743},

187187journal = {Advanced Functional Programming},

@@ -196,7 +196,7 @@ year = {2001}

196196}

197197@phdthesis{Boquist1999,

198198author = {Boquist, Urban},

199−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Boquist - 1999 - Code optimisation techniques for lazy functional languages.pdf:pdf},

199+file = {:Users/edwin/Documents/Mendeley Desktop/Boquist/Code optimisation techniques for lazy functional languages/Boquist - Code optimisation techniques for lazy functional languages - 1999.pdf:pdf},

200200title = {{Code optimisation techniques for lazy functional languages}},

201201url = {http://mirror.seize.it/papers/Code Optimization Techniques for Lazy Functional Languages.pdf},

202202year = {1999}

@@ -204,7 +204,7 @@ year = {1999}

204204@inproceedings{Taha2003,

205205author = {Taha, Walid and Nielsson, Michael Florentin},

206206booktitle = {Principles of Programming Languages},

207−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Taha, Nielsson - 2003 - Environment Classifiers.pdf:pdf},

207+file = {:Users/edwin/Documents/Mendeley Desktop/Taha, Nielsson/Environment Classifiers/Taha, Nielsson - Environment Classifiers - 2003.pdf:pdf},

208208isbn = {1581136285},

209209keywords = {linear,modal logic,multi-stage programming,temporal logic,type safety,type systems},

210210title = {{Environment Classifiers}},

@@ -213,7 +213,7 @@ year = {2003}

213213@article{Brady2012a,

214214author = {{Peyton Jones}, S.L.},

215215doi = {10.1093/geront/gns026},

216−file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter24BeautifulConcurre.pdf:pdf},

216+file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones/Beautiful Code Chapter 24/Peyton Jones - Beautiful Code Chapter 24 - 2012.pdf:pdf},

217217isbn = {9780596510046},

218218issn = {1758-5341},

219219journal = {The Gerontologist},

@@ -228,7 +228,7 @@ year = {2012}

228228}

229229@article{mcbride2010ornamental,

230230author = {McBride, Conor},

231−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 2010 - Ornamental algebras, algebraic ornaments.pdf:pdf},

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

232232journal = {Journal of Functional Programming},

233233title = {{Ornamental algebras, algebraic ornaments}},

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

@@ -237,7 +237,7 @@ year = {2010}

237237@inproceedings{Gall2012,

238238author = {Gall, Yann Le and Lee, Adam J and Kapdia, Apu},

239239booktitle = {SCMAT},

240−file = {:Users/edwin/Downloads/Papers/p219-legall.pdf:pdf},

240+file = {:Users/edwin/Documents/Mendeley Desktop/Gall, Lee, Kapdia/PlexC A Policy Language for Exposure Control/Gall, Lee, Kapdia - PlexC A Policy Language for Exposure Control - 2012.pdf:pdf},

241241isbn = {9781450312950},

242242keywords = {exposure,policy languages,privacy},

243243pages = {219--228},

@@ -246,14 +246,14 @@ year = {2012}

246246}

247247@article{Campbell-moore,

248248author = {Campbell-moore, Catrin},

249−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Campbell-moore - Unknown - A Computable Infinitary Logic.pdf:pdf},

249+file = {:Users/edwin/Documents/Mendeley Desktop/Campbell-moore/A Computable Infinitary Logic/Campbell-moore - A Computable Infinitary Logic - Unknown.pdf:pdf},

250250pages = {1--10},

251251title = {{A Computable Infinitary Logic}}

252252}

253253@misc{Resolution2012a,

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

255255doi = {10.1093/epirev/mxr031},

256−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fall, Stevens - Unknown - TCPIP Illustrated Volume 1 Chapter 11.pdf:pdf},

256+file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/TCPIP Illustrated Volume 1 Chapter 11/Fall, Stevens - TCPIP Illustrated Volume 1 Chapter 11 - Unknown.pdf:pdf},

257257issn = {1478-6729},

258258pmid = {22215642},

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

@@ -262,7 +262,7 @@ title = {{TCP/IP Illustrated Volume 1 Chapter 11}}

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

263263booktitle = {International Conference on Functional Programming},

264264doi = {10.1145/583852.581499},

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

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

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

267267issn = {03621340},

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

@@ -276,7 +276,7 @@ year = {2002}

276276}

277277@book{Projects,

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

279−file = {:Users/edwin/Downloads/Safari/ThePragmaticProgrammerFromJourneymantoMasterChapter8PragmaticProjects.pdf:pdf},

279+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/The Pragmatic Programmer Chapter 8/Hunt, Thomas - The Pragmatic Programmer Chapter 8 - Unknown.pdf:pdf},

280280isbn = {020161622X},

281281title = {{The Pragmatic Programmer Chapter 8}}

282282}

@@ -285,7 +285,7 @@ abstract = {From the type of a polymorphic function we can derive a theorem that

285285author = {Wadler, Philip},

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

287287doi = {10.1145/99370.99404},

288−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Wadler - 1989 - Theorems for free!.pdf:pdf},

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

289289isbn = {0897913280},

290290number = {June},

291291pages = {347--359},

@@ -298,7 +298,7 @@ year = {1989}

298298@inproceedings{swierstra2007beauty,

299299author = {Swierstra, W. and Altenkirch, T.},

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

301−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Swierstra, Altenkirch - 2007 - Beauty in the beast.pdf:pdf},

301+file = {:Users/edwin/Documents/Mendeley Desktop/Swierstra, Altenkirch/Beauty in the beast/Swierstra, Altenkirch - Beauty in the beast - 2007.pdf:pdf},

302302pages = {25--36},

303303publisher = {ACM},

304304title = {{Beauty in the beast}},

@@ -310,7 +310,7 @@ abstract = {Note: OCR errors may be found in this Reference List extracted from

310310author = {Xi, Hongwei and Pfenning, Frank},

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

312312doi = {10.1145/292540.292560},

313−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Xi, Pfenning - 1999 - Dependent types in practical programming.pdf:pdf},

313+file = {:Users/edwin/Documents/Mendeley Desktop/Xi, Pfenning/Dependent types in practical programming/Xi, Pfenning - Dependent types in practical programming - 1999.pdf:pdf},

314314isbn = {1581130953},

315315issn = {07439016},

316316keywords = {Dependent Types},

@@ -327,7 +327,7 @@ year = {1999}

327327@inproceedings{Kimmell2012,

328328author = {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},

329329booktitle = {Programming Languages meets Program Verification},

330−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Kimmell et al. - 2012 - Equational reasoning about programs with general recursion and call-by-value semantics.pdf:pdf},

330+file = {:Users/edwin/Documents/Mendeley Desktop/Kimmell et al/Equational reasoning about programs with general recursion and call-by-value semantics/Kimmell et al. - Equational reasoning about programs with general recursion and call-by-value semantics - 2012.pdf:pdf},

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

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

333333year = {2012}

@@ -345,7 +345,7 @@ year = {2000}

345345}

346346@article{McBride2007,

347347author = {McBride, Conor and Paterson, Ross},

348−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, Paterson - 2007 - Applicative programming with effects.pdf:pdf},

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

349349journal = {Journal of functional programming},

350350title = {{Applicative programming with effects}},

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

@@ -375,7 +375,7 @@ p9 It seems that the type system is strong enough to support some optimisations

375375

376376In related work, you don't mention any other compilers for dependently typed languages which have to tackle similar problems, though you do mention program extraction for Coq. There is also MAlonzo, which translates Agda to Haskell, and Epic (Trends in Functional Programming), used by Epigram, Agda and Idris, which deals with naming though in a much more limited way than this paper.},

377377author = {Ferreira, Francisco and Monnier, Stefan and Pientka, Brigitte},

378−file = {:Users/edwin/Downloads/Papers/plpv2013_submission_9.pdf:pdf},

378+file = {:Users/edwin/Documents/Mendeley Desktop/Ferreira, Monnier, Pientka/Compiling Contextual Objects Bringing Higher-Order Abstract Syntax to Programmers/Ferreira, Monnier, Pientka - Compiling Contextual Objects Bringing Higher-Order Abstract Syntax to Programmers - 2012.pdf:pdf},

379379keywords = {compilation,contextual objects,pattern matching},

380380title = {{Compiling Contextual Objects Bringing Higher-Order Abstract Syntax to Programmers}},

381381year = {2012}

@@ -383,7 +383,7 @@ year = {2012}

383383@misc{The2012b,

384384author = {Brooks, Fred},

385385doi = {10.1093/epirev/mxr031},

386−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 1.pdf:pdf},

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

387387isbn = {9780321702081},

388388issn = {1478-6729},

389389pmid = {22215642},

@@ -398,7 +398,7 @@ year = {1987}

398398}

399399@article{Miller1992,

400400author = {Miller, Dale},

401−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Miller - 1992 - Unification under a mixed prefix.pdf:pdf},

401+file = {:Users/edwin/Documents/Mendeley Desktop/Miller/Unification under a mixed prefix/Miller - Unification under a mixed prefix - 1992.pdf:pdf},

402402journal = {Journal of Symbolic Computation},

403403title = {{Unification under a mixed prefix}},

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

@@ -408,7 +408,7 @@ year = {1992}

408408author = {Danielsson, Nils Anders},

409409booktitle = {International Conference on Functional Programming},

410410doi = {10.1145/1932681.1863585},

411−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Danielsson - 2010 - Total parser combinators.pdf:pdf},

411+file = {:Users/edwin/Documents/Mendeley Desktop/Danielsson/Total parser combinators/Danielsson - Total parser combinators - 2010.pdf:pdf},

412412isbn = {978-1-60558-794-3},

413413issn = {03621340},

414414keywords = {dependent types,mixed induction and coinduction,parser combinators,productivity,termination},

@@ -435,7 +435,7 @@ address = {New York, New York, USA},

435435author = {Sheard, Tim},

436436booktitle = {Proceedings of the 2005 ACM SIGPLAN workshop on Haskell - Haskell '05},

437437doi = {10.1145/1088348.1088356},

438−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sheard - 2005 - Putting curry-howard to work.pdf:pdf},

438+file = {:Users/edwin/Documents/Mendeley Desktop/Sheard/Putting curry-howard to work/Sheard - Putting curry-howard to work - 2005.pdf:pdf},

439439isbn = {159593071X},

440440keywords = {GADT,curry-howard isomorphism,extensional kind system,haskell,logic},

441441month = sep,

@@ -447,7 +447,7 @@ year = {2005}

447447}

448448@phdthesis{McBride1999,

449449author = {McBride, Conor},

450−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.pdf:pdf},

450+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Dependently typed functional programs and their proofs/McBride - Dependently typed functional programs and their proofs - 1999.pdf:pdf},

451451keywords = {Dependent Types},

452452mendeley-tags = {Dependent Types},

453453school = {University of Edinburgh},

@@ -458,7 +458,7 @@ year = {1999}

458458@article{The2012a,

459459author = {Bentley, Jon},

460460doi = {10.1093/geront/gns026},

461−file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter3TheMostBeautiful.pdf:pdf},

461+file = {:Users/edwin/Documents/Mendeley Desktop/Bentley/Beautiful Code Chapter 3/Bentley - Beautiful Code Chapter 3 - 2012.pdf:pdf},

462462isbn = {9780596510046},

463463issn = {1758-5341},

464464month = dec,

@@ -473,7 +473,7 @@ year = {2012}

473473@inproceedings{Fournet2011,

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

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

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

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

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

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

479479year = {2010}

@@ -481,7 +481,7 @@ year = {2010}

481481@inproceedings{chlipala2010ur,

482482author = {Chlipala, Adam},

483483booktitle = {ACM SIGPLAN Notices},

484−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chlipala - 2010 - Ur statically-typed metaprogramming with type-level record computation.pdf:pdf},

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

485485number = {6},

486486pages = {122--133},

487487publisher = {ACM},

@@ -500,13 +500,13 @@ This paper gives a control flow analysis for polymorphic functional programs (sp

500500While I like what is achieved by this paper, I did find it rather hard going. The introduction feels laboured and then the paper covers a lot of detail (possibly too much) in quite a short space (though it still runs to 18 pages, two more than the limit!). I would suggest that the paper would be much improved, particularly to a non-expert reader, if it give one or more motivating examples in the introduction and showed how the analysis applied to these examples, when translated to ANF.

501501I think this would shorten the introduction and give a much better intuition for the rules.},

502502author = {Fluet, Matthew},

503−file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_6.pdf:pdf},

503+file = {:Users/edwin/Documents/Mendeley Desktop/Fluet/A Type- and Control-Flow Analysis for System F/Fluet - A Type- and Control-Flow Analysis for System F - Unknown.pdf:pdf},

504504pages = {1--18},

505505title = {{A Type- and Control-Flow Analysis for System F}}

506506}

507507@article{Vytiniotis2011,

508508author = {Vytiniotis, Dimitrios and {Peyton Jones}, Simon and Schrijvers, Tom and Sulzmann, Martin},

509−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions.pdf:pdf;:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Vytiniotis et al. - 2011 - textsc{OutsideIn}(X) Modular type inference with local assumptions(2).pdf:pdf},

509+file = {:Users/edwin/Documents/Mendeley Desktop/Vytiniotis et al/textsc{OutsideIn}(X) Modular type inference with local assumptions/Vytiniotis et al. - textsc{OutsideIn}(X) Modular type inference with local assumptions - 2011.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Vytiniotis et al/textsc{OutsideIn}(X) Modular type inference with local assumptions/Vytiniotis et al. - textsc{OutsideIn}(X) Modular type inference with local assumptions - 2011(2).pdf:pdf},

510510journal = {{Journal of Functional Programming}},

511511number = {4--5},

512512pages = {333----412},

@@ -518,7 +518,7 @@ year = {2011}

518518@inproceedings{Gregoire2005,

519519author = {Gregoire, Benjamin and Mahboubi, Assia},

520520booktitle = {{Theorem Proving in Higher Order Logics (TPHOLS 2005)}},

521−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Gregoire, Mahboubi - 2005 - Proving Equalities in a Commutative Ring Done Right in Coq.pdf:pdf},

521+file = {:Users/edwin/Documents/Mendeley Desktop/Gregoire, Mahboubi/Proving Equalities in a Commutative Ring Done Right in Coq/Gregoire, Mahboubi - Proving Equalities in a Commutative Ring Done Right in Coq - 2005.pdf:pdf},

522522pages = {98----113},

523523title = {{Proving Equalities in a Commutative Ring Done Right in Coq}},

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

@@ -527,7 +527,7 @@ year = {2005}

527527@book{Cryptography2012,

528528author = {Anderson, Ross},

529529doi = {10.1093/intimm/dxs023},

530−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 5.pdf:pdf},

530+file = {:Users/edwin/Documents/Mendeley Desktop/Anderson/Security Engineering Chapter 5/Anderson - Security Engineering Chapter 5 - Unknown.pdf:pdf},

531531isbn = {9780470068526},

532532issn = {1460-2377},

533533number = {4},

@@ -538,14 +538,14 @@ volume = {24}

538538}

539539@article{Brady,

540540author = {Butenhof, David R.},

541−file = {:Users/edwin/Downloads/Safari/ProgrammingwithPOSIXThreadsChapter8Hintstoavoiddebu.pdf:pdf},

541+file = {:Users/edwin/Documents/Mendeley Desktop/Butenhof/Programming with POSIX Threads Chapter 8/Butenhof - Programming with POSIX Threads Chapter 8 - Unknown.pdf:pdf},

542542isbn = {0201633922},

543543title = {{Programming with POSIX Threads Chapter 8}}

544544}

545545@inproceedings{oury2008power,

546546author = {Oury, N. and Swierstra, W.},

547547booktitle = {International Conference on Functional Programming},

548−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Oury, Swierstra - 2008 - The power of Pi.pdf:pdf},

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

549549keywords = {Dependent Types},

550550mendeley-tags = {Dependent Types},

551551number = {9},

@@ -560,7 +560,7 @@ year = {2008}

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

561561author = {McBride, Conor and McKinna, James},

562562doi = {10.1017/S0956796803004829},

563−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, McKinna - 2004 - The view from the left.pdf:pdf},

563+file = {:Users/edwin/Documents/Mendeley Desktop/McBride, McKinna/The view from the left/McBride, McKinna - The view from the left - 2004.pdf:pdf},

564564issn = {09567968},

565565journal = {Journal of Functional Programming},

566566keywords = {Dependent Types},

@@ -577,7 +577,7 @@ year = {2004}

577577author = {Pfleeger, Charles P and Pfleeger, S. L.},

578578booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

579579doi = {10.1093/ntr/nts035},

580−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 2.pdf:pdf},

580+file = {:Users/edwin/Documents/Mendeley Desktop/Pfleeger, Pfleeger/Security in Computing Chapter 2/Pfleeger, Pfleeger - Security in Computing Chapter 2 - 2012.pdf:pdf},

581581isbn = {0132390779},

582582issn = {1469-994X},

583583month = oct,

@@ -591,7 +591,7 @@ year = {2012}

591591}

592592@phdthesis{Pretnar2010,

593593author = {Pretnar, Matija},

594−file = {:Users/edwin/Downloads/the-logic-and-handling-of-algebraic-effects.pdf:pdf},

594+file = {:Users/edwin/Documents/Mendeley Desktop/Pretnar/The Logic and Handling of Algebraic Effects/Pretnar - The Logic and Handling of Algebraic Effects - 2010.pdf:pdf},

595595school = {University of Edinburgh},

596596title = {{The Logic and Handling of Algebraic Effects}},

597597year = {2010}

@@ -599,7 +599,7 @@ year = {2010}

599599@inproceedings{Brady2010,

600600author = {Brady, Edwin and Hammond, Kevin},

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

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

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

603603isbn = {9781605587943},

604604keywords = {Dependent Types,code generation gives,contrast,dependent types,efficient,harder,however,implementation,likely efficient,ness interpreter,partial evaluation,resulting implementation,un,verify its correctness},

605605mendeley-tags = {Dependent Types},

@@ -611,7 +611,7 @@ year = {2010}

611611}

612612@misc{Danielsson2002,

613613author = {Danielsson, Nils Anders and Altenkirch, Thorsten},

614−file = {:Users/edwin/Downloads/Papers/danielsson-altenkirch-subtyping.pdf:pdf},

614+file = {:Users/edwin/Documents/Mendeley Desktop/Danielsson, Altenkirch/Subtyping, Declaratively/Danielsson, Altenkirch - Subtyping, Declaratively - 2002.pdf:pdf},

615615title = {{Subtyping, Declaratively}},

616616year = {2002}

617617}

@@ -619,7 +619,7 @@ year = {2002}

619619author = {Sedgewick, Robert and Wayne, Kevin},

620620booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

621621doi = {10.1093/ntr/nts035},

622−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sedgewick, Wayne - 2012 - Algorithms Chapter 5.pdf:pdf},

622+file = {:Users/edwin/Documents/Mendeley Desktop/Sedgewick, Wayne/Algorithms Chapter 5/Sedgewick, Wayne - Algorithms Chapter 5 - 2012.pdf:pdf},

623623isbn = {9780132762571},

624624issn = {1469-994X},

625625month = oct,

@@ -650,19 +650,19 @@ year = {1985}

650650@misc{Abel1998,

651651author = {Abel, Andreas},

652652booktitle = {Language},

653−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abel - 1998 - foetus - Termination Checker for Simple Functional Programs.pdf:pdf},

653+file = {:Users/edwin/Documents/Mendeley Desktop/Abel/foetus - Termination Checker for Simple Functional Programs/Abel - foetus - Termination Checker for Simple Functional Programs - 1998.pdf:pdf},

654654title = {{foetus - Termination Checker for Simple Functional Programs}},

655655year = {1998}

656656}

657657@article{Silkensen,

658658author = {Silkensen, Erik and Siek, Jeremy},

659−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Silkensen, Siek - Unknown - Well-typed Islands Parse Faster.pdf:pdf},

659+file = {:Users/edwin/Documents/Mendeley Desktop/Silkensen, Siek/Well-typed Islands Parse Faster/Silkensen, Siek - Well-typed Islands Parse Faster - Unknown.pdf:pdf},

660660title = {{Well-typed Islands Parse Faster}}

661661}

662662@misc{Svenningsson,

663663author = {Svenningsson, Josef and Axelsson, Emil},

664664booktitle = {Writing},

665−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Svenningsson, Axelsson - Unknown - Combining Deep and Shallow Embedding for EDSL.pdf:pdf},

665+file = {:Users/edwin/Documents/Mendeley Desktop/Svenningsson, Axelsson/Combining Deep and Shallow Embedding for EDSL/Svenningsson, Axelsson - Combining Deep and Shallow Embedding for EDSL - Unknown.pdf:pdf},

666666title = {{Combining Deep and Shallow Embedding for EDSL}}

667667}

668668@misc{Bauer,

@@ -670,21 +670,21 @@ archivePrefix = {arXiv},

670670arxivId = {arXiv:1203.1539v1},

671671author = {Bauer, Andrej and Pretnar, Matija},

672672eprint = {arXiv:1203.1539v1},

673−file = {:Users/edwin/Downloads/1203.1539v1.pdf:pdf},

673+file = {:Users/edwin/Documents/Mendeley Desktop/Bauer, Pretnar/Programming with Algebraic Effects and Handlers/Bauer, Pretnar - Programming with Algebraic Effects and Handlers - Unknown.pdf:pdf},

674674keywords = {()},

675675title = {{Programming with Algebraic Effects and Handlers}}

676676}

677677@misc{Krustev,

678678author = {Krustev, Dimitur},

679679booktitle = {Language},

680−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Krustev - Unknown - Towards a Framework for Building Formally Verified Supercompilers in Coq.pdf:pdf},

680+file = {:Users/edwin/Documents/Mendeley Desktop/Krustev/Towards a Framework for Building Formally Verified Supercompilers in Coq/Krustev - Towards a Framework for Building Formally Verified Supercompilers in Coq - Unknown.pdf:pdf},

681681title = {{Towards a Framework for Building Formally Verified Supercompilers in Coq}}

682682}

683683@book{Graphs2012,

684684author = {Sedgewick, Robert and Wayne, Kevin},

685685booktitle = {The Gerontologist},

686686doi = {10.1093/geront/gns026},

687−file = {:Users/edwin/Downloads/Safari/AlgorithmsFourthEditionChapterFourGraphs.pdf:pdf},

687+file = {:Users/edwin/Documents/Mendeley Desktop/Sedgewick, Wayne/Algorithms Chapter 4/Sedgewick, Wayne - Algorithms Chapter 4 - 2012.pdf:pdf},

688688isbn = {9780132762571},

689689issn = {1758-5341},

690690month = dec,

@@ -699,7 +699,7 @@ year = {2012}

699699@misc{Brady2012c,

700700author = {Brooks, Fred},

701701doi = {10.1093/epirev/mxr031},

702−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 5.pdf:pdf},

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

703703isbn = {9780321702081},

704704issn = {1478-6729},

705705number = {1},

@@ -711,7 +711,7 @@ volume = {34}

711711@inproceedings{coquand1986analysis,

712712author = {Coquand, T.},

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

714−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Coquand - 1986 - An analysis of Girard's paradox.pdf:pdf},

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

715715pages = {227----246},

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

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

@@ -719,13 +719,13 @@ year = {1986}

719719}

720720@book{Harper2012,

721721author = {Harper, Robert},

722−file = {:Users/edwin/Downloads/pfpl.pdf:pdf},

722+file = {:Users/edwin/Documents/Mendeley Desktop/Harper/Practical Foundations for Programming Languages/Harper - Practical Foundations for Programming Languages - 2012.pdf:pdf},

723723title = {{Practical Foundations for Programming Languages}},

724724year = {2012}

725725}

726726@misc{dagand2011transporting,

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

728−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Dagand, McBride - 2011 - Transporting Functions across Ornaments.pdf:pdf},

728+file = {:Users/edwin/Documents/Mendeley Desktop/Dagand, McBride/Transporting Functions across Ornaments/Dagand, McBride - Transporting Functions across Ornaments - 2011.pdf:pdf},

729729title = {{Transporting Functions across Ornaments}},

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

731731year = {2011}

@@ -733,7 +733,7 @@ year = {2011}

733733@article{Abel2010,

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

735735author = {Abel, Andreas},

736−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abel - 2010 - MiniAgda Integrating Sized and Dependent Types.pdf:pdf},

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

737737journal = {EPTCS},

738738pages = {1--15},

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

@@ -743,7 +743,7 @@ year = {2010}

743743}

744744@article{burrows1990,

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

746−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Burrows, Abadi, Needham - 1990 - A logic of authentication.pdf:pdf},

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

747747journal = {ACM Transactions on Computer Systems},

748748pages = {18----36},

749749title = {{A logic of authentication}},

@@ -753,7 +753,7 @@ year = {1990}

753753}

754754@article{loh2010tutorial,

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

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

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

757757journal = {Fundamenta Informaticae},

758758number = {2},

759759pages = {177--207},

@@ -765,7 +765,7 @@ year = {2010}

765765}

766766@article{mcbride2008functional,

767767author = {McBride, C. and Paterson, R.},

768−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, Paterson - 2008 - Functional pearl Applicative programming with effects.pdf:pdf},

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

769769journal = {Journal of functional programming},

770770number = {1},

771771pages = {1--13},

@@ -777,14 +777,14 @@ year = {2008}

777777}

778778@techreport{Cardelli1988,

779779author = {Cardelli, L},

780−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Cardelli - 1988 - Phase distinctions in type theory.pdf:pdf},

780+file = {:Users/edwin/Documents/Mendeley Desktop/Cardelli/Phase distinctions in type theory/Cardelli - Phase distinctions in type theory - 1988.pdf:pdf},

781781title = {{Phase distinctions in type theory}},

782782year = {1988}

783783}

784784@misc{Abadi1997,

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

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

787−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Abadi, Gordon - 1997 - A calculus for cryptographic protocols The spi calculus.pdf:pdf},

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

788788pages = {36 -- 47},

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

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

@@ -793,7 +793,7 @@ year = {1997}

793793@article{Haskell2012a,

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

795795doi = {10.1093/epirev/mxr031},

796−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Biancuzzi, Warden - Unknown - Masterminds of Programming Chapter 8.pdf:pdf},

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

797797isbn = {9780596801670},

798798issn = {1478-6729},

799799pmid = {22215642},

@@ -802,7 +802,7 @@ title = {{Masterminds of Programming Chapter 8}}

802802@inproceedings{madhavapeddy2010turning,

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

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

805−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Madhavapeddy et al. - 2010 - Turning down the LAMP software specialisation for the cloud.pdf:pdf},

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

806806publisher = {USENIX Association},

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

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

@@ -824,14 +824,14 @@ Could these techniques improve (compile-time) unification in dependently typed l

824824

825825Not many results. Encouraging, but only 7 of various forms isn't conclusive. },

826826author = {Bra\ss el, Bernd and Hanus, Michael and Peem\"{o}ller, Bj\"{o}rn and Reck, Fabian},

827−file = {:Users/edwin/Downloads/Papers/padl2013_submission_17.pdf:pdf},

827+file = {:Users/edwin/Documents/Mendeley Desktop/Bra\ss el et al/Implementing Equational Constraints in a Functional Language/Bra\ss el et al. - Implementing Equational Constraints in a Functional Language - Unknown.pdf:pdf},

828828keywords = {func-,functional logic programming,implementation,unification},

829829title = {{Implementing Equational Constraints in a Functional Language}}

830830}

831831@inproceedings{Brady2003,

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

833833booktitle = {Types for Proofs and Programs {(TYPES 2003)}},

834−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, McBride, McKinna - 2003 - Inductive families need not store their indices.pdf:pdf},

834+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, McBride, McKinna/Inductive families need not store their indices/Brady, McBride, McKinna - Inductive families need not store their indices - 2003.pdf:pdf},

835835keywords = {Dependent Types},

836836mendeley-tags = {Dependent Types},

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

@@ -841,7 +841,7 @@ year = {2003}

841841author = {Fowler, Martin},

842842booktitle = {Carcinogenesis},

843843doi = {10.1093/carcin/bgs054},

844−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},

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

845845isbn = {9780132107549},

846846issn = {1460-2180},

847847number = {3},

@@ -854,7 +854,7 @@ volume = {33}

854854author = {Fowler, Martin},

855855booktitle = {Carcinogenesis},

856856doi = {10.1093/carcin/bgs054},

857−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},

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

858858isbn = {9780132107549},

859859issn = {1460-2180},

860860number = {3},

@@ -865,7 +865,7 @@ volume = {33}

865865}

866866@misc{altenkirch2008nσ,

867867author = {Altenkirch, T. and Oury, N.},

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

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

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

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

871871year = {2008}

@@ -892,7 +892,7 @@ A question on contribution 1: how realistic is it to assume that nonterminals ar

892892

893893Some modern languages with dependent types have systems for syntax extension, e.g. Agda has mixfix declarations, Idris has syntax rules, type-directed elaboration and overloaded variable bindings. I wonder, therefore, if your approach to parsing could be better integrated into this kind of language, where embedded verifiable DSLs seem to be an obvious application. The Typed Racket example suggests to me that this would be an interesting thing to explore.},

894894author = {Silkensen, Erik and Siek, Jeremy},

895−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Silkensen, Siek - 2012 - Well-typed Islands Parse Faster.pdf:pdf},

895+file = {:Users/edwin/Documents/Mendeley Desktop/Silkensen, Siek/Well-typed Islands Parse Faster/Silkensen, Siek - Well-typed Islands Parse Faster - 2012.pdf:pdf},

896896pages = {1--12},

897897title = {{Well-typed Islands Parse Faster}},

898898year = {2012}

@@ -900,7 +900,7 @@ year = {2012}

900900@misc{The2012c,

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

902902doi = {10.1093/epirev/mxr031},

903−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Robbins, Hannah, Lamb - Unknown - Learning the vi and Vim Editors.pdf:pdf},

903+file = {:Users/edwin/Documents/Mendeley Desktop/Robbins, Hannah, Lamb/Learning the vi and Vim Editors/Robbins, Hannah, Lamb - Learning the vi and Vim Editors - Unknown.pdf:pdf},

904904isbn = {9780596529833},

905905issn = {1478-6729},

906906pmid = {22215642},

@@ -908,7 +908,7 @@ title = {{Learning the vi and Vim Editors}}

908908}

909909@misc{idristutorial,

910910author = {Brady, Edwin},

911−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},

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

912912title = {{Programming in Idris : a tutorial}},

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

914914year = {2012}

@@ -917,7 +917,7 @@ year = {2012}

917917author = {Seibel, Peter},

918918booktitle = {The Gerontologist},

919919doi = {10.1093/geront/gns026},

920−file = {:Users/edwin/Downloads/Safari/CodersatWorkReflectionsontheCraftofProgrammingChapter7SimonPeytonJones.pdf:pdf},

920+file = {:Users/edwin/Documents/Mendeley Desktop/Seibel/Coders at Work Chapter 7/Seibel - Coders at Work Chapter 7 - 2012.pdf:pdf},

921921isbn = {9781430219484},

922922issn = {1758-5341},

923923month = dec,

@@ -934,7 +934,7 @@ abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your pe

934934address = {London},

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

936936booktitle = {Mendeley Desktop},

937−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

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

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

939939pages = {1--16},

940940publisher = {Mendeley Ltd.},

@@ -946,7 +946,7 @@ year = {2011}

946946author = {Seibel, Peter},

947947booktitle = {The Gerontologist},

948948doi = {10.1093/geront/gns026},

949−file = {:Users/edwin/Downloads/Safari/CodersatWorkReflectionsontheCraftofProgrammingChapter6JoeArmstrong.pdf:pdf},

949+file = {:Users/edwin/Documents/Mendeley Desktop/Seibel/Coders at Work Chapter 6/Seibel - Coders at Work Chapter 6 - 2012.pdf:pdf},

950950isbn = {9781430219484},

951951issn = {1758-5341},

952952month = dec,

@@ -961,7 +961,7 @@ year = {2012}

961961@inproceedings{l,

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

963963booktitle = {ACM SIGPLAN Notices},

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

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

965965number = {3},

966966pages = {26--37},

967967publisher = {ACM},

@@ -972,7 +972,7 @@ year = {2003}

972972}

973973@phdthesis{Okasaki1996,

974974author = {Okasaki, Chris},

975−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Okasaki - 1996 - Purely Functional Data Structures.pdf:pdf},

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

976976school = {Carnegie Mellon University},

977977title = {{Purely Functional Data Structures}},

978978year = {1996}

@@ -980,14 +980,14 @@ year = {1996}

980980@inproceedings{McBride2004b,

981981author = {McBride, Conor and McKinna, James},

982982booktitle = {Haskell Workshop},

983−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride, McKinna - 2004 - I am not a number I am a free variable.pdf:pdf},

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

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

985985year = {2004}

986986}

987987@inproceedings{Brady2005a,

988988author = {Brady, E and Hammond, K},

989989booktitle = {Implementation and Application of Functional \ldots},

990−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2005 - A dependently typed framework for static analysis of program execution costs.pdf:pdf},

990+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/A dependently typed framework for static analysis of program execution costs/Brady, Hammond - A dependently typed framework for static analysis of program execution costs - 2005.pdf:pdf},

991991keywords = {Dependent Types},

992992mendeley-tags = {Dependent Types},

993993title = {{A dependently typed framework for static analysis of program execution costs}},

@@ -996,7 +996,7 @@ year = {2005}

996996}

997997@misc{TMR13,

998998author = {Eidhof, Chris and Elkins, Derek and Hicks, Stephen},

999−file = {:Users/edwin/Downloads/Papers/TMR-Issue13.pdf:pdf},

999+file = {:Users/edwin/Documents/Mendeley Desktop/Eidhof, Elkins, Hicks/The Monad . Reader Issue 13/Eidhof, Elkins, Hicks - The Monad . Reader Issue 13 - 2009.pdf:pdf},

10001000number = {13},

10011001title = {{The Monad . Reader Issue 13}},

10021002year = {2009}

@@ -1048,14 +1048,14 @@ Reference 1 is blank

10481048

10491049 },

10501050author = {Rose, Eva},

1051−file = {:Users/edwin/Downloads/Papers/padl2013_submission_33.pdf:pdf},

1051+file = {:Users/edwin/Documents/Mendeley Desktop/Rose/Declarative implementation aspects of privacy policy effects/Rose - Declarative implementation aspects of privacy policy effects - Unknown.pdf:pdf},

10521052keywords = {constraints,language design,mon-,privacy policy,semantics},

10531053title = {{Declarative implementation aspects of privacy policy effects}}

10541054}

10551055@inproceedings{morris2006exploring,

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

10571057booktitle = {Types for Proofs and Programs},

1058−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Morris, Altenkirch, McBride - 2006 - Exploring the regular tree types.pdf:pdf},

1058+file = {:Users/edwin/Documents/Mendeley Desktop/Morris, Altenkirch, McBride/Exploring the regular tree types/Morris, Altenkirch, McBride - Exploring the regular tree types - 2006.pdf:pdf},

10591059pages = {252--267},

10601060publisher = {Springer},

10611061title = {{Exploring the regular tree types}},

@@ -1065,7 +1065,7 @@ year = {2006}

10651065@inproceedings{pj2006gadts,

10661066author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},

10671067booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},

1068−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},

1068+file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/Simple unification-based type inference for GADTs/Peyton Jones et al. - Simple unification-based type inference for GADTs - 2006.pdf:pdf},

10691069number = {9},

10701070pages = {50--61},

10711071publisher = {ACM},

@@ -1083,14 +1083,14 @@ year = {1994}

10831083}

10841084@misc{Hancock,

10851085author = {Hancock, Peter and Setzer, Anton},

1086−file = {:Users/edwin/Downloads/10.1.1.25.9367.pdf:pdf},

1086+file = {:Users/edwin/Documents/Mendeley Desktop/Hancock, Setzer/Interactive Programs in Dependent Type Theory/Hancock, Setzer - Interactive Programs in Dependent Type Theory - 2000(2).pdf:pdf},

10871087keywords = {dependent types,functional programming,interac-,monadic i,o,reactive programming,refinement,repetition constructs,tion},

10881088title = {{Interactive Programs in Dependent Type Theory}},

10891089year = {2000}

10901090}

10911091@book{Chlipala2012,

10921092author = {Chlipala, Adam},

1093−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chlipala - 2012 - Certified Programming with Dependent Types.pdf:pdf},

1093+file = {:Users/edwin/Documents/Mendeley Desktop/Chlipala/Certified Programming with Dependent Types/Chlipala - Certified Programming with Dependent Types - 2012.pdf:pdf},

10941094title = {{Certified Programming with Dependent Types}},

10951095year = {2012}

10961096}

@@ -1112,7 +1112,7 @@ year = {2007}

11121112}

11131113@article{Nabais2008,

11141114author = {Nabais, Davide},

1115−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Nabais - 2008 - DesCo a Web Based Information System for Descriptional Complexity of Formal Languages.pdf:pdf},

1115+file = {:Users/edwin/Documents/Mendeley Desktop/Nabais/DesCo a Web Based Information System for Descriptional Complexity of Formal Languages/Nabais - DesCo a Web Based Information System for Descriptional Complexity of Formal Languages - 2008.pdf:pdf},

11161116journal = {Most},

11171117pages = {1--5},

11181118title = {{DesCo : a Web Based Information System for Descriptional Complexity of Formal Languages}},

@@ -1122,7 +1122,7 @@ year = {2008}

11221122author = {Pfleeger, Charles P and Pfleeger, S. L.},

11231123booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

11241124doi = {10.1093/ntr/nts035},

1125−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 1.pdf:pdf},

1125+file = {:Users/edwin/Documents/Mendeley Desktop/Pfleeger, Pfleeger/Security in Computing Chapter 1/Pfleeger, Pfleeger - Security in Computing Chapter 1 - 2012.pdf:pdf},

11261126isbn = {0132390779},

11271127issn = {1469-994X},

11281128month = oct,

@@ -1136,14 +1136,14 @@ year = {2012}

11361136}

11371137@book{Eap,

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

1139−file = {:Users/edwin/Downloads/Safari/TCPIPIllustratedVolume1TheProtocolsSecondEditionChapter18SecurityEAPIPs.pdf:pdf},

1139+file = {:Users/edwin/Documents/Mendeley Desktop/Fall, Stevens/TCPIP Illustrated Chapter 18/Fall, Stevens - TCPIP Illustrated Chapter 18 - Unknown.pdf:pdf},

11401140isbn = {9780132808200},

11411141title = {{TCP/IP Illustrated Chapter 18}}

11421142}

11431143@book{Fowler,

11441144author = {Fowler, Martin},

11451145booktitle = {Language},

1146−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},

1146+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Domain Specific Languages Chapter 2/Fowler - Domain Specific Languages Chapter 2 - Unknown.pdf:pdf},

11471147isbn = {9780132107549},

11481148title = {{Domain Specific Languages Chapter 2}}

11491149}

@@ -1151,7 +1151,7 @@ title = {{Domain Specific Languages Chapter 2}}

11511151author = {Seibel, Peter},

11521152booktitle = {The Gerontologist},

11531153doi = {10.1093/geront/gns026},

1154−file = {:Users/edwin/Downloads/Safari/CodersatWorkReflectionsontheCraftofProgrammingChapter9GuySteele.pdf:pdf},

1154+file = {:Users/edwin/Documents/Mendeley Desktop/Seibel/Coders at Work Chapter 9/Seibel - Coders at Work Chapter 9 - 2012.pdf:pdf},

11551155isbn = {9781430219484},

11561156issn = {1758-5341},

11571157month = dec,

@@ -1166,7 +1166,7 @@ year = {2012}

11661166@article{Regular2012,

11671167author = {Kernighan, Brian},

11681168doi = {10.1093/geront/gns026},

1169−file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter1ARegularExpressio.pdf:pdf},

1169+file = {:Users/edwin/Documents/Mendeley Desktop/Kernighan/Beautiful Code Chapter 1/Kernighan - Beautiful Code Chapter 1 - 2012.pdf:pdf},

11701170isbn = {9780596510046},

11711171issn = {1758-5341},

11721172month = dec,

@@ -1181,7 +1181,7 @@ year = {2012}

11811181@inproceedings{norell2009dependently,

11821182author = {Norell, Ulf},

11831183booktitle = {Advanced Functional Programming},

1184−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Norell - 2009 - Dependently typed programming in Agda.pdf:pdf},

1184+file = {:Users/edwin/Documents/Mendeley Desktop/Norell/Dependently typed programming in Agda/Norell - Dependently typed programming in Agda - 2009.pdf:pdf},

11851185keywords = {Dependent Types},

11861186mendeley-tags = {Dependent Types},

11871187pages = {230--266},

@@ -1193,7 +1193,7 @@ year = {2009}

11931193@misc{Interface2012a,

11941194author = {Kreibich, Jay A.},

11951195doi = {10.1093/epirev/mxr031},

1196−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Kreibich - Unknown - Using SQLite Chapter 7.pdf:pdf},

1196+file = {:Users/edwin/Documents/Mendeley Desktop/Kreibich/Using SQLite Chapter 7/Kreibich - Using SQLite Chapter 7 - Unknown.pdf:pdf},

11971197isbn = {9781449394592},

11981198issn = {1478-6729},

11991199pmid = {22215642},

@@ -1204,7 +1204,7 @@ abstract = {Cayenne is a Haskell-like language. The main difference between Hask

12041204author = {Augustsson, Lennart},

12051205booktitle = {International Conference on Functional Programming},

12061206doi = {10.1097/MEG.0b013e328342f213},

1207−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Augustsson - 1998 - Cayenne - a language with dependent types.pdf:pdf},

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

12081208issn = {14735687},

12091209keywords = {Depe,Dependent Types},

12101210mendeley-tags = {Depe,Dependent Types},

@@ -1219,7 +1219,7 @@ year = {1998}

12191219}

12201220@article{OutsideIn,

12211221author = {Vytiniotis, D and {Peyton Jones}, Simon and Shrijvers, Tom and Sulzmann, Martin},

1222−file = {:Users/edwin/Downloads/jfp-outsidein.pdf:pdf},

1222+file = {:Users/edwin/Documents/Mendeley Desktop/Vytiniotis et al/textsc{OutsideIn}(X) Modular type inference with local assumptions/Vytiniotis et al. - textsc{OutsideIn}(X) Modular type inference with local assumptions - 2011.pdf:pdf},

12231223journal = {Journal of Functional Programming},

12241224number = {4--5},

12251225pages = {333----412},

@@ -1243,7 +1243,7 @@ year = {2005}

12431243author = {Chapman, James and Dagand, Pierre-Evariste and McBride, Conor and Morris, Peter},

12441244booktitle = {{15th ACM SIGPLAN International Conference on Functional programming (ICFP '10)}},

12451245doi = {10.1145/1932681.1863547},

1246−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chapman et al. - 2010 - The gentle art of levitation.pdf:pdf},

1246+file = {:Users/edwin/Documents/Mendeley Desktop/Chapman et al/The gentle art of levitation/Chapman et al. - The gentle art of levitation - 2010.pdf:pdf},

12471247isbn = {978-1-60558-794-3},

12481248issn = {03621340},

12491249keywords = {Dependent Types,data structure,metaprogramming,monads,proof assistants,type systems},

@@ -1259,7 +1259,7 @@ year = {2010}

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

12601260booktitle = {Carcinogenesis},

12611261doi = {10.1093/carcin/bgs054},

1262−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},

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

12631263isbn = {020161622X},

12641264issn = {1460-2180},

12651265number = {3},

@@ -1274,7 +1274,7 @@ author = {Hughes, J},

12741274chapter = {2},

12751275doi = {10.1093/comjnl/32.2.98},

12761276editor = {Turner, David A},

1277−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hughes - 1989 - Why Functional Programming Matters.pdf:pdf},

1277+file = {:Users/edwin/Documents/Mendeley Desktop/Hughes/Why Functional Programming Matters/Hughes - Why Functional Programming Matters - 1989.pdf:pdf},

12781278institution = {Programming Methodology Group, University of {G\"{o}teborg} and Chalmers Institute of Technology, Sweden},

12791279isbn = {0201172364},

12801280issn = {00104620},

@@ -1289,7 +1289,7 @@ year = {1989}

12891289}

12901290@article{Brady2006a,

12911291author = {Brady, E and Hammond, K},

1292−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2006 - A verified staged interpreter is a verified compiler.pdf:pdf},

1292+file = {:Users/edwin/Documents/Mendeley Desktop/Brady, Hammond/A verified staged interpreter is a verified compiler/Brady, Hammond - A verified staged interpreter is a verified compiler - 2006.pdf:pdf},

12931293journal = {\ldots of the 5th international conference on \ldots},

12941294keywords = {Dependent Types},

12951295mendeley-tags = {Dependent Types},

@@ -1301,7 +1301,7 @@ year = {2006}

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

13021302author = {Xi, Hongwei and Pfenning, Frank},

13031303doi = {10.1145/277652.277732},

1304−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Xi, Pfenning - 1998 - Eliminating array bound checking through dependent types.pdf:pdf},

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

13051305isbn = {0897919874},

13061306issn = {03621340},

13071307journal = {ACM Sigplan Notices},

@@ -1319,7 +1319,7 @@ year = {1998}

13191319@inproceedings{Abel2013,

13201320author = {Abel, Andreas and Pientka, Brigitte and Thibodeau, David and Setzer, Anton},

13211321booktitle = {Principles of Programming Languages},

1322−file = {:Users/edwin/Downloads/popl13.pdf:pdf},

1322+file = {:Users/edwin/Documents/Mendeley Desktop/Abel et al/Copatterns Programming Infinite Structures by Observations/Abel et al. - Copatterns Programming Infinite Structures by Observations - 2013.pdf:pdf},

13231323isbn = {9781450318327},

13241324keywords = {2008,by the graduiertenkol-,coinduction,elimination,functional programming,introduction,leg programm und modellanalyse,message passing,of the deutsche,pattern matching,puma,thibodeau acknowledges financial support,vs},

13251325title = {{Copatterns: Programming Infinite Structures by Observations}},

@@ -1327,7 +1327,7 @@ year = {2013}

13271327}

13281328@misc{pollack1997believe,

13291329author = {Pollack, R.},

1330−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pollack - 1997 - How to believe a machine-checked proof.pdf:pdf},

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

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

13321332url = {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},

13331333year = {1997}

@@ -1336,7 +1336,7 @@ year = {1997}

13361336author = {Sedgewick, Robert and Wayne, Kevin},

13371337booktitle = {The Gerontologist},

13381338doi = {10.1093/geront/gns026},

1339−file = {:Users/edwin/Downloads/Safari/AlgorithmsFourthEditionChapterThreeSearching.pdf:pdf},

1339+file = {:Users/edwin/Documents/Mendeley Desktop/Sedgewick, Wayne/Algorithms Chapter 3/Sedgewick, Wayne - Algorithms Chapter 3 - 2012.pdf:pdf},

13401340isbn = {9780132762571},

13411341issn = {1758-5341},

13421342month = dec,

@@ -1352,7 +1352,7 @@ year = {2012}

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

13531353booktitle = {Carcinogenesis},

13541354doi = {10.1093/carcin/bgs054},

1355−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},

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

13561356isbn = {020161622X},

13571357issn = {1460-2180},

13581358number = {3},

@@ -1363,7 +1363,7 @@ volume = {33}

13631363}

13641364@article{Servers,

13651365author = {Totty, Brian and Gourley, David},

1366−file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter5WebServers.pdf:pdf},

1366+file = {:Users/edwin/Documents/Mendeley Desktop/Totty, Gourley/HTTP The Definitive Guide Chapter 5/Totty, Gourley - HTTP The Definitive Guide Chapter 5 - Unknown.pdf:pdf},

13671367isbn = {1565925092},

13681368title = {{HTTP: The Definitive Guide Chapter 5}}

13691369}

@@ -1373,7 +1373,7 @@ annote = {This new version of the paper is, I think, very clear and an entertain

13731373

13741374I'm not totally convinced about the condition of the algorithm being "discovered in a disciplined manner" since many of the steps in the calculation required some insight, but others will disagree and I don't think it really matters for the main point of this paper in any case - the point is the calculational development, which is sufficiently detailed that a careful reader should be able to develop that insight, with practice. I would recommend this paper for acceptance in its current form. },

13751375author = {Bird, Richard S},

1376−file = {:Users/edwin/Downloads/Papers/s1-ln13057035-302779530-1939656818Hwf-543670216IdV208531454713057035PDF_HI0001.pdf:pdf},

1376+file = {:Users/edwin/Documents/Mendeley Desktop/Bird/An in-situ algorithm for expanding a graph/Bird - An in-situ algorithm for expanding a graph - 2012.pdf:pdf},

13771377keywords = {a href,journal of functional programming},

13781378title = {{An in-situ algorithm for expanding a graph}},

13791379year = {2012}

@@ -1381,14 +1381,14 @@ year = {2012}

13811381@inproceedings{Sculthorpe2009,

13821382author = {Sculthorpe, Neil and Nilsson, Henrik},

13831383booktitle = {International Conference on Functional Programming ({ICFP} '09)},

1384−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},

1384+file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Safe functional reactive programming through dependent types/Sculthorpe, Nilsson - Safe functional reactive programming through dependent types - 2009.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Safe functional reactive programming through dependent types/Sculthorpe, Nilsson - Safe functional reactive programming through dependent types - 2009(2).pdf:pdf},

13851385title = {{Safe functional reactive programming through dependent types}},

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

13871387year = {2009}

13881388}

13891389@article{landin1966next,

13901390author = {Landin, P.J.},

1391−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Landin - 1966 - The next 700 programming languages.pdf:pdf},

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

13921392journal = {Communications of the ACM},

13931393number = {3},

13941394pages = {157--166},

@@ -1401,7 +1401,7 @@ year = {1966}

14011401@inproceedings{Delahaye2000,

14021402author = {Delahaye, D},

14031403booktitle = {Logic for Programming and Automated Reasoning},

1404−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Delahaye - 2000 - A tactic language for the system Coq.pdf:pdf;:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Delahaye - 2000 - A tactic language for the system Coq(2).pdf:pdf},

1404+file = {:Users/edwin/Documents/Mendeley Desktop/Delahaye/A tactic language for the system Coq/Delahaye - A tactic language for the system Coq - 2000.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Delahaye/A tactic language for the system Coq/Delahaye - A tactic language for the system Coq - 2000(2).pdf:pdf},

14051405pages = {85----95},

14061406publisher = {Springer},

14071407title = {{A tactic language for the system Coq}},

@@ -1410,14 +1410,14 @@ year = {2000}

14101410}

14111411@book{Messages,

14121412author = {Totty, Brian and Gourley, David},

1413−file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter3HTTPMessages.pdf:pdf},

1413+file = {:Users/edwin/Documents/Mendeley Desktop/Totty, Gourley/HTTP The Definitive Guide Chapter 3/Totty, Gourley - HTTP The Definitive Guide Chapter 3 - Unknown.pdf:pdf},

14141414isbn = {1565925092},

14151415title = {{HTTP: The Definitive Guide Chapter 3}}

14161416}

14171417@article{Asperti,

14181418author = {Asperti, Andrea and Ricciotti, Wilmer and Coen, Claudio Sacerdoti and Tassi, Enrico},

14191419doi = {10.2168/LMCS-},

1420−file = {:Users/edwin/Downloads/lmcs_types_2010.pdf:pdf},

1420+file = {:Users/edwin/Documents/Mendeley Desktop/Asperti et al/A bi-directional refinement algorithm for the calculus of (co)inductive constructions/Asperti et al. - A bi-directional refinement algorithm for the calculus of (co)inductive constructions - 2012.pdf:pdf},

14211421journal = {Logical Methods in Computer Science},

14221422keywords = {and phrases,calculus of inductive construc-,interactive theorem prover,refiner,type inference},

14231423pages = {1----49},

@@ -1431,7 +1431,7 @@ author = {Altenkirch, Thorsten and Danielsson, Nils Anders and L\"{o}h, Andres a

14311431booktitle = {{FLOPS 2010}},

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

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

1434−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch et al. - 2010 - Dependent Types without the Sugar.pdf:pdf},

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

14351435isbn = {9783642122507},

14361436pages = {40----55},

14371437publisher = {Springer Berlin Heidelberg},

@@ -1443,7 +1443,7 @@ year = {2010}

14431443@misc{Gobi2010,

14441444author = {Gobi, Attila and Shkaravska, Olha and {Van Eekelen}, Marko},

14451445booktitle = {Syntax},

1446−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Gobi, Shkaravska, Van Eekelen - 2010 - Higher-Order Size Checking Without Subtyping.pdf:pdf},

1446+file = {:Users/edwin/Documents/Mendeley Desktop/Gobi, Shkaravska, Van Eekelen/Higher-Order Size Checking Without Subtyping/Gobi, Shkaravska, Van Eekelen - Higher-Order Size Checking Without Subtyping - 2010.pdf:pdf},

14471447number = {100039},

14481448title = {{Higher-Order Size Checking Without Subtyping}},

14491449year = {2010}

@@ -1452,7 +1452,7 @@ year = {2010}

14521452author = {Sedgewick, Robert and Wayne, Kevin},

14531453booktitle = {The Gerontologist},

14541454doi = {10.1093/geront/gns026},

1455−file = {:Users/edwin/Downloads/Safari/AlgorithmsFourthEditionChapterSixContext.pdf:pdf},

1455+file = {:Users/edwin/Documents/Mendeley Desktop/Sedgewick, Wayne/Algorithms Chapter 6/Sedgewick, Wayne - Algorithms Chapter 6 - 2012.pdf:pdf},

14561456isbn = {9780132762571},

14571457issn = {1758-5341},

14581458month = dec,

@@ -1467,7 +1467,7 @@ year = {2012}

14671467@misc{Protocols2012a,

14681468author = {Anderson, Ross},

14691469doi = {10.1093/epirev/mxr031},

1470−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 3.pdf:pdf},

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

14711471isbn = {9780470068526},

14721472issn = {1478-6729},

14731473pmid = {22215642},

@@ -1482,7 +1482,7 @@ year = {2008}

14821482}

14831483@inproceedings{gibbons2011modularising,

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

1485−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

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

14861486title = {{Modularising inductive families}},

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

14881488year = {2011}

@@ -1491,7 +1491,7 @@ year = {2011}

14911491author = {Butenhof, David R.},

14921492booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

14931493doi = {10.1093/ntr/nts035},

1494−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Butenhof - Unknown - Programming with POSIX Threads Chapter 3.pdf:pdf},

1494+file = {:Users/edwin/Documents/Mendeley Desktop/Butenhof/Programming with POSIX Threads Chapter 3/Butenhof - Programming with POSIX Threads Chapter 3 - Unknown.pdf:pdf},

14951495isbn = {0201633922},

14961496issn = {1469-994X},

14971497number = {10},

@@ -1542,12 +1542,12 @@ p14 (and other places similarly) I don't think it helps much to give the full se

15421542

15431543 },

15441544author = {Pl\"{u}micke, Martin},

1545−file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_13.pdf:pdf},

1545+file = {:Users/edwin/Documents/Mendeley Desktop/Pl{u}micke/Functional implementation of well-typings in/Pl{u}micke - Functional implementation of well-typings in - Unknown.pdf:pdf},

15461546title = {{Functional implementation of well-typings in}}

15471547}

15481548@article{gordon2003authenticity,

15491549author = {Gordon, A.D. and Jeffrey, A.},

1550−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Gordon, Jeffrey - 2003 - Authenticity by typing for security protocols.pdf:pdf},

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

15511551journal = {Journal of computer security},

15521552number = {4},

15531553pages = {451--520},

@@ -1561,7 +1561,7 @@ year = {2003}

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

15621562booktitle = {Carcinogenesis},

15631563doi = {10.1093/carcin/bgs054},

1564−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},

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

15651565isbn = {020161622X},

15661566issn = {1460-2180},

15671567number = {3},

@@ -1573,7 +1573,7 @@ volume = {33}

15731573@inproceedings{barras2008implicit,

15741574author = {Barras, B. and Bernardo, B.},

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

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

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

15771577pages = {365--379},

15781578publisher = {Springer},

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

@@ -1582,7 +1582,7 @@ year = {2008}

15821582}

15831583@article{Zanasi,

15841584author = {Zanasi, Fabio},

1585−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Zanasi - Unknown - On the Expressive Power of MSO and WMSO on Trees of Arbitrary Degree ( Extended abstract ).pdf:pdf},

1585+file = {:Users/edwin/Documents/Mendeley Desktop/Zanasi/On the Expressive Power of MSO and WMSO on Trees of Arbitrary Degree ( Extended abstract )/Zanasi - On the Expressive Power of MSO and WMSO on Trees of Arbitrary Degree ( Extended abstract ) - Unknown.pdf:pdf},

15861586pages = {1--6},

15871587title = {{On the Expressive Power of MSO and WMSO on Trees of Arbitrary Degree ( Extended abstract )}}

15881588}

@@ -1619,7 +1619,7 @@ p10 Another alternative for the type of filter could be a type level function to

16191619

16201620p14 "We have build" => "We have built"},

16211621author = {Thiemann, Peter and Chakravarty, Manuel M T},

1622−file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_30.pdf:pdf},

1622+file = {:Users/edwin/Documents/Mendeley Desktop/Thiemann, Chakravarty/Agda Meets Accelerate/Thiemann, Chakravarty - Agda Meets Accelerate - Unknown.pdf:pdf},

16231623keywords = {data parallelism,programming with dependent types},

16241624pages = {1--16},

16251625title = {{Agda Meets Accelerate}}

@@ -1636,7 +1636,7 @@ year = {2009}

16361636@inproceedings{ko2011modularising,

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

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

1639−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Ko, Gibbons - 2011 - Modularising inductive families.pdf:pdf},

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

16401640pages = {13--24},

16411641publisher = {ACM},

16421642title = {{Modularising inductive families}},

@@ -1645,7 +1645,7 @@ year = {2011}

16451645}

16461646@article{Chapman2005epigram,

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

1648−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Chapman, Altenkirch, McBride - 2005 - Epigram Reloaded A Standalone Typechecker for {ETT}.pdf:pdf},

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

16491649journal = {Trends in Functional Programming},

16501650publisher = {Intellect Books},

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

@@ -1654,7 +1654,7 @@ year = {2005}

16541654}

16551655@article{Hutton,

16561656author = {Hutton, Graham and Fulger, Diana},

1657−file = {:Users/edwin/Downloads/effects.pdf:pdf},

1657+file = {:Users/edwin/Documents/Mendeley Desktop/Hutton, Fulger/Reasoning About Effects Seeing the Wood Through the Trees/Hutton, Fulger - Reasoning About Effects Seeing the Wood Through the Trees - Unknown.pdf:pdf},

16581658title = {{Reasoning About Effects : Seeing the Wood Through the Trees}}

16591659}

16601660@article{dybjer1994inductive,

@@ -1673,7 +1673,7 @@ abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your pe

16731673address = {London},

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

16751675booktitle = {Mendeley Desktop},

1676−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

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

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

16781678pages = {1--16},

16791679publisher = {Mendeley Ltd.},

@@ -1684,7 +1684,7 @@ year = {2011}

16841684@misc{Brady2012b,

16851685author = {Brooks, Fred},

16861686doi = {10.1093/epirev/mxr031},

1687−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 2.pdf:pdf},

1687+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/The Design of Design Chapter 2/Brooks - The Design of Design Chapter 2 - Unknown.pdf:pdf},

16881688isbn = {9780321702081},

16891689issn = {1478-6729},

16901690pmid = {22215642},

@@ -1695,7 +1695,7 @@ abstract = {In these lecture notes we give an introduction to functional program

16951695author = {Bove, Ana and Dybjer, Peter},

16961696booktitle = {Notes},

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

1698−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bove, Dybjer - 2008 - Dependent Types at Work.pdf:pdf},

1698+file = {:Users/edwin/Documents/Mendeley Desktop/Bove, Dybjer/Dependent Types at Work/Bove, Dybjer - Dependent Types at Work - 2008.pdf:pdf},

16991699number = {February},

17001700pages = {57--99},

17011701publisher = {Springer},

@@ -1707,7 +1707,7 @@ year = {2008}

17071707@article{In2012,

17081708author = {Gulhati, Ashish},

17091709doi = {10.1093/geront/gns026},

1710−file = {:Users/edwin/Downloads/Safari/BeautifulCodeChapter11SecureCommunicati.pdf:pdf},

1710+file = {:Users/edwin/Documents/Mendeley Desktop/Gulhati/Beautiful Code Chapter 11/Gulhati - Beautiful Code Chapter 11 - 2012.pdf:pdf},

17111711isbn = {9780596510046},

17121712issn = {1758-5341},

17131713month = dec,

@@ -1721,7 +1721,7 @@ year = {2012}

17211721}

17221722@article{McBride2002,

17231723author = {McBride, C},

1724−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/McBride - 2000 - Elimination with a Motive.pdf:pdf},

1724+file = {:Users/edwin/Documents/Mendeley Desktop/McBride/Elimination with a Motive/McBride - Elimination with a Motive - 2000.pdf:pdf},

17251725journal = {Types for proofs and programs ({TYPES 2000})},

17261726title = {{Elimination with a Motive}},

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

@@ -1730,7 +1730,7 @@ year = {2000}

17301730@inproceedings{lempsink2009type,

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

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

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

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

17341734pages = {61--72},

17351735publisher = {ACM},

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

@@ -1742,7 +1742,7 @@ address = {New York, New York, USA},

17421742author = {Brady, Edwin},

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

17441744doi = {10.1145/1929529.1929536},

1745−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2011 - Idris --- Systems Programming Meets Full Dependent Types.pdf:pdf},

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

17461746isbn = {9781450304870},

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

17481748mendeley-tags = {Dependent Types},

@@ -1755,7 +1755,7 @@ year = {2011}

17551755@misc{altenkirch2005dependent,

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

17571757booktitle = {Manuscript, available online},

1758−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, McBride, McKinna - 2005 - Why dependent types matter.pdf:pdf},

1758+file = {:Users/edwin/Documents/Mendeley Desktop/Altenkirch, McBride, McKinna/Why dependent types matter/Altenkirch, McBride, McKinna - Why dependent types matter - 2005.pdf:pdf},

17591759title = {{Why dependent types matter}},

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

17611761year = {2005}

@@ -1763,7 +1763,7 @@ year = {2005}

17631763@misc{Nodes2012a,

17641764author = {Brooks, Fred},

17651765doi = {10.1093/epirev/mxr031},

1766−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 3.pdf:pdf},

1766+file = {:Users/edwin/Documents/Mendeley Desktop/Brooks/The Design of Design Chapter 3/Brooks - The Design of Design Chapter 3 - Unknown.pdf:pdf},

17671767isbn = {9780321702081},

17681768issn = {1478-6729},

17691769pmid = {22215642},

@@ -1780,7 +1780,7 @@ year = {2011}

17801780}

17811781@book{Bird2010,

17821782author = {Bird, Richard},

1783−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bird - 2010 - Pearls of Functional Algorithm Design.pdf:pdf},

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

17841784isbn = {9780521513388},

17851785title = {{Pearls of Functional Algorithm Design}},

17861786year = {2010}

@@ -1788,7 +1788,7 @@ year = {2010}

17881788@article{Jones1999,

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

17901790author = {Jones, Mark P},

1791−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Jones - 1999 - Typing Haskell in Haskell.pdf:pdf},

1791+file = {:Users/edwin/Documents/Mendeley Desktop/Jones/Typing Haskell in Haskell/Jones - Typing Haskell in Haskell - 1999.pdf:pdf},

17921792journal = {October},

17931793publisher = {Citeseer},

17941794title = {{Typing Haskell in Haskell}},

@@ -1799,7 +1799,7 @@ year = {1999}

17991799author = {Pfleeger, Charles P and Pfleeger, S. L.},

18001800booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

18011801doi = {10.1093/ntr/nts035},

1802−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computing Chapter 3.pdf:pdf},

1802+file = {:Users/edwin/Documents/Mendeley Desktop/Pfleeger, Pfleeger/Security in Computing Chapter 3/Pfleeger, Pfleeger - Security in Computing Chapter 3 - 2012.pdf:pdf},

18031803isbn = {0132390779},

18041804issn = {1469-994X},

18051805month = oct,

@@ -1813,7 +1813,7 @@ year = {2012}

18131813}

18141814@article{Steiner1988,

18151815author = {Steiner, JG},

1816−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},

1816+file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Kerberos An authentication service for open network systems/Steiner - Kerberos An authentication service for open network systems - 1988.pdf:pdf},

18171817journal = {Proc. Winter USENIX Conference},

18181818title = {{Kerberos: An authentication service for open network systems}},

18191819url = {http://www.cse.nd.edu/$\sim$dthain/courses/cse598z/fall2004/papers/kerberos.pdf},

@@ -1822,7 +1822,7 @@ year = {1988}

18221822@inproceedings{stump2010resource,

18231823author = {Stump, A. and Austin, E.},

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

1825−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Stump, Austin - 2010 - Resource typing in Guru.pdf:pdf},

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

18261826pages = {27--38},

18271827publisher = {ACM},

18281828title = {{Resource typing in Guru}},

@@ -1831,7 +1831,7 @@ year = {2010}

18311831}

18321832@article{fisher2006next,

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

1834−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Fisher, Mandelbaum, Walker - 2010 - The next 700 data description languages.pdf:pdf},

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

18351835journal = {Journal of the ACM},

18361836number = {2},

18371837pages = {1--51},

@@ -1844,7 +1844,7 @@ year = {2010}

18441844@inproceedings{brady2011epic,

18451845author = {Brady, Edwin},

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

1847−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2011 - Epic --- A Library for Generating Compilers.pdf:pdf},

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

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

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

18501850year = {2011}

@@ -1852,7 +1852,7 @@ year = {2011}

18521852@inproceedings{Brady2006b,

18531853author = {Brady, Edwin},

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

1855−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2006 - Ivor, a proof engine.pdf:pdf},

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

18561856isbn = {978-3-540-74129-9},

18571857month = sep,

18581858pages = {145----162},

@@ -1863,7 +1863,7 @@ year = {2006}

18631863@article{Reynolds1972,

18641864abstract = {Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters which are themselves written in a programming language based on the lambda calculus (i.e., an applicative language such as pure LISP). Examples include McCarthy's definition of LISP, Landin's SECD machine, the Vienna definition of PL/I, Reynolds' definitions of GEDANKEN, and recent unpublished work by L. Morris and C. Wadsworth. Such definitions can be classified according to whether the interpreter contains higher-order functions, and whether the order of application (i.e., call-by-value versus call-by-name) in the defined language depends upon the order of application in the defining language. As an example, we consider the definition of a simple applicative programming language by means of an interpreter written in a similar language. Definitions in each of the above classifications are derived from one another by informal but constructive methods. The treatment of imperative features such as jumps and assignment is also discussed.},

18651865author = {Reynolds, John C},

1866−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Reynolds - 1972 - Definitional interpreters for higher-order programming languages.pdf:pdf},

1866+file = {:Users/edwin/Documents/Mendeley Desktop/Reynolds/Definitional interpreters for higher-order programming languages/Reynolds - Definitional interpreters for higher-order programming languages - 1972.pdf:pdf},

18671867journal = {Proceedings of the ACM annual conference on ACM 72},

18681868keywords = {applicative language,closure,continuation,gedanken,higher order function,interpreter,j operator,lambda calculus,language definition,lisp,order application,pal,programming language,reference,secd machine},

18691869number = {30602},

@@ -1876,7 +1876,7 @@ year = {1972}

18761876@book{Hunt,

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

18781878booktitle = {Design},

1879−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},

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

18801880isbn = {020161622X},

18811881title = {{The Pragmatic Programmer Chapter 4}}

18821882}

@@ -1899,7 +1899,7 @@ year = {2004}

18991899}

19001900@article{Swierstra2011,

19011901author = {Swierstra, W},

1902−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Swierstra - 2011 - Sorted Verifying the Problem of the {Dutch National} Flag in {Agda}.pdf:pdf},

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

19031903journal = {Journal of Functional Programming},

19041904number = {6},

19051905pages = {575----583},

@@ -1910,7 +1910,7 @@ year = {2011}

19101910}

19111911@misc{Casinghino2012,

19121912author = {Casinghino, Chris and Sj\"{o}berg, Vilhelm and Weirich, Stephanie},

1913−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Casinghino, Sj{o}berg, Weirich - 2012 - Combining Proofs and Programs in a Dependently Typed Language.pdf:pdf},

1913+file = {:Users/edwin/Documents/Mendeley Desktop/Casinghino, Sj{o}berg, Weirich/Combining Proofs and Programs in a Dependently Typed Language/Casinghino, Sj{o}berg, Weirich - Combining Proofs and Programs in a Dependently Typed Language - 2012.pdf:pdf},

19141914keywords = {dependent types,general recursion,termination},

19151915pages = {1--12},

19161916title = {{Combining Proofs and Programs in a Dependently Typed Language}},

@@ -1918,7 +1918,7 @@ year = {2012}

19181918}

19191919@article{Huet1997,

19201920author = {Huet, G},

1921−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Huet - 1997 - The zipper.pdf:pdf},

1921+file = {:Users/edwin/Documents/Mendeley Desktop/Huet/The zipper/Huet - The zipper - 1997.pdf:pdf},

19221922journal = {{Journal of Functional Programming}},

19231923number = {5},

19241924pages = {549----554},

@@ -1930,7 +1930,7 @@ year = {1997}

19301930@inproceedings{bradyresource,

19311931author = {Brady, Edwin and Hammond, Kevin},

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

1933−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady, Hammond - 2012 - Resource-safe Systems Programming with Embedded Domain Specific Languages.pdf:pdf},

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

19341934pages = {242----257},

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

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

@@ -1938,13 +1938,13 @@ year = {2012}

19381938}

19391939@book{Management,

19401940author = {Totty, Brian and Gourley, David},

1941−file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter4ConnectionManageme.pdf:pdf},

1941+file = {:Users/edwin/Documents/Mendeley Desktop/Totty, Gourley/HTTP The Definitive Guide Chapter 4/Totty, Gourley - HTTP The Definitive Guide Chapter 4 - Unknown.pdf:pdf},

19421942isbn = {1565925092},

19431943title = {{HTTP: The Definitive Guide Chapter 4}}

19441944}

19451945@phdthesis{Brady2005,

19461946author = {Brady, Edwin},

1947−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brady - 2005 - Practical Implementation of a Dependently Typed Functional Programming Language.pdf:pdf},

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

19481948keywords = {Dependent Types},

19491949mendeley-tags = {Dependent Types},

19501950school = {University of Durham},

@@ -1954,7 +1954,7 @@ year = {2005}

19541954@article{Lee2001,

19551955author = {Lee, Chin Soon and Jones, Neil D. and Ben-Amram, Amir M.},

19561956doi = {10.1145/373243.360210},

1957−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Lee, Jones, Ben-Amram - 2001 - The size-change principle for program termination.pdf:pdf},

1957+file = {:Users/edwin/Documents/Mendeley Desktop/Lee, Jones, Ben-Amram/The size-change principle for program termination/Lee, Jones, Ben-Amram - The size-change principle for program termination - 2001.pdf:pdf},

19581958isbn = {1-58113-336-7},

19591959issn = {03621340},

19601960journal = {ACM SIGPLAN Notices},

@@ -1969,13 +1969,13 @@ year = {2001}

19691969}

19701970@misc{Bloat,

19711971author = {Brooks, Fred},

1972−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Brooks - Unknown - The Design of Design Chapter 4.pdf:pdf},

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

19731973isbn = {9780321702081},

19741974title = {{The Design of Design Chapter 4}}

19751975}

19761976@misc{Caldwell,

19771977author = {Caldwell, James and Roan, Ryan},

1978−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Caldwell, Roan - Unknown - Type Checking SQL for Secure Database Access.pdf:pdf},

1978+file = {:Users/edwin/Documents/Mendeley Desktop/Caldwell, Roan/Type Checking SQL for Secure Database Access/Caldwell, Roan - Type Checking SQL for Secure Database Access - Unknown.pdf:pdf},

19791979title = {{Type Checking SQL for Secure Database Access}}

19801980}

19811981@inproceedings{Peterson1993,

@@ -1983,7 +1983,7 @@ address = {New York, New York, USA},

19831983author = {Peterson, John and Jones, Mark},

19841984booktitle = {Proceedings of the ACM SIGPLAN 1993 conference on Programming Language Design and Implementation - PLDI '93},

19851985doi = {10.1145/155090.155112},

1986−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Peterson, Jones - 1993 - Implementing type classes.pdf:pdf},

1986+file = {:Users/edwin/Documents/Mendeley Desktop/Peterson, Jones/Implementing type classes/Peterson, Jones - Implementing type classes - 1993.pdf:pdf},

19871987isbn = {0897915984},

19881988issn = {0362-1340},

19891989month = aug,

@@ -1998,7 +1998,7 @@ year = {1993}

19981998@misc{Attacks2012a,

19991999author = {Anderson, Ross},

20002000doi = {10.1093/epirev/mxr031},

2001−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Anderson - Unknown - Security Engineering Chapter 18.pdf:pdf},

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

20022002isbn = {9780470068526},

20032003issn = {1478-6729},

20042004number = {1},

@@ -2023,7 +2023,7 @@ abstract = {This paper suggests that input and output are basic primitives of pr

20232023author = {Hoare, C A R},

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

20252025editor = {McKeag, R M and Macnaghten, A M},

2026−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hoare - 1978 - Communicating sequential processes.pdf:pdf},

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

20272027isbn = {0131532715},

20282028issn = {01676423},

20292029journal = {Communications of the ACM},

@@ -2039,20 +2039,28 @@ year = {1978}

20392039}

20402040@article{Overview,

20412041author = {Totty, Brian and Gourley, David},

2042−file = {:Users/edwin/Downloads/Safari/HTTPTheDefinitiveGuideChapter1OverviewofHTTP.pdf:pdf},

2042+file = {:Users/edwin/Documents/Mendeley Desktop/Totty, Gourley/HTTP The Definitive Guide Chapter 1/Totty, Gourley - HTTP The Definitive Guide Chapter 1 - Unknown.pdf:pdf},

20432043isbn = {1565925092},

20442044title = {{HTTP: The Definitive Guide Chapter 1}}

20452045}

2046+@inproceedings{Sozeau2008,

2047+author = {Sozeau, Matthieu and Oury, Nicolas},

2048+booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs 2008})},

2049+file = {:Users/edwin/Documents/Mendeley Desktop/Sozeau, Oury/First-Class Type Classes/Sozeau, Oury - First-Class Type Classes - 2008.pdf:pdf},

2050+pages = {278----293},

2051+title = {{First-Class Type Classes}},

2052+year = {2008}

2053+}

20462054@book{Fogel,

20472055author = {Fogel, Karl},

2048−file = {:Users/edwin/Downloads/Books/producingoss.pdf:pdf},

2056+file = {:Users/edwin/Documents/Mendeley Desktop/Fogel/Producing Open Source Software How to Run a Successful Free Software Project/Fogel - Producing Open Source Software How to Run a Successful Free Software Project - Unknown.pdf:pdf},

20492057title = {{Producing Open Source Software: How to Run a Successful Free Software Project}}

20502058}

20512059@book{Brady2012,

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

20532061booktitle = {Carcinogenesis},

20542062doi = {10.1093/carcin/bgs054},

2055−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},

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

20562064isbn = {020161622X},

20572065issn = {1460-2180},

20582066number = {3},

@@ -2064,7 +2072,7 @@ volume = {33}

20642072@inproceedings{augustsson2008paradise,

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

20662074booktitle = {International Conference on Functional Programming},

2067−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Augustsson, Mansell, Sittampalam - 2008 - Paradise a two-stage DSL embedded in Haskell.pdf:pdf},

2075+file = {:Users/edwin/Documents/Mendeley Desktop/Augustsson, Mansell, Sittampalam/Paradise a two-stage DSL embedded in Haskell/Augustsson, Mansell, Sittampalam - Paradise a two-stage DSL embedded in Haskell - 2008.pdf:pdf},

20682076number = {9},

20692077pages = {225--228},

20702078publisher = {ACM},

@@ -2075,7 +2083,7 @@ year = {2008}

20752083}

20762084@article{marlow2006making,

20772085author = {Marlow, S. and {Peyton Jones}, S.},

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

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

20792087journal = {Journal of Functional Programming},

20802088number = {4-5},

20812089pages = {415--449},

@@ -2090,7 +2098,7 @@ abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your pe

20902098address = {London},

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

20922100booktitle = {Mendeley Desktop},

2093−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/The Mendeley Support Team - 2011 - Getting Started with Mendeley.pdf:pdf},

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

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

20952103pages = {1--16},

20962104publisher = {Mendeley Ltd.},

@@ -2111,7 +2119,7 @@ year = {2011}

21112119author = {Abelson, Harold and Sussman, Gerald and Sussman, Julie},

21122120booktitle = {Computer Music Journal},

21132121doi = {10.2307/3679579},

2114−file = {:Users/edwin/Downloads/sicp.pdf:pdf},

2122+file = {:Users/edwin/Documents/Mendeley Desktop/Abelson, Sussman, Sussman/Structure and Interpretation of Computer Programs/Abelson, Sussman, Sussman - Structure and Interpretation of Computer Programs - 1985.pdf:pdf},

21152123isbn = {0262011530},

21162124issn = {01489267},

21172125month = jan,

@@ -2155,7 +2163,7 @@ p14 The last paragraph appears to be largely a comment to the present referees!

21552163

21562164 },

21572165author = {Bird, Richard S},

2158−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Bird - 2012 - An in-situ algorithm for expanding a graph.pdf:pdf},

2166+file = {:Users/edwin/Documents/Mendeley Desktop/Bird/An in-situ algorithm for expanding a graph/Bird - An in-situ algorithm for expanding a graph - 2012(2).pdf:pdf},

21592167journal = {Journal of Functional Programming},

21602168keywords = {a href,journal of functional programming},

21612169title = {{An in-situ algorithm for expanding a graph}},

@@ -2185,13 +2193,13 @@ Minor comments:

21852193

21862194Fig 1,2 and 3 - I'm not sure I would like the rotation of these in print (it's pretty awkward on screen too).},

21872195author = {Ahn, Ki Yung and Sheard, Tim and Fiore, Marcelo and Pitts, Andrew M},

2188−file = {:Users/edwin/Dropbox/Reviewing/IFL12/submissions/ifl2012_submission_28.pdf:pdf},

2196+file = {:Users/edwin/Documents/Mendeley Desktop/Ahn et al/Programming with Term-Indexed Types in Nax/Ahn et al. - Programming with Term-Indexed Types in Nax - Unknown.pdf:pdf},

21892197keywords = {gadts,indexed datatypes,lightweight dependent types,term-indexed types,universe polymorphism,universe subtyping},

21902198title = {{Programming with Term-Indexed Types in Nax}}

21912199}

21922200@article{Morrisett1999,

21932201author = {Morrisett, G and Walker, D},

2194−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Morrisett, Walker - 1999 - From System F to typed assembly language.pdf:pdf},

2202+file = {:Users/edwin/Documents/Mendeley Desktop/Morrisett, Walker/From System F to typed assembly language/Morrisett, Walker - From System F to typed assembly language - 1999.pdf:pdf},

21952203journal = {ACM Transactions on \ldots},

21962204title = {{From System F to typed assembly language}},

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

@@ -2200,7 +2208,7 @@ year = {1999}

22002208@article{Altenkirch2010a,

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

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

2203−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Altenkirch, Mcbride, Morris - 2010 - Generic Programming with Dependent Types.pdf:pdf},

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

22042212journal = {Citeseer},

22052213publisher = {Citeseer},

22062214title = {{Generic Programming with Dependent Types}},

@@ -2211,7 +2219,7 @@ year = {2010}

22112219author = {Pfleeger, Charles P and Pfleeger, S. L.},

22122220booktitle = {Nicotine & tobacco research : official journal of the Society for Research on Nicotine and Tobacco},

22132221doi = {10.1093/ntr/nts035},

2214−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pfleeger, Pfleeger - 2012 - Security in Computer Chapter 12.pdf:pdf},

2222+file = {:Users/edwin/Documents/Mendeley Desktop/Pfleeger, Pfleeger/Security in Computer Chapter 12/Pfleeger, Pfleeger - Security in Computer Chapter 12 - 2012.pdf:pdf},

22152223isbn = {0132390779},

22162224issn = {1469-994X},

22172225month = oct,

@@ -2226,7 +2234,7 @@ year = {2012}

22262234@book{Pierce2004,

22272235author = {Pierce, Benjamin},

22282236editor = {Pierce, Benjamin},

2229−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pierce - 2004 - Advanced topics in types and programming languages.pdf:pdf},

2237+file = {:Users/edwin/Documents/Mendeley Desktop/Pierce/Advanced topics in types and programming languages/Pierce - Advanced topics in types and programming languages - 2004.pdf:pdf},

22302238publisher = {MIT Press},

22312239title = {{Advanced topics in types and programming languages}},

22322240year = {2004}

@@ -2244,14 +2252,14 @@ year = {1997}

22442252}

22452253@misc{Lorenzen,

22462254author = {Lorenzen, Florian},

2247−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Lorenzen - Unknown - A Statically Typed Functional Language With Programmable Binders.pdf:pdf},

2255+file = {:Users/edwin/Documents/Mendeley Desktop/Lorenzen/A Statically Typed Functional Language With Programmable Binders/Lorenzen - A Statically Typed Functional Language With Programmable Binders - Unknown.pdf:pdf},

22482256title = {{A Statically Typed Functional Language With Programmable Binders}}

22492257}

22502258@book{The2012,

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

22522260booktitle = {Carcinogenesis},

22532261doi = {10.1093/carcin/bgs054},

2254−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},

2262+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/The Pragmatic Programmer Chapter 3/Hunt, Thomas - The Pragmatic Programmer Chapter 3 - Unknown.pdf:pdf},

22552263isbn = {020161622X},

22562264issn = {1460-2180},

22572265number = {3},

@@ -2263,7 +2271,7 @@ volume = {33}

22632271@inproceedings{pollack1990implicit,

22642272author = {Pollack, R.},

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

2266−file = {:Users/edwin/Library/Application Support/Mendeley Desktop/Downloaded/Pollack - 1990 - Implicit syntax.pdf:pdf},

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

22672275publisher = {Citeseer},

22682276title = {{Implicit syntax}},

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

@@ -2271,7 +2279,7 @@ year = {1990}

22712279}

22722280@article{Bradya,

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

2274−file = {:Users/edwin/Downloads/Safari/ThePragmaticProgrammerFromJourneymantoMasterChapter7BeforetheProject.pdf:pdf},

2282+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/The Pragmatic Programmer Chapter 7/Hunt, Thomas - The Pragmatic Programmer Chapter 7 - Unknown.pdf:pdf},

22752283isbn = {020161622X},

22762284title = {{The Pragmatic Programmer Chapter 7}}

22772285}