...

1 files changed, 652 insertions, 0 deletions

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