@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}} }