bibfile.bib

@COMMENT{{This file has been generated by bib2bib 1.61}}

@COMMENT{{Command line: ./bib2bib -oc citefile -ob bibfile.bib -c 'author : "Pollack"' --expand -s year -r mybib.bib}}

@PREAMBLE{{{{\newcommand{\ML}{Martin-L\"of}}}}}


@INPROCEEDINGS{CoqPolTakTLCA03,
  AUTHOR = {T. Coquand and R. Pollack and M. Takeyama},
  TITLE = {A Logical Framework with Dependently Typed Records},
  BOOKTITLE = {Typed Lambda Calculus and Applications, TLCA'03},
  YEAR = 2003,
  SERIES = {{LNCS}},
  VOLUME = 2701,
  PUBLISHER = {Springer-Verlag},
  NOTE = {See extended version \cite{CoqPolTak:LF_extended}}
}


@UNPUBLISHED{CoqPolTak:LF_extended,
  AUTHOR = {T. Coquand and R. Pollack and M. Takeyama},
  TITLE = {A Logical Framework with Dependently Typed Records},
  YEAR = 2003,
  NOTE = {Extended version of~\cite{CoqPolTakTLCA03}},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/TLCA03extended.ps.gz}
}


@ARTICLE{pollackFAC02,
  AUTHOR = {Robert Pollack},
  TITLE = {Dependently Typed Records in Type Theory},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = 2002,
  VOLUME = 13,
  PAGES = {386--402},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/recordsFAC.ps.gz}
}


@ARTICLE{algHier02,
  AUTHOR = {H. Geuvers and R. Pollack and F. Wiedijk and J. Zwanenburg},
  TITLE = {A Constructive Algebraic Hierarchy in {C}oq},
  JOURNAL = {Journal of Symbolic Computation},
  YEAR = 2002,
  VOLUME = 34,
  NUMBER = 4,
  PAGES = {271--286},
  NOTE = {Special Issue on the Integration of Automated Reasoning 
          and Computer Algebra Systems}
}


@MISC{legoWWW,
  KEY = {LEGO},
  AUTHOR = {Pollack \emph{et.al.}},
  TITLE = {{The LEGO Proof Assistant}},
  YEAR = 2001,
  URL = {http://www.dcs.ed.ac.uk/home/lego/}
}


@INPROCEEDINGS{algHier01,
  AUTHOR = {Geuvers and Pollack and Wiedijk and Zwanenburg},
  TITLE = {The Algebraic Hierarchy of the {FTA} Project},
  BOOKTITLE = {Calculemus 2001 Proceedings},
  YEAR = 2001,
  EDITOR = {Linton and Sebastiani},
  MONTH = JUN,
  NOTE = {See updated version~\cite{algHier02}}
}


@UNPUBLISHED{CoqPolTakPPDP01submitted,
  AUTHOR = {T. Coquand and R. Pollack and M. Takeyama},
  TITLE = {Modules as Dependently Typed Records},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/modulesNBE.ps.gz},
  YEAR = 2001
}


@UNPUBLISHED{pollackIndDefFormal01,
  AUTHOR = {R. Pollack},
  TITLE = {Inductive Definition Schemas Formalised},
  NOTE = {Slides},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/inductSchemaSlides.ps.gz},
  YEAR = 2001
}


@INPROCEEDINGS{pollack2000,
  AUTHOR = {Robert Pollack},
  TITLE = {Dependently Typed Records for Representing
                  Mathematical Structure},
  BOOKTITLE = {Theorem Proving in Higher Order Logics, {TPHOL}s 2000},
  YEAR = 2000,
  EDITOR = {Aagard and Harrison},
  VOLUME = 1869,
  SERIES = {{LNCS}},
  MONTH = AUG,
  PUBLISHER = {Springer-Verlag},
  NOTE = {See updated version~\cite{pollackFAC02}}
}


@INPROCEEDINGS{pollack2000dtp,
  AUTHOR = {Robert Pollack},
  TITLE = {Dependently Typed Records for Representing
                  Mathematical Structure},
  BOOKTITLE = {Workshop on Subtyping and Dependent Types in Programming,
                  {DTP'2000}},
  YEAR = 2000,
  MONTH = JUN,
  EDITOR = {Barthe and Dybjer},
  PUBLISHER = {INRIA},
  NOTE = {See updated version~\cite{pollackFAC02}}
}


@ARTICLE{McKinnaPollack99,
  AUTHOR = {J. McKinna and R. Pollack},
  TITLE = {Some Lambda Calculus and Type Theory Formalized},
  JOURNAL = {Journal of Automated Reasoning},
  YEAR = 1999,
  VOLUME = 23,
  NUMBER = {3--4},
  MONTH = NOV,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/McKinnaPollack99.ps.gz}
}


@INPROCEEDINGS{Pollack:belief,
  AUTHOR = {Robert Pollack},
  TITLE = {How to Believe a Machine-Checked Proof},
  BOOKTITLE = {Twenty Five Years of Constructive Type Theory},
  EDITOR = {G. Sambin and J. Smith},
  YEAR = 1998,
  PUBLISHER = {Oxford Univ. Press},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/believing.ps.gz}
}


@ARTICLE{pollack:theory,
  AUTHOR = {R. Pollack},
  TITLE = {Theories in Type Theory },
  JOURNAL = {In \cite{Durham:workshop97}},
  YEAR = 1997
}


@INPROCEEDINGS{PollackTLCA95,
  AUTHOR = {Robert Pollack},
  TITLE = {A Verified Typechecker},
  BOOKTITLE = {Proceedings of the Second International
                  Conference on Typed Lambda Calculi and Applications,
                  TLCA'95, Edinburgh},
  EDITOR = {M.Dezani-Ciancaglini and G.Plotkin},
  YEAR = 1995,
  MONTH = APR,
  PUBLISHER = {Springer-Verlag},
  SERIES = {{LNCS}},
  VOLUME = 902,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/tcAlgorithm.ps.gz}
}


@INPROCEEDINGS{pollackExtensibility,
  AUTHOR = {Robert Pollack},
  TITLE = {On Extensibility of Proof Checkers},
  BOOKTITLE = {Types for Proofs and Programs: International
                  Workshop TYPES'94, B\aa stad, June 1994, Selected
                  Papers},
  EDITOR = {Dybjer and Nordstrom and Smith},
  SERIES = {{LNCS}},
  VOLUME = 996,
  PAGES = {140--161},
  YEAR = 1995,
  PUBLISHER = {Springer-Verlag},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/extensibility.ps.gz}
}


@INCOLLECTION{pollack:CR,
  AUTHOR = {Robert Pollack},
  TITLE = {Polishing Up the {Tait--Martin-L\"{o}f} Proof of the
                  {Church-Rosser} Theorem},
  BOOKTITLE = {Proceedings of {De Winterm\"{o}te} '95},
  PUBLISHER = {Department of Computing Science, Chalmers Univ.
                  of Technology, {G\"{o}teborg}, Sweden},
  YEAR = 1995,
  MONTH = JAN,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/churchrosser.ps.gz}
}


@INPROCEEDINGS{Pollack93,
  AUTHOR = {Robert Pollack},
  TITLE = {Closure Under Alpha-Conversion},
  BOOKTITLE = {TYPES'93: Workshop on Types for Proofs and Programs,
                 Nijmegen, May 1993, Selected Papers},
  EDITOR = {H. Barendregt and T. Nipkow},
  PAGES = {313--332},
  VOLUME = 806,
  SERIES = {{LNCS}},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1994,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/alpha_closure.ps.gz}
}


@INPROCEEDINGS{JuttingMcKinnaPollack93,
  AUTHOR = {L.S. van Benthem Jutting and J. McKinna and
                 R. Pollack},
  TITLE = {Checking Algorithms for {P}ure {T}ype {S}ystems},
  BOOKTITLE = {TYPES'93: Workshop on Types for Proofs and Programs,
                 Selected Papers},
  EDITOR = {Barendregt and Nipkow},
  PAGES = {19--61},
  VOLUME = 806,
  SERIES = {{LNCS}},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1994,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/JMPchecking.ps.gz}
}


@UNPUBLISHED{pollack94a,
  AUTHOR = {Robert Pollack},
  TITLE = {Are Tactics Feasible?},
  NOTE = {Extended abstract in informal proceedings of the
                  {\em Workshop on correctness and metatheoretic
                  extensibility of automated reasoning systems}, at
                  {CADE-12}, Nancy, France},
  YEAR = 1994,
  MONTH = JUN
}


@UNPUBLISHED{LegoChanges94,
  AUTHOR = {R. Pollack},
  TITLE = {Incremental Changes in {LEGO}: 1994},
  NOTE = {See \cite{legoWWW}},
  YEAR = {1994},
  MONTH = MAY
}


@PHDTHESIS{PollackPhD,
  AUTHOR = {Robert Pollack},
  TITLE = {The Theory of {LEGO}: {A} Proof Checker for the
                  Extended Calculus of Constructions},
  SCHOOL = {Univ. of Edinburgh},
  YEAR = 1994,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/thesis.ps.gz}
}


@INPROCEEDINGS{McKinnaPollack93,
  AUTHOR = {J. McKinna and R. Pollack},
  TITLE = {{P}ure {T}ype {S}ystems Formalized},
  BOOKTITLE = {Proceedings of the International Conference on Typed
                 Lambda Calculi and Applications, TLCA'93, Utrecht},
  YEAR = 1993,
  EDITOR = {M.Bezem and J.F.Groote},
  PAGES = {289--305},
  MONTH = MAR,
  PUBLISHER = {Springer-Verlag},
  SERIES = {{LNCS}},
  NUMBER = 664,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/formalPTS.ps.gz}
}


@UNPUBLISHED{LegoChanges93,
  AUTHOR = {C. Jones and R. Pollack},
  TITLE = {Incremental Changes in {LEGO}: 1993},
  NOTE = {See \cite{legoWWW}},
  YEAR = {1993},
  MONTH = MAY
}


@INPROCEEDINGS{Pollack92,
  AUTHOR = {R. Pollack},
  TITLE = {Typechecking in {P}ure {T}ype {S}ystems},
  BOOKTITLE = {Informal Proceedings of the 
                 1992 Workshop on Types for Proofs and Programs,
                 B\aa stad, Sweden},
  YEAR = 1992,
  PAGES = {271-288},
  MONTH = JUN,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/BaastadTypechecking.ps.gz}
}


@TECHREPORT{legomanual,
  AUTHOR = {Z. Luo and R. Pollack},
  TITLE = {{LEGO} Proof Development System: User's Manual},
  INSTITUTION = {Computer Science Dept., Univ. of Edinburgh},
  YEAR = 1992,
  NUMBER = {ECS-LFCS-92-211},
  NOTE = {See \cite{legoWWW}}
}


@ARTICLE{PollackA,
  AUTHOR = {A. Avron and F. Honsell and I. Mason and R. Pollack},
  TITLE = {Using Typed Lambda Calculus to Implement Formal
                  Systems on a Machine},
  JOURNAL = {Journal of Automated Reasoning},
  YEAR = 1992,
  VOLUME = 9,
  PAGES = {309-352},
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/AHMP92jar.ps.gz}
}


@ARTICLE{HarperPollack91,
  AUTHOR = {Robert Harper and Robert Pollack},
  TITLE = {Type Checking with Universes},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = 89,
  PAGES = {107--136},
  YEAR = 1991,
  URL = {http://homepages.inf.ed.ac.uk/rpollack/export/universes_TCS.ps.gz}
}


@UNPUBLISHED{Pollack90,
  AUTHOR = {Robert Pollack},
  TITLE = {Implicit Syntax},
  NOTE = {Informal Proceedings of First Workshop on 
                 Logical Frameworks, Antibes},
  YEAR = {1990},
  MONTH = MAY
}


@UNPUBLISHED{pollack:implicit90,
  AUTHOR = {Pollack, R.},
  TITLE = {Implicit Syntax},
  NOTE = {In the preliminary Proceedings of the 1st Workshop
		 on Logical Frameworks},
  YEAR = 1990
}


@UNPUBLISHED{pollack:tarski,
  AUTHOR = {Pollack, R.},
  TITLE = {The {Tarski} Fixpoint Theorem},
  NOTE = {communication on TYPES e-mail network},
  YEAR = {1990},
  OPTMONTH = {}
}


@INPROCEEDINGS{HarperPollack89,
  AUTHOR = {Robert Harper and Robert Pollack},
  TITLE = {Type Checking, Universe Polymorphism, and 
                Typical Ambiguity in the Calculus of Constructions},
  YEAR = 1989,
  BOOKTITLE = {Proceedings, TAPSOFT '89},
  EDITOR = {J. Diaz and F. Orejas},
  PUBLISHER = {Springer-Verlag},
  SERIES = {{LNCS}},
  VOLUME = 352
}


@UNPUBLISHED{PollackExisVar89,
  AUTHOR = {Robert Pollack},
  TITLE = {Existential Variables and Resolution in Type Theory},
  NOTE = {Talk at the \emph{Jumelage on Typed Lambda Calculus}},
  YEAR = 1989,
  MONTH = SEP
}


@UNPUBLISHED{pollack:legothy,
  AUTHOR = {Pollack, R.},
  TITLE = {The Theory of {LEGO}},
  NOTE = {manuscript},
  YEAR = 1989
}


@UNPUBLISHED{pollack88,
  AUTHOR = {Robert Pollack},
  TITLE = {The Theory of {LEGO}},
  NOTE = {Thesis proposal},
  YEAR = {1988},
  MONTH = OCT
}


@UNPUBLISHED{LegoChanges9394,
  AUTHOR = {C. Jones and R. Pollack},
  TITLE = {Incremental Changes in {LEGO}: 1993, 1994},
  NOTE = {See \cite{legoWWW}}
}


@UNPUBLISHED{PollackTheories,
  AUTHOR = {Robert Pollack},
  TITLE = {Theories in Type Theory},
  NOTE = {Transparencies for a talk at~\cite{Durham:workshop97},
                  available from \cite{legoWWW}}
}


This file has been generated by bibtex2html 1.61