diff options
Diffstat (limited to 'thesis.bib')
-rw-r--r-- | thesis.bib | 314 |
1 files changed, 314 insertions, 0 deletions
diff --git a/thesis.bib b/thesis.bib new file mode 100644 index 0000000..9519f9f --- /dev/null +++ b/thesis.bib @@ -0,0 +1,314 @@ +@inbook{Thompson1991, + author = {Thompson, Simon}, + title = {Type Theory and Functional Programming}, + publisher = {Addison-Wesley}, + year = {1991} +} + +@inbook{Pierce2002, + author = {Pierce, Benjamin C.}, + title = {Types and Programming Languages}, + publisher = {The MIT Press}, + year = {2002} +} + +@online{Coq, + author = {{The Coq Team}}, + title = {The Coq Proof Assistant}, + url = {\url{coq.inria.fr}}, + howpublished = {\url{http://coq.inria.fr}}, + year = 2013 +} + +@online{GHC, + author = {{The GHC Team}}, + title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1}, + url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/}, + howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}}, + year = 2012 +} + +@online{EpigramTut, + author = {Conor McBride}, + title = {Epigram: Practical Programming with Dependent Types}, + url = {http://strictlypositive.org/epigram-notes.ps.gz}, + howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}}, + year = 2004 +} + +@online{Haskell2010, + author = {Simon Marlow}, + title = {Haskell 2010, Language Report}, + url = {http://www.haskell.org/onlinereport/haskell2010/}, + howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}}, + year = 2010 +} + +@online{LYAH, + author = {Miran Lipova\v{c}a}, + title = {Learn You a Haskell for Great Good!}, + url = {http://learnyouahaskell.com/}, + howpublished = {\url{http://learnyouahaskell.com/}}, + year = 2009 +} + +@inbook{ProgInHask, + author = {Graham Hutton}, + title = {Programming in Haskell}, + year = 2007, + publisher = {Cambridge University Press} +} + +@inbook{NuPRL, + author = {Robert L. Constable and the PRL Group}, + title = {Implementing Mathematics with The NuPRL Proof Development System}, + year = 1986, + publisher = Prentice-Hall +} + + +@article{Altenkirch2010, +author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas}, +file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf}, +journal = {Functional and Logic \ldots}, +number = {Sheard 2005}, +title = {{$\Pi$$\Sigma$: dependent types without the sugar}}, +url = {http://www.springerlink.com/index/91W712G2806R575H.pdf}, +year = {2010} +} +@article{Altenkirch2007, +address = {New York, New York, USA}, +author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter}, +doi = {10.1145/1292597.1292608}, +file = {:home/bitonic/docs/papers/OTT2.pdf:pdf}, +isbn = {9781595936776}, +journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07}, +keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory}, +pages = {57}, +publisher = {ACM Press}, +title = {{Observational equality, now!}}, +url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608}, +year = {2007} +} +@article{Barendregt1991, +author = {Barendregt, Henk}, +file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf}, +journal = {Journal of functional programming}, +title = {{Introduction to generalized type systems}}, +url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf}, +year = {1991} +} +@article{Bove2009, +author = {Bove, Ana and Dybjer, Peter and Norell, Ulf}, +file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf}, +journal = {Theorem Proving in Higher Order Logics}, +title = {{A brief overview of Agda - a functional language with dependent types}}, +url = {http://www.springerlink.com/index/h12lq70470983732.pdf}, +year = {2009} +} +@article{Brady2012, +author = {Brady, Edwin}, +file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf}, +journal = {Unpublished draft}, +number = {November}, +title = {{Implementing General Purpose Dependently Typed Programming Languages}}, +url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf}, +year = {2012} +} +@article{Chapman2010, +address = {New York, New York, USA}, +author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter}, +doi = {10.1145/1863543.1863547}, +file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf}, +isbn = {9781605587943}, +journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10}, +pages = {3}, +publisher = {ACM Press}, +title = {{The gentle art of levitation}}, +url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547}, +year = {2010} +} +@article{Church1936, +author = {Church, Alonzo}, +file = {:home/bitonic/docs/papers/church-lc.pdf:pdf}, +journal = {American journal of mathematics}, +number = {2}, +pages = {345--363}, +title = {{An unsolvable problem of elementary number theory}}, +url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045}, +volume = {58}, +year = {1936} +} +@article{Church1940, +author = {Church, Alonzo}, +file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf}, +journal = {J. Symb. Log.}, +number = {2}, +pages = {56--68}, +title = {{A formulation of the simple theory of types}}, +url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170}, +volume = {5}, +year = {1940} +} +@article{Coquand1986, +author = {Coquand, Thierry and Huet, Gerard}, +file = {:home/bitonic/docs/papers/coc.pdf:pdf}, +title = {{The calculus of constructions}}, +url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf}, +year = {1986} +} +@article{Curry1934, +author = {Curry, Haskell B.}, +file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf}, +journal = {Proceedings of the National Academy of Sciences of the United States of America}, +number = {1930}, +pages = {584--590}, +title = {{Functionality in combinatory logic}}, +url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/}, +volume = {511}, +year = {1934} +} +@article{Dybjer1991, +author = {Dybjer, Peter}, +file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps}, +journal = {Logical Frameworks}, +title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}}, +url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats}, +year = {1991} +} +@article{Hurkens1995, +author = {Hurkens, Antonius J.C.}, +file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf}, +journal = {Typed Lambda Calculi and Applications}, +title = {{A simplification of Girard's paradox}}, +url = {http://www.springerlink.com/index/W718604JN467672H.pdf}, +year = {1995} +} +@article{Jacobs1997, +author = {Jacobs, Bart and Rutten, Jan}, +file = {:home/bitonic/docs/papers/coalgebra-coind.pdf:pdf}, +journal = {EATCS Bulletin}, +number = {1997}, +title = {{A tutorial on (co) algebras and (co) induction}}, +url = {http://synrc.com/publications/cat/Logic/CoinductionCoalgebrasTutorial.pdf}, +volume = {62}, +year = {1997} +} +@book{Martin-Lof1984, +author = {Martin-L\"{o}f, Per}, +file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf}, +isbn = {8870881059}, +publisher = {Bibliopolis}, +title = {{Intuitionistic type theory}}, +year = {1984} +} +@article{McBride2004, +author = {McBride, Conor}, +doi = {10.1017/S0956796803004829}, +file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz}, +journal = {Journal of Functional Programming}, +month = jan, +number = {1}, +pages = {69--111}, +title = {{The View from The Left}}, +url = {http://strictlypositive.org/view.ps.gz}, +volume = {14}, +year = {2004} +} +@phdthesis{Norell2007, +author = {Norell, Ulf}, +file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf}, +isbn = {9789172919969}, +school = {Chalmers University of Technology and G\"{o}teborg University}, +title = {{Towards a practical programming language based on dependent type theory}}, +url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf}, +year = {2007} +} +@article{Oury2008, +address = {New York, New York, USA}, +author = {Oury, Nicolas and Swierstra, Wouter}, +doi = {10.1145/1411204.1411213}, +file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf}, +isbn = {9781595939197}, +journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08}, +pages = {39}, +publisher = {ACM Press}, +title = {{The power of Pi}}, +url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213}, +year = {2008} +} +@article{Pierce2000, +author = {Pierce, Benjamin C. and Turner, David N.}, +doi = {10.1145/345099.345100}, +file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf}, +issn = {01640925}, +journal = {ACM Transactions on Programming Languages and Systems}, +month = jan, +number = {1}, +pages = {1--44}, +title = {{Local type inference}}, +url = {http://portal.acm.org/citation.cfm?doid=345099.345100}, +volume = {22}, +year = {2000} +} +@article{Pollack1990, +author = {Pollack, Robert}, +file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps}, +journal = {Informal Proceedings of First Workshop on Logical Frameworks}, +title = {{Implicit syntax}}, +url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf}, +year = {1992} +} +@article{Reynolds1994, +author = {Reynolds, John C.}, +file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps}, +journal = {Logical Foundations of Functional Programming}, +title = {{An introduction to the polymorphic lambda calculus}}, +url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf}, +year = {1994} +} +@article{Sulzmann2007, +address = {New York, New York, USA}, +author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin}, +doi = {10.1145/1190315.1190324}, +file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf}, +isbn = {159593393X}, +journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07}, +pages = {53}, +publisher = {ACM Press}, +title = {{System F with type equality coercions}}, +url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324}, +year = {2007} +} +@article{Vytiniotis2011, +author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin}, +file = {:home/bitonic/docs/papers/outsidein.pdf:pdf}, +journal = {Journal of Functional Programming}, +number = {4-5}, +pages = {333--412}, +title = {{OutsideIn (X) Modular type inference with local assumptions}}, +url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818}, +volume = {21}, +year = {2011} +} +@article{Yorgey2012, +address = {New York, New York, USA}, +author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro}, +doi = {10.1145/2103786.2103795}, +file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf}, +isbn = {9781450311205}, +journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12}, +pages = {53}, +publisher = {ACM Press}, +title = {{Giving Haskell a promotion}}, +url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795}, +year = {2012} +} +@phdthesis{McBride1999, +author = {McBride, Conor}, +file = {:home/bitonic/docs/papers/conorthesis.pdf:pdf}, +school = {University of Edinburgh}, +title = {{Dependently typed functional programs and their proofs}}, +url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374}, +year = {1999} +} |