[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 ] |