Publications of Randy Pollack

[1] T. Coquand, R. Pollack, and M. Takeyama. A logical framework with dependently typed records. In Typed Lambda Calculus and Applications, TLCA'03, volume 2701 of LNCS. Springer-Verlag, 2003. See extended version [2].
[ bib ]
[2] T. Coquand, R. Pollack, and M. Takeyama. A logical framework with dependently typed records. Extended version of [1], 2003.
[ bib | .ps.gz ]
[3] Robert Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13:386-402, 2002.
[ bib | .ps.gz ]
[4] H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg. A constructive algebraic hierarchy in Coq. Journal of Symbolic Computation, 34(4):271-286, 2002. Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems.
[ bib ]
[5] Pollack et.al. The LEGO Proof Assistant, 2001.
[ bib | http ]
[6] Geuvers, Pollack, Wiedijk, and Zwanenburg. The algebraic hierarchy of the FTA project. In Linton and Sebastiani, editors, Calculemus 2001 Proceedings, June 2001. See updated version [4].
[ bib ]
[7] T. Coquand, R. Pollack, and M. Takeyama. Modules as dependently typed records. 2001.
[ bib | .ps.gz ]
[8] R. Pollack. Inductive definition schemas formalised. Slides, 2001.
[ bib | .ps.gz ]
[9] Robert Pollack. Dependently typed records for representing mathematical structure. In Aagard and Harrison, editors, Theorem Proving in Higher Order Logics, TPHOLs 2000, volume 1869 of LNCS. Springer-Verlag, August 2000. See updated version [3].
[ bib ]
[10] Robert Pollack. Dependently typed records for representing mathematical structure. In Barthe and Dybjer, editors, Workshop on Subtyping and Dependent Types in Programming, DTP'2000. INRIA, June 2000. See updated version [3].
[ bib ]
[11] J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23(3-4), November 1999.
[ bib | .ps.gz ]
[12] Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998.
[ bib | .ps.gz ]
[13] R. Pollack. Theories in type theory. In [?], 1997.
[ bib ]
[14] Robert Pollack. A verified typechecker. In M.Dezani-Ciancaglini and G.Plotkin, editors, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, TLCA'95, Edinburgh, volume 902 of LNCS. Springer-Verlag, April 1995.
[ bib | .ps.gz ]
[15] Robert Pollack. On extensibility of proof checkers. In Dybjer, Nordstrom, and Smith, editors, Types for Proofs and Programs: International Workshop TYPES'94, Bå stad, June 1994, Selected Papers, volume 996 of LNCS, pages 140-161. Springer-Verlag, 1995.
[ bib | .ps.gz ]
[16] Robert Pollack. Polishing up the Tait-Martin-Löf proof of the Church-Rosser theorem. In Proceedings of De Wintermöte '95. Department of Computing Science, Chalmers Univ. of Technology, Göteborg, Sweden, January 1995.
[ bib | .ps.gz ]
[17] Robert Pollack. Closure under alpha-conversion. In H. Barendregt and T. Nipkow, editors, TYPES'93: Workshop on Types for Proofs and Programs, Nijmegen, May 1993, Selected Papers, volume 806 of LNCS, pages 313-332. Springer-Verlag, 1994.
[ bib | .ps.gz ]
[18] L.S. van Benthem Jutting, J. McKinna, and R. Pollack. Checking algorithms for Pure Type Systems. In Barendregt and Nipkow, editors, TYPES'93: Workshop on Types for Proofs and Programs, Selected Papers, volume 806 of LNCS, pages 19-61. Springer-Verlag, 1994.
[ bib | .ps.gz ]
[19] Robert Pollack. Are tactics feasible? Extended abstract in informal proceedings of the Workshop on correctness and metatheoretic extensibility of automated reasoning systems, at CADE-12, Nancy, France, June 1994.
[ bib ]
[20] R. Pollack. Incremental changes in LEGO: 1994. See [5], May 1994.
[ bib ]
[21] Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, Univ. of Edinburgh, 1994.
[ bib | .ps.gz ]
[22] J. McKinna and R. Pollack. Pure Type Systems formalized. In M.Bezem and J.F.Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, Utrecht, number 664 in LNCS, pages 289-305. Springer-Verlag, March 1993.
[ bib | .ps.gz ]
[23] C. Jones and R. Pollack. Incremental changes in LEGO: 1993. See [5], May 1993.
[ bib ]
[24] R. Pollack. Typechecking in Pure Type Systems. In Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bå stad, Sweden, pages 271-288, June 1992.
[ bib | .ps.gz ]
[25] Z. Luo and R. Pollack. LEGO proof development system: User's manual. Technical Report ECS-LFCS-92-211, Computer Science Dept., Univ. of Edinburgh, 1992. See [5].
[ bib ]
[26] A. Avron, F. Honsell, I. Mason, and R. Pollack. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309-352, 1992.
[ bib | .ps.gz ]
[27] Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89:107-136, 1991.
[ bib | .ps.gz ]
[28] Robert Pollack. Implicit syntax. Informal Proceedings of First Workshop on Logical Frameworks, Antibes, May 1990.
[ bib ]
[29] R. Pollack. Implicit syntax. In the preliminary Proceedings of the 1st Workshop on Logical Frameworks, 1990.
[ bib ]
[30] R. Pollack. The Tarski fixpoint theorem. communication on TYPES e-mail network, 1990.
[ bib ]
[31] Robert Harper and Robert Pollack. Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions. In J. Diaz and F. Orejas, editors, Proceedings, TAPSOFT '89, volume 352 of LNCS. Springer-Verlag, 1989.
[ bib ]
[32] Robert Pollack. Existential variables and resolution in type theory. Talk at the Jumelage on Typed Lambda Calculus, September 1989.
[ bib ]
[33] R. Pollack. The theory of LEGO. manuscript, 1989.
[ bib ]
[34] Robert Pollack. The theory of LEGO. Thesis proposal, October 1988.
[ bib ]
[35] C. Jones and R. Pollack. Incremental changes in LEGO: 1993, 1994. See [5].
[ bib ]
[36] Robert Pollack. Theories in type theory. Transparencies for a talk at [?], available from [5].
[ bib ]

This file has been generated by bibtex2html 1.61