Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft). - Robert Harper 001; Robert Pollack (TAPSOFT, Vol.2, 1989)

Type Checking with Universes. - Robert Harper 001; Robert Pollack (Theor. Comput. Sci., 1991)

Using Typed Lambda Calculus to Implement Formal Systems on a Machine. - Arnon Avron; Furio Honsell; Ian A. Mason; Robert Pollack (J. Autom. Reason., 1992)

Pure Type Systems Formalized. - James McKinna; Robert Pollack (TLCA, 1993)

Checking Algorithms for Pure Type Systems. - L. S. van Benthem Jutting; James McKinna; Robert Pollack (TYPES, 1993)

On Extensibility of Proof Checkers. - Robert Pollack (TYPES, 1994)

A Verified Typechecker. - Robert Pollack (TLCA, 1995)

The theory of LEGO. - Robert Pollack (1995)

Some Lambda Calculus and Type Theory Formalized. - James McKinna; Robert Pollack (J. Autom. Reason., 1999)

Dependently Typed Records for Representing Mathematical Structure. - Robert Pollack (TPHOLs, 2000)

Dependently Typed Records in Type Theory. - Robert Pollack (Formal Aspects Comput., 2002)

Critical slope p-adic L-functions. - Robert Pollack; Glenn Stevens (J. Lond. Math. Soc., 2013)

On the Statistical Mechanics of Life: Schrödinger Revisited. - Kate Jeffery; Robert Pollack; Carlo Rovelli (Entropy, 2019)