Selected publications

• S.Artemov,  E.Barzilay , R.Constable, A.Nogin ``Reflection and Propositions-as-Types'', submitted to a conference, 2001.
• S.Artemov and T.Sidon-Yavorskaya ``On the first order logic of proofs'', Technical Report CFIS 99-11, Cornell University, 1999. To appear in the Moscow Mathematical Journal in 2001.
• S. Artemov, ``Explicit provability and constructive semantics'', Bulletin of Symbolic Logic, volume 7, No.1, pp.1-36, 2001
• S. Artemov, ``Operations on proofs that can be specified by means of modal logic,'' Technical Report  CFIS 99-02, Cornell University, 1999. To appear in Advances in Modal Logic, Volume 2,  CSLI Publications, Stanford University, pp.59-72, 2001.
• S. Artemov, ``Unified semantics for modality and  lambda-terms via proof polynomials,'' Technical Report  CFIS 99-03, Cornell University, 1999. To appear in Logic, Language and Computation, CSLI Publications, Stanford University, 2001
• J.Alt and S.Artemov, ``Reflective lambda-calculus'', Technical Report CFIS 00-06, Cornell University, 2000  (submitted to a conference in 2001)
• S.Artemov, E.Kazakov and D.Shapiro ``On logic of knowledge with justifications'', Technical Report CFIS 99-12, Cornell University, 1999.
• S. Artemov, ``Understanding Constructive Semantics'', Spinoza Lecture for European Association for Logic, Language and Information, Utrecht, August 1999
• S. Artemov, ``Uniform provability realization of intuitionistic logic, modality and lambda-terms'', Electronic Notes on Theoretical Computer Science v. 23, No. 1, 1999
• S. Artemov, ``Deep isomorphism of modal derivations and lambda-terms'',  Technical Report CFIS 99-07, Cornell University, 1999. Proceedings of the Workshop Intuitionistic Modal Logic and Applications, Trento, Italy, 1999
• S. Artemov. Preface to L. Beklemishev, M. Pentus, K. Vereshchagin ``Provability, Complexity, Grammars''. American Mathematical Society Translations,  series 2, volume 192, 1999
• S. Artemov, ``On explicit reflection in theorem proving and formal verification,'' In Springer Lecture Notes in Artificial Intelligence v. 1632, Automated Deduction - CADE-16. Proceedings of the 16th International Conference on Automated Deduction, Trento, Italy, July 1999, pp. 267-281, 1999
• S. Artemov, ``Realization of Intuitionistic Logic by Proof Polynomials'', Journal of Applied Non-Classical Logics, v. 9, n. 2-3, pp. 285-302, 1999
• S. Artemov, ``Explicit Modal Logic,'' Workshop Proceedings Advances in Modal Logic, Volume 2, Uppsala, 1998, Technical Report  CFIS 98-17, Cornell University, 1998.
• S. Artemov, ``Explicit provability: the intended semantics for intuitionistic and modal logic,'' Technical Report CFIS 98-10, Cornell University, 1998
• S. Artemov. ``Logic of proofs: a unified semantics for modality and lambda-terms,'' Technical Report  CFIS 98-06, Cornell University, 1998.
• S. Artemov, J. Davoren and A. Nerode. ``Modal logics and topological semantics for Hybrid Systems,'' Technical Report  MSI 97-05, Cornell University, 1997.
• S. Artemov, J. Davoren and A. Nerode. ``Topological semantics for and Hybrid Systems,'' In  Springer Lecture Notes in Computer Science; v. 1234, Proceedings of the 4th International Symposium on Logical Foundations of Computer Science, LFCS'97, pp. 1-8, 1997.
• S. Artemov. ``Proof realizations of the typed lambda-calculi,'' Technical Report MSI 97-02, Cornell University, 1997.
• S. Artemov and V. Krupski. ``Data storage interpretation of labeled modal logic,'' Annals of Pure and Applied Logic, v. 78, pp. 57-71, 1996.
• S. Artemov and A. Chuprina. ``Logic of proofs with complexity operators, Logic and Algebra,'' Lecture Notes in Pure and Applied Mathematics,  Series/180, Marcel Dekker, Inc. New York, 1996.
• S. Artemov. ``Proof realization of intuitionistic and modal logics,'' Technical Report MSI 96-06, Cornell University, 1996.
• S. Artemov. ``Operational modal logic,'' Technical Report MSI 95-29, Cornell University, 1995.
• S. Artemov, G. Boolos, E. Engeler, S. Feferman, G. Jager and A. Visser. Preface. Annals of Pure and Applied Logic, v. 75 (1-2):1, 1995. Special issue of papers from the Conference on Proof Theory, Provability Logic and Computation, Berne, Switzerland, 20-24 March 1994.
• S. Artemov. ``Logic of Proofs,'' Annals of Pure and Applied Logic, v. 67, pp. 29-59, 1994.
• S. Artemov and V. Krupski. ``Referential data structures and labeled modal logic,'' In Springer Lecture Notes in Computer Science; v. 813, Proceedings of the 3th International Symposium on Logical Foundations of Computer Science, LFCS'94, pp. 23-33, 1994.
• S. Artemov and F. Montagna. ``On first order theories with provability operator,'' Journal of Symbolic Logic, v. 59, No. 4, 1994.
• S. Artemov. ``On propositional quantifiers in Provability Logic, Logic Colloquium'91,'' Journal of Symbolic Logic, v. 58, No. 2, pp. 743-744, 1993.
• S. Artemov and T. Strassen. ``The logic of the Godel proof predicate,'' Lecture Notes in Computer Science, v. 713, pp. 71-82, Springer-Verlag, 1993.
• S. Artemov and T. Strassen. ``The Basic Logic of Proofs,'' Lecture Notes in Computer Science, v. 702, pp. 14-28, Springer-Verlag, 1993.
• S. Artemov and L.D. Beklemishev. ``On propositional quantifiers in Provability Logic,'' Notre Dame Journal of Formal Logic, v. 34, No. 3, pp. 401-419, 1993.
• S. Artemov. ``Uniform arithmetical completeness of modal provability logics,'' Matematicheskie Zametki, v. 48, No. 1, pp. 3-10, 1990 (Russian); English transl.: Soviet Math. Notes, v. 48, no. 1-2, 625-629, 1991.
• S. Artemov. ``Kolmogorov logic of problems and a provability interpretation of intuitionistic logic,'' Theoretical Aspects of Reasoning about Knowledge - III Proceedings, Morgan Kaufman Pbl., pp.257-272, 1990.
• S. Artemov and G.K. Dzhaparidze. ``Finite Kripke models and predicate logics of provability,'' Journal of Symbolic Logic, v. 55, No. 3, pp. 1090-1098, 1990.
• S. Artemov. ``Degrees of undecidability of extensions of arithmetic by true statements,'' Uspekhi Mat. Nauk.}, v. 43, No. 2(260), pp. 127-128, 1988 (Russian); English transl.: Russian Math. Surveys, v. 43, No. 2, pp. 159-160, 1988.
• S. Artemov and G.K. Dzhaparidze. ``Effective predicate logics of provability,'' Doklady AN SSSR, v. 297, No. 3, pp. 521-523, 1987 (Russian); English transl.: Soviet Math. Doklady, v. 36, No. 3, pp. 478-480, 1987.
• S. Artemov. ``Superintuitionistic logics having a provability interpretation,'' Doklady AN SSSR, v. 291, No. 6, pp. 1289-1291, 1986 (Russian); English transl.: Soviet Math. Doklady, v. 34, No. 3, pp. 596-598, 1987.
• S. Artemov. ``Numerically correct provability logics,'' Doklady AN SSSR, v.~290, No.~6, pp.~1289-1292, 1986 (Russian); English transl.: Soviet Math. Doklady, v. 34, No. 2, pp. 384-387, 1987.
• S. Artemov et al., ``Six Papers in Logic'', American Mathematical Society Translations, series 2, volume 135, 1987.
• S. Artemov. ``Modal logics axiomatizing provability,'' Izvestiya AN SSSR, ser. matem., v.~49, No.~6, pp.~1123-1154, 1985 (Russian); English transl.: Math USSR Izvestiya, v. 27, No. 2, pp. 401-429, 1986.
• S. Artemov. ``Non-arithmeticity of truth predicate logics of provability,'' Doklady AN SSSR, v. 284, No. 2, pp. 270-271, 1985 (Russian); English transl.: Soviet Math. Doklady, v. 32, No. 2, pp. 403-405, 1985.
• S. Artemov. ``Arithmetically complete modal theories,'' Semiotika i Informatika, Moscow, v. 14, pp. 115-133, 1980 (Russian)