| 2002 |
|---|
| 11 | | Paul Callaghan,
Zhaohui Luo,
James McKinna,
Robert Pollack:
Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers
Springer 2002 |
| 10 | EE | Robert Pollack:
Dependently Typed Records in Type Theory.
Formal Asp. Comput. 13(3-5): 386-402 (2002) |
| 2000 |
|---|
| 9 | | Robert Pollack:
Dependently Typed Records for Representing Mathematical Structure.
TPHOLs 2000: 462-479 |
| 1999 |
|---|
| 8 | | James McKinna,
Robert Pollack:
Some Lambda Calculus and Type Theory Formalized.
J. Autom. Reasoning 23(3-4): 373-409 (1999) |
| 1995 |
|---|
| 7 | | Robert Pollack:
A Verified Typechecker.
TLCA 1995: 365-380 |
| 1994 |
|---|
| 6 | | Robert Pollack:
On Extensibility of Proof Checkers.
TYPES 1994: 140-161 |
| 1993 |
|---|
| 5 | | James McKinna,
Robert Pollack:
Pure Type Systems Formalized.
TLCA 1993: 289-305 |
| 4 | | L. S. van Benthem Jutting,
James McKinna,
Robert Pollack:
Checking Algorithms for Pure Type Systems.
TYPES 1993: 19-61 |
| 1992 |
|---|
| 3 | | Arnon Avron,
Furio Honsell,
Ian A. Mason,
Robert Pollack:
Using Typed Lambda Calculus to Implement Formal Systems on a Machine.
J. Autom. Reasoning 9(3): 309-354 (1992) |
| 1991 |
|---|
| 2 | | Robert Harper,
Robert Pollack:
Type Checking with Universes.
Theor. Comput. Sci. 89(1): 107-136 (1991) |
| 1989 |
|---|
| 1 | | Robert Harper,
Robert Pollack:
Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions (Draft).
TAPSOFT, Vol.2 1989: 241-256 |
