I n t e r e s t s

Logic and its applications in Computer Science: Non-Classical Logics, Proof Complexity, Type Theory, Programming Language Semantics, Automated Deduction, and Formal Verification

E d u c a t i o n

• Ph.D., Cornell University, 1998
• Honors Diploma, Moscow State University, 1992

T e a c h i n g   @   M c D a n i e l

• CSC 1106 The Art of Programming: Spring 06, Fall 05
• CSC/MAT 1109 Discrete Mathematics: Fall 06, Spring 06
• CSC 1110 Recursion in Algorithms, Logic, and Mathematics: Fall 07, Fall 06
• CSC 2209 Computer Organization: Spring 07
• CSC/MAT 2210 Numerical Methods: Spring 07, Fall 05
• CSC 2217 Data Structures: Fall 07, Fall 06
• CSC 2265 Artificial Intellegence: Fall 05
• CSC 3315 Principles of Computer Graphics: Fall 07
• CSC 3317 Algorithms: Spring 07, Spring 06

P r e v i o u s l y   T a u g h t

Discrete Mathematics, Discrete Mathematical Structures, Data Structures and Algorithms, Foundations of Mathematics, Formal Languages with Applications, Software Engineering and Design, Artificial Intelligence, Object-Oriented Programming with Java, Fundamentals of Computer Science III, Formal Methods for Software Engineering, Advanced Programming Languages, Advanced Artificial Intelligence

J o u r n a l   A r t i c l e s

• P. Naumov, On meta complexity of propositional formulas and propositional proofs, Archive for Mathematical Logic, (to appear)
• P. Naumov, Logic of Subtyping, Theoretical Computer Science, pp. 167-185, v. 357, n.1-3, 2006 (link)
• P. Naumov, Upper bounds on complexity of Frege proofs with limited use of certain schemata, Archive for Mathematical Logic, pp. 432-446, v. 45, 2006 (link)
• P. Naumov, On Modal Logic of Deductive Closure, Annals of Pure and Applied Logic, pp. 218-224, v. 141, n.1-2, 2006 (link)
• P. Naumov, On Modal Logics of Partial Recursive Functions, Studia Logica, pp. 295-309, v. 81, 2005, (link)
• P. Naumov, Undecidability of Second Order Provability Logic with Witness Comparison, Vestnik MGU, pp. 14-17, Vol. 48, No. 3, 1993 (Russian). English translation in Moscow University Mathematics Bulletin, Allerton Press, NY
• P. Naumov, Undecidability of Gödel-Löb Logic with Quantifiers over Propositional Variables, Vestnik MGU, pp. 13-16, Vol. 48, No. 2, 1993, (Russian). English translation in Moscow University Mathematics Bulletin, Allerton Press, NY
• P. Naumov, On Modal Logics, Conservative over Intuitionistic Calculus, Vestnik MGU, pp. 58-61, Vol. 46, No. 6, 1991 (Russian). English translation in Moscow University Mathematics Bulletin, Allerton Press, NY

B o o k   C h a p t e r

• R. Constable, P. Jackson, P. Naumov, and J. Uribe, Constructively Formalizing Automata Theory, in Proof, Language, and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000

C o n f e r e n c e   P a p e r s

• P. Naumov, On Modal Logic of Deductive Closure, Logic Colloquium 2004, ASL European Summer Meeting, Turin, Italy, July 2004, The Bulletin of Symbolic Logic, v. 11, n. 2, pp. 288-289, 2005
• P. Naumov, On Modal Logics of Computable Functions, Annual Meeting of the Association for Symbolic Logic, Pittsburgh, May 2004, The Bulletin of Symbolic Logic, v. 11, n. 1, p. 113, 2005
• P. Naumov, Logic of Subtyping, presented at The 18th Annual IEEE Symposium on Logic in Computer Science (LICS`03), Ottawa, Canada, June 2003
• P. Naumov, An extension of the classical propositional logic by type constructors, Winter Meeting of the Association for Symbolic Logic, Baltimore, January 2003, The Bulletin of Symbolic Logic, v. 9, n.2, pp. 254-255, 2003
• P. Naumov, M.-O. Stehr, and J. Meseguer, The HOL/NuPRL Proof Translator: A Practical Approach to Formal Interoperatability, The 14th International Conference on Theorem Proving in Higher Order Logics, pp. 329-345, Edinburgh, Scotland, September 2001, Lecture Notes in Computer Science, Springer
• M.-O. Stehr, P. Naumov, and J. Meseguer, A Proof-Theoretic Approach to HOL-Nuprl Connection with Applications to Proof Translation, The 15th International Workshop on Algebraic Development Techniques/General Workshop of the Common Framework Initiative, Genova, Italy, April 2001
• P. Naumov, Formalization of Isabelle Meta Logic in NuPRL, Supplemental proceedings of The 13th International Conference on Theorem Proving in Higher Order Logics,, Portland, Oregon, 2000
• P. Naumov, Importing Isabelle Formal Mathematics into NuPRL, Theorem Proving in Higher Order Logics: Emerging Trends 1999, Supplemental proceedings of The 12th International Conference on Theorem Proving in Higher Order Logics, Nice, France, 1999

T e c h n i c a l   R e p o r t s

• P. Naumov, Theory of Reference Types, Cornell CS Technical Report 98-1711, 1998
• P. Naumov, Publishing Formal Mathematics on the Web, Cornell CS Technical Report 98-1689, 1998
• P. Naumov, Formalizing Reference Types in NuPRL, Ph.D. Dissertation, Cornell Computer Science Technical Report TR98-1709, 1998
• P. Naumov, Second Order Modal Logics with Provability Interpretation, Diploma Thesis, Moscow State University, June 1992

N o t   t o   b e   t a k e n   t o o   s e r i o u s l y . . .

Advisor genealogy