Pavel Naumov Postdoctoral Associate Ph.D., Cornell University, 1998 Honors Diploma, Moscow State Univ., 1992 pavel@cs.cornell.edu http://www.cs.cornell.edu/home/pavel   Office Address 456  Theory Center Office Phone (607) 255-5716 Office Fax (607) 255-4428 Mailing Address Computer Science Department Cornell University Upson Hall Ithaca, NY 14853 Home Phone (607) 257-6951

Interpreting Isabelle Theories in NuPRL

• PRL Seminar: March 8, 1999
• Importing Isabelle Formal Mathematics into NuPRL, Cornell Computer Science Technical Report TR99-1734, February 1999
• PRL Seminar: September 8, 1998

NuPRL Web Publisher

• Publishing Formal Mathematics on the Web, Cornell Computer Science Technical Report TR98-1689, June 1998
• Online Demo

Reference Types

• Theory of Reference Types Cornell Computer Science Technical Report TR98-1711, October 1998
• Formalizing Reference Types in NuPRL Ph.D. Dissertation, Cornell University, August 1998; Cornell Computer Science Technical Report TR98-1709, September 1998
• PRL Seminar: March 10, 1998
• PRL Seminar: November 25, 1997
• PRL Seminar: September 9, 1997
• Online NuPRL Library

Simple Imperative Programming Language

• Online NuPRL Library

Automata Theory

• Constructively Formalizing Automata Theory joint work with R.L. Constable, P. Jackson, and J. Uribe in Proof, Language, and Interaction: Essays in Honour of Robert Milner, MIT Press, 1998 (322K)
• Online NuPRL Library

Modal Logic

• Undesidability of Second Order Provability Logic with Witness Comparison, Vestnik MGU , Vol. 48, No. 3, pp. 14-17 1993 (Russian). English Translation in Moscow University Mathematics Bulletin, Allerton Press, New York
• Undesidability of Godel-Lob Logic with Quantifiers over Propositional Variables, Vestnik MGU , Vol. 48, No. 2, pp. 13-16 1993 (Russian). English Translation in Moscow University Mathematics Bulletin, Allerton Press, New York
• On Modal Logics, Conservative over Intuitionistic Calculus, Vestnik MGU , Vol. 46, No. 6, pp. 58-61 1993 (Russian). English Translation in Moscow University Mathematics Bulletin, Allerton Press, New York
• Second Order Modal Logics with Provability Interpretation, Diploma Thesis, Moscow State University, June 1992

Personal

• Family Photo Album with many pictures of my wife, Elena, our relatives, and friends
• Humor