П |
What we Learn from Formal Checking. Part I. How to Believe a Machine-Checked Proof |
1996 |
Pollack R. |
|
|
Basic Research in Computer Science |
|
21.01.1997 |
П |
What we Learn from Formal Checking. Part II. Using Type Theory: An Introduction |
1996 |
Pollack R. |
|
|
Basic Research in Computer Science |
|
21.01.1997 |
П |
What we Learn from Formal Checking. Part III. Formalization is Not Just Filling In Details |
1996 |
Pollack R. |
|
|
Basic Research in Computer Science |
|
21.01.1997 |
СТ |
On Extensibility of Proof Checkers |
1995 |
Pollack R. |
Lecture Notes in Computer Science |
|
|
Types for Proofs and Programs |
30.11.1995 |
СТ |
A Verified Typechecker |
1995 |
Pollack R. |
|
|
|
Lecture Notes in Computer Science |
15.04.1995 |
СТ |
Checking Algorithms for Pure Type Systems |
1994 |
Van Benthem Jutting L. S., Mckinna J., Pollack R. |
|
|
|
Lecture Notes in Computer Science |
21.07.1994 |
СТ |
Closure Under Alpha-Conversion |
1994 |
Pollack R. |
|
|
|
Lecture Notes in Computer Science |
21.07.1994 |
СТ |
Type checking with universes |
1991 |
Harper R., Pollack R. |
|
|
|
Theoretical Computer Science |
28.11.1991 |