X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=thesis.bib;fp=thesis.bib;h=0000000000000000000000000000000000000000;hb=ebdf439a201d6fda0780284fc7f49b1f8deb88ab;hp=f58ff07f5150fdb65b3c504c16a63b4e4bd6622c;hpb=7e1d2c79545c573617ccedf458ba11bda1cc3eb8;p=bitonic-mengthesis.git diff --git a/thesis.bib b/thesis.bib deleted file mode 100644 index f58ff07..0000000 --- a/thesis.bib +++ /dev/null @@ -1,652 +0,0 @@ -@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