@@ -1,12 +1,24 @@
11Automatically generated by Mendeley 1.3.1
22Any changes to this file will be lost if it is regenerated by Mendeley.
33
4−@misc{idristutorial,
5−author = {Brady, Edwin},
6−file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
7−title = {{Programming in Idris : a tutorial}},
8−url = {http://idris-lang.org/tutorial},
9−year = {2012}
4+@inproceedings{pj2006gadts,
5+author = {{Peyton Jones}, S. and Vytiniotis, D. and Weirich, S. and Washburn, G.},
6+booktitle = {{International Conference on Functional Programming} ({ICFP} '06)},
7+file = {:Users/edwin/Documents/Mendeley Desktop/Peyton Jones et al/Peyton Jones et al. - 2006 - Simple unification-based type inference for GADTs.pdf:pdf},
8+number = {9},
9+pages = {50--61},
10+publisher = {ACM},
11+title = {{Simple unification-based type inference for GADTs}},
12+url = {http://dl.acm.org/citation.cfm?id=1159811},
13+volume = {41},
14+year = {2006}
15+}
16+@book{Hunt,
17+author = {Hunt, Andrew and Thomas, David},
18+booktitle = {Design},
19+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 4.pdf:pdf},
20+isbn = {020161622X},
21+title = {{The Pragmatic Programmer Chapter 4}}
1022}
1123@inproceedings{Brady2010,
1224author = {Brady, Edwin and Hammond, Kevin},
@@ -124,6 +136,13 @@ url = {http://www.scopus.com/inward/record.url?eid=2-s2.0-67650032847&partnerID=
124136volume = {43},
125137year = {2008}
126138}
139+@book{luo1994,
140+author = {Luo, Z.},
141+publisher = {Oxford University Press, Inc.},
142+title = {{Computation and reasoning: a type theory for computer science}},
143+url = {http://dl.acm.org/citation.cfm?id=SERIES9893.184757},
144+year = {1994}
145+}
127146@article{mccann2000packet,
128147author = {McCann, P.J. and Chandra, S.},
129148journal = {ACM SIGCOMM Computer Communication Review},
@@ -200,6 +219,19 @@ url = {http://www.springerlink.com/index/1039q8qk71257677.pdf},
200219volume = {5520},
201220year = {2008}
202221}
222+@book{While2012,
223+author = {Hunt, Andrew and Thomas, David},
224+booktitle = {Carcinogenesis},
225+doi = {10.1093/carcin/bgs054},
226+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 6.pdf:pdf},
227+isbn = {020161622X},
228+issn = {1460-2180},
229+number = {3},
230+pmid = {22383472},
231+title = {{The Pragmatic Programmer Chapter 6}},
232+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
233+volume = {33}
234+}
203235@inproceedings{madhavapeddy2010turning,
204236author = {Madhavapeddy, A. and Mortier, R. and Sohan, R. and Gazagnaire, T. and Hand, S. and Deegan, T. and McAuley, D. and Crowcroft, J.},
205237booktitle = {Proceedings of the 2nd USENIX conference on Hot topics in cloud computing},
@@ -312,10 +344,19 @@ url = {http://journals.cambridge.org/abstract_S0956796811000207},
312344volume = {21},
313345year = {2011}
314346}
347+@inproceedings{pollack1990implicit,
348+author = {Pollack, R.},
349+booktitle = {Informal Proceedings of First Workshop on Logical Frameworks, Antibes},
350+file = {:Users/edwin/Documents/Mendeley Desktop/Pollack/Pollack - 1990 - Implicit syntax.pdf:pdf},
351+publisher = {Citeseer},
352+title = {{Implicit syntax}},
353+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.30.7361&rep=rep1&type=pdf},
354+year = {1990}
355+}
315356@inproceedings{Sculthorpe2009,
316357author = {Sculthorpe, Neil and Nilsson, Henrik},
317358booktitle = {International Conference on Functional Programming ({ICFP} '09)},
318−file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf},
359+file = {:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types.pdf:pdf;:Users/edwin/Documents/Mendeley Desktop/Sculthorpe, Nilsson/Sculthorpe, Nilsson - 2009 - Safe functional reactive programming through dependent types(2).pdf:pdf},
319360title = {{Safe functional reactive programming through dependent types}},
320361url = {http://dl.acm.org/citation.cfm?id=1596558},
321362year = {2009}
@@ -357,6 +398,17 @@ title = {{Epigram Reloaded: A Standalone Typechecker for {ETT}}},
357398url = {http://books.google.co.uk/books?hl=en&lr=&id=p0yV1sHLubcC&oi=fnd&pg=PA79&dq=epigram+reloaded&ots=x50ou0VMsm&sig=7TjAGohIatNLTWsHcuNcK5hEGGY},
358399year = {2005}
359400}
401+@article{dybjer1994inductive,
402+author = {Dybjer, P.},
403+journal = {Formal aspects of computing},
404+number = {4},
405+pages = {440--465},
406+publisher = {Springer},
407+title = {{Inductive families}},
408+url = {http://www.springerlink.com/index/J17824H467X6J288.pdf},
409+volume = {6},
410+year = {1994}
411+}
360412@article{Hughes1989,
361413abstract = {As software becomes more and more complex, it is more and more important to structure it well. Well-structured software is easy to write, easy to debug, and provides a collection of modules that can be re-used to reduce future programming costs. Conventional languages place conceptual limits on the way problems can be modularised. Functional languages push those limits back. In this paper we show that two features of functional languages in particular, higher-order functions and lazy evaluation, can contribute greatly to modularity. As examples, we manipulate lists and trees, program several numerical algorithms, and implement the alpha-beta heuristic (an algorithm from Artificial Intelligence used in game-playing programs). Since modularity is the key to successful programming, functional languages are vitally important to the real world.},
362414author = {Hughes, J},
@@ -414,6 +466,19 @@ title = {{Dependently typed functional programs and their proofs}},
414466url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.4785&rep=rep1&type=pdf},
415467year = {1999}
416468}
469+@book{The2012,
470+author = {Hunt, Andrew and Thomas, David},
471+booktitle = {Carcinogenesis},
472+doi = {10.1093/carcin/bgs054},
473+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 3.pdf:pdf},
474+isbn = {020161622X},
475+issn = {1460-2180},
476+number = {3},
477+pmid = {22383472},
478+title = {{The Pragmatic Programmer Chapter 3}},
479+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
480+volume = {33}
481+}
417482@inproceedings{oury2008power,
418483author = {Oury, N. and Swierstra, W.},
419484booktitle = {International Conference on Functional Programming},
@@ -591,6 +656,19 @@ url = {http://dl.acm.org/citation.cfm?id=1111039},
591656volume = {15},
592657year = {2010}
593658}
659+@book{Brady2012,
660+author = {Hunt, Andrew and Thomas, David},
661+booktitle = {Carcinogenesis},
662+doi = {10.1093/carcin/bgs054},
663+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 5.pdf:pdf},
664+isbn = {020161622X},
665+issn = {1460-2180},
666+number = {3},
667+pmid = {22383472},
668+title = {{The Pragmatic Programmer Chapter 5}},
669+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
670+volume = {33}
671+}
594672@inproceedings{Wadler1989,
595673abstract = {From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds' abstraction theorem for the polymorphic lambda calculus.},
596674author = {Wadler, Philip},
@@ -625,6 +703,19 @@ title = {{The implicit calculus of constructions as a programming language with
625703url = {http://www.springerlink.com/index/m84h82904546l265.pdf},
626704year = {2008}
627705}
706+@book{Philosophy2012,
707+author = {Hunt, Andrew and Thomas, David},
708+booktitle = {Carcinogenesis},
709+doi = {10.1093/carcin/bgs054},
710+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 1.pdf:pdf},
711+isbn = {020161622X},
712+issn = {1460-2180},
713+number = {3},
714+pmid = {22383472},
715+title = {{The Pragmatic Programmer Chapter 1}},
716+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
717+volume = {33}
718+}
628719@article{landin1966next,
629720author = {Landin, P.J.},
630721file = {:Users/edwin/Documents/Mendeley Desktop/Landin/Landin - 1966 - The next 700 programming languages.pdf:pdf},
@@ -646,6 +737,19 @@ issn = {1478-6729},
646737pmid = {22215642},
647738title = {{The Design of Design Chapter 2}}
648739}
740+@book{Approach2012,
741+author = {Hunt, Andrew and Thomas, David},
742+booktitle = {Carcinogenesis},
743+doi = {10.1093/carcin/bgs054},
744+file = {:Users/edwin/Documents/Mendeley Desktop/Hunt, Thomas/Hunt, Thomas - Unknown - The Pragmatic Programmer Chapter 2.pdf:pdf},
745+isbn = {020161622X},
746+issn = {1460-2180},
747+number = {3},
748+pmid = {22383472},
749+title = {{The Pragmatic Programmer Chapter 2}},
750+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
751+volume = {33}
752+}
649753@inproceedings{Brady2003,
650754author = {Brady, Edwin and McBride, Conor and McKinna, James},
651755booktitle = {Types for Proofs and Programs},
@@ -665,6 +769,13 @@ issn = {1478-6729},
665769pmid = {22215642},
666770title = {{The Design of Design Chapter 3}}
667771}
772+@book{Fowler,
773+author = {Fowler, Martin},
774+booktitle = {Language},
775+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 2.pdf:pdf},
776+isbn = {9780132107549},
777+title = {{Domain Specific Languages Chapter 2}}
778+}
668779@article{Abel2010,
669780abstract = {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.},
670781author = {Abel, Andreas},
@@ -766,6 +877,13 @@ title = {{Idris --- Systems Programming Meets Full Dependent Types}},
766877url = {http://dl.acm.org/citation.cfm?id=1929529.1929536},
767878year = {2011}
768879}
880+@misc{idristutorial,
881+author = {Brady, Edwin},
882+file = {:Users/edwin/Documents/Mendeley Desktop/Brady/Brady - 2012 - Programming in Idris a tutorial.pdf:pdf},
883+title = {{Programming in Idris : a tutorial}},
884+url = {http://idris-lang.org/tutorial},
885+year = {2012}
886+}
769887@article{Steiner1988,
770888author = {Steiner, JG},
771889file = {:Users/edwin/Documents/Mendeley Desktop/Steiner/Steiner - 1988 - Kerberos An authentication service for open network systems.pdf:pdf},
@@ -782,6 +900,19 @@ title = {{Cryptographic verification by typing for a sample protocol implementat
782900url = {http://www.springerlink.com/index/V168041M46658R73.pdf},
783901year = {2010}
784902}
903+@book{An2012,
904+author = {Fowler, Martin},
905+booktitle = {Carcinogenesis},
906+doi = {10.1093/carcin/bgs054},
907+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 1.pdf:pdf},
908+isbn = {9780132107549},
909+issn = {1460-2180},
910+number = {3},
911+pmid = {22383472},
912+title = {{Domain Specific Languages Chapter 1}},
913+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
914+volume = {33}
915+}
785916@inproceedings{augustsson2008paradise,
786917author = {Augustsson, L. and Mansell, H. and Sittampalam, G.},
787918booktitle = {International Conference on Functional Programming},
@@ -1023,6 +1154,19 @@ pmid = {22215642},
10231154title = {{Security Engineering Chapter 18}},
10241155volume = {34}
10251156}
1157+@book{Choosing2012,
1158+author = {Fowler, Martin},
1159+booktitle = {Carcinogenesis},
1160+doi = {10.1093/carcin/bgs054},
1161+file = {:Users/edwin/Documents/Mendeley Desktop/Fowler/Fowler - Unknown - Domain Specific Languages Chapter 6.pdf:pdf},
1162+isbn = {9780132107549},
1163+issn = {1460-2180},
1164+number = {3},
1165+pmid = {22383472},
1166+title = {{Domain Specific Languages Chapter 6}},
1167+url = {http://www.ncbi.nlm.nih.gov/pubmed/22383472},
1168+volume = {33}
1169+}
10261170@article{Xi1998,
10271171abstract = {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.},
10281172author = {Xi, Hongwei and Pfenning, Frank},