From ebdf439a201d6fda0780284fc7f49b1f8deb88ab Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Sat, 22 Jun 2013 17:06:40 +0100 Subject: ... --- final.bib | 652 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 652 insertions(+) create mode 100644 final.bib (limited to 'final.bib') diff --git a/final.bib b/final.bib new file mode 100644 index 0000000..f58ff07 --- /dev/null +++ b/final.bib @@ -0,0 +1,652 @@ +@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} +} + +@inbook{Queinnec2003, + author = {Christian Queinnec}, + title = {Lisp in Small Pieces}, + publisher = {Cambridge University Press}, + year = {2003}, +} + +@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.3}, + url = {http://www.haskell.org/ghc/docs/latest/html/users_guide/}, + howpublished = {\url{http://www.haskell.org/ghc/docs/7.6.3/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, Nils Anders and L\"{o}h, Andres and Oury, Nicolas}, +file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf}, +journal = {Functional and Logic Programming}, +pages = {40--55}, +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{Brady2013, +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 = {2013} +} +@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, + journal = {{J}ournal of {F}unctional {P}rogramming}, + pages = {69--111}, + number = {1}, + volume = {14}, + title = {The view from the left}, + year = {2004}, + author = {C. McBride and J. McKinna} +} + +@phdthesis{Gimenez1996, +author={Giménez, Eduardo}, +title={Un calcul de constructions infinies et son application {\`a} la v{\'e}rification de syst{\`e}mes communicants}, +school = {Ecole Normale Sup{\'e}rieure de Lyon}, +year = 1996 +} + +@phdthesis{McBride1999, +author = {McBride, Conor}, +file = {:home/bitonic/.local/share/data/Mendeley Ltd./Mendeley Desktop/Downloaded/McBride - 1999 - Dependently typed functional programs and their proofs.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} +} +@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{Tait1967, +author = {Tait, William W.}, +file = {:home/bitonic/docs/papers/tait-normalising.pdf:pdf}, +journal = {The Journal of Symbolic Logic}, +number = {2}, +pages = {198--212}, +title = {{Intensional Interpretations of Functionals of Finite Type}}, +volume = {32}, +year = {1967} +} +@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} +} + +@ARTICLE{Loh2010, + author = {Andres L{\"o}h and Conor McBride and Wouter Swierstra}, + title = {A Tutorial Implementation of a Dependently Typed Lambda Calculus}, + journal = {Fundam. Inform.}, + year = {2010}, + volume = {102}, + pages = {177-207}, + number = {2}, + bibsource = {DBLP, http://dblp.uni-trier.de}, + ee = {http://dx.doi.org/10.3233/FI-2010-304}, + file = {:home/bitonic/docs/papers/simply-easy.pdf:pdf}, + owner = {bitonic} +} + +@ARTICLE{Bruijn91, + author = {de Bruijn, Nicolaas Govert}, + title = {Telescopic mappings in typed lambda calculus}, + journal = {Information and Computation}, + year = {1991}, + volume = {91}, + pages = {189--204}, + number = {2}, + file = {:/home/bitonic/docs/papers/telescopes.pdf:PDF}, + publisher = {Elsevier} +} + +@UNPUBLISHED{Huet1988, + author = {Huet, Gerard P.}, + title = {Extending The Calculus of Constructions with Type:Type}, + note = {Unpublished draft}, + year = {1988}, + file = {:home/bitonic/docs/papers/huet-typtyp.pdf:pdf}, + owner = {bitonic}, + timestamp = {2013.06.10} +} + +@ARTICLE{Harper1991, + author = {Harper, Robert and Pollack, Robert}, + title = {Type checking with universes}, + journal = {Theoretical computer science}, + year = {1991}, + volume = {89}, + pages = {107--136}, + number = {1}, + file = {:/home/bitonic/docs/papers/type-checking-universes.ps.gz:PostScript}, + publisher = {Elsevier} +} + +@ARTICLE{Jacobs1994, + author = {Jacobs, Bart}, + title = {Quotients in Simple Type Theory}, + journal = {Manuscript, Math. Inst}, + year = {1994} +} + +@inproceedings{Hofmann1994, + title={The groupoid model refutes uniqueness of identity proofs}, + author={Hofmann, Martin and Streicher, Thomas}, + booktitle={Logic in Computer Science, 1994. LICS'94. Proceedings., Symposium on}, + pages={208--212}, + year={1994}, + organization={IEEE} +} + +@INPROCEEDINGS{Coquand1992, + author = {Coquand, Thierry}, + title = {Pattern matching with dependent types}, + booktitle = {Informal proceedings of Logical Frameworks}, + year = {1992}, + volume = {92}, + pages = {66--79}, + file = {:/home/bitonic/docs/papers/coquand-pattern.ps:PostScript} +} + +@INPROCEEDINGS{Abel2007, + author = {Abel, Andreas and Coquand, Thierry and Dybjer, Peter}, + title = {Normalization by evaluation for Martin-Lof type theory with typed + equality judgements}, + booktitle = {Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium + on}, + year = {2007}, + pages = {3--12}, + organization = {IEEE}, + file = {:/home/bitonic/docs/papers/nbe.pdf:PDF} +} + +@inproceedings{McBride2004b, + title={I am not a number: I am a free variable}, + author={McBride, Conor and McKinna, James}, + booktitle={Proceedings of the ACM SIGPLAN Haskell Workshop}, + year={2004}, +} + +@article{Bird1999, + title={De Bruijn notation as a nested datatype}, + author={Richard S. Bird and Ross Paterson}, + journal={J. Functional Programming}, + volume={9}, + number={1}, + pages={77--91}, + year={1999}, + publisher={Cambridge Univ Press} +} + +@inproceedings{de1972lambda, + title={Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem}, + author={de Bruijn, Nicolaas Govert}, + booktitle={Indagationes Mathematicae (Proceedings)}, + volume={75}, + number={5}, + pages={381--392}, + year={1972}, + organization={Elsevier} +} + +@article{henglein1993type, + title={Type inference with polymorphic recursion}, + author={Henglein, Fritz}, + journal={ACM Transactions on Programming Languages and Systems (TOPLAS)}, + volume={15}, + number={2}, + pages={253--289}, + year={1993}, + publisher={ACM} +} + +@inproceedings{weirich2011binders, + title={Binders unbound}, + author={Weirich, Stephanie and Yorgey, Brent A and Sheard, Tim}, + booktitle={ACM SIGPLAN Notices}, + volume={46}, + number={9}, + pages={333--345}, + year={2011}, + organization={ACM} +} + +@inproceedings{King1995, + title={Structuring depth-first search algorithms in Haskell}, + author={King, David J and Launchbury, John}, + booktitle={Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + pages={344--354}, + year={1995}, + organization={ACM} +} + +@article{milner1978theory, + title={A theory of type polymorphism in programming}, + author={Milner, Robin}, + journal={Journal of computer and system sciences}, + volume={17}, + number={3}, + pages={348--375}, + year={1978}, + publisher={Elsevier} +} + +@article{dagand2012elaborating, + title={Elaborating inductive definitions}, + author={Dagand, Pierre-Evariste and McBride, Conor}, + journal={arXiv preprint arXiv:1210.6390}, + year={2012} +} + +@inproceedings{chapman2010gentle, + title={The gentle art of levitation}, + author={Chapman, James and Dagand, Pierre-{\'E}variste and McBride, Conor and Morris, Peter}, + booktitle={ACM Sigplan Notices}, + volume={45}, + number={9}, + pages={3--14}, + year={2010}, + organization={ACM} +} + +@article{dybjer2000general, + title={A general formulation of simultaneous inductive-recursive definitions in type theory}, + author={Dybjer, Peter}, + journal={Journal of Symbolic Logic}, + pages={525--549}, + year={2000}, + publisher={JSTOR} +} + +@inproceedings{chakravarty2005associated, + title={Associated types with class}, + author={Chakravarty, Manuel MT and Keller, Gabriele and Jones, Simon Peyton and Marlow, Simon}, + booktitle={ACM SIGPLAN Notices}, + volume={40}, + number={1}, + pages={1--13}, + year={2005}, + organization={ACM} +} + +@article{miller1992unification, + title={Unification under a mixed prefix}, + author={Miller, Dale}, + journal={Journal of symbolic computation}, + volume={14}, + number={4}, + pages={321--358}, + year={1992}, + publisher={Elsevier} +} + +@UNPUBLISHED{gundrytutorial, + title={A tutorial implementation of dynamic pattern unification}, + author={Gundry, Adam and McBride, Conor}, + note= {Unpublished draft}, + year={2013} +} + +@techreport{cockett1992charity, + title={About charity}, + author={Cockett, Robin and Fukushima, Tom}, + year={1992}, + journal={Yellow Series Report} +} + +@incollection{mcbride2009let, + title={Let’s see how things unfold: Reconciling the infinite with the intensional}, + author={McBride, Conor}, + booktitle={Algebra and Coalgebra in Computer Science}, + pages={113--126}, + year={2009}, + publisher={Springer} +} + +@article{huet1973undecidability, + title={The undecidability of unification in third order logic}, + author={Huet, Gerard P.}, + journal={Information and Control}, + volume={22}, + number={3}, + pages={257--267}, + year={1973}, + publisher={Elsevier} +} + +@article{dybjer1997representing, + title={Representing inductively defined sets by wellorderings in Martin-L{\"o}f's type theory}, + author={Dybjer, Peter}, + journal={Theoretical Computer Science}, + volume={176}, + number={1}, + pages={329--335}, + year={1997}, + publisher={Elsevier} +} + +@inbook{Nordstrom1990, + author = {Nordstr{\"o}m, Bengt and Petersson, Kent and Smith, Jan M.}, + title = {Programming in Martin-L{\"o}f Type Theory: An Introduction}, + publisher = {Oxford University Press}, + year = {1990} +} + +@incollection{Gimenez1995, +year={1995}, +isbn={978-3-540-60579-9}, +booktitle={Types for Proofs and Programs}, +volume={996}, +series={Lecture Notes in Computer Science}, +editor={Dybjer, Peter and Nordström, Bengt and Smith, Jan}, +doi={10.1007/3-540-60579-7_3}, +title={Codifying guarded definitions with recursive schemes}, +url={http://dx.doi.org/10.1007/3-540-60579-7_3}, +publisher={Springer Berlin Heidelberg}, +author={Giménez, Eduardo}, +pages={39-59} +} + +@article{Capretta2005, + author = {Venanzio Capretta}, + title = {General recursion via coinductive types}, + journal = {Logical Methods in Computer Science}, + volume = {1}, + number = {2}, + year = {2005}, + ee = {http://dx.doi.org/10.2168/LMCS-1(2:1)2005}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@article{Danielsson2012, + author = {Danielsson, Nils Anders}, + title = {Operational semantics using the partiality monad}, + journal = {SIGPLAN Not.}, + issue_date = {September 2012}, + volume = {47}, + number = {9}, + month = sep, + year = {2012}, + issn = {0362-1340}, + pages = {127--138}, + numpages = {12}, + url = {http://doi.acm.org/10.1145/2398856.2364546}, + doi = {10.1145/2398856.2364546}, + acmid = {2364546}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {dependent types, mixed induction and coinduction, partiality monad}, +} + + +@incollection{Paulson1990, + Author = {Paulson, Lawrence C.}, + Booktitle = {Logic and Computer Science}, + Date-Modified = {2005-04-20 12:07:55 +0100}, + Editor = {P. Odifreddi}, + Pages = {361-386}, + Publisher = {Academic Press}, + Title = {{Isabelle}: The Next 700 Theorem Provers}, + Year = {1990}} + + +@book{Russell1927, + author = "Whitehead, Alfred North and Russell, Bertrand Arthur + William", + title = "Principia mathematica; 2nd ed.", + publisher = "Cambridge Univ. Press", + address = "Cambridge", + year = "1927", +} \ No newline at end of file -- cgit v1.2.3