Books:
• 1. A Short Introduction to Modal Logic Center for the Study of Language and Information, Stanford, 1992, 91p.
• 2.Selected Papers in Proof Theory, Bibliopolis, Napoli, Italia and North-Holland, Amsterdam, 1992.
• 3.A Short Introduction to Intuitionistic Logic, Kluwer Academic - Plenum Publishers, New York, Boston, Dordrecht, London, Moscow, 2000

Some articles after 1990:
• "Gentzen-type Systems and Resolution Rules.Part I. Propositional Logic, " Lecture Notes in Computer Sci. 1990, 417, 198-231
• "Proof Theory in the USSR, 1925-1970" Journal of Symbolic Logic, 56:2, 1991, 385-423
• "Complexity of Subclasses of the Intuitionistic Propositional Calculus," BIT, 32:1, 1992, 64-69
• "A simple proof of the coherence theorem for cartesian closed categories, in G. Mints, Select Papers" in Proof Theory. North-Holland-Bibliopolis, 1992 , 213-220
• "A Normal Form Theorem for Logical Derivations Implying one for Arithmetic Derivations." Annals of Pure and Applied Logic, 62, 1993, p. 65-79
• "Resolution Calculus for the First Order Linear Logic," Journal of Logic, Language and Information, 2 :1993, 59-83
• "Gentzen-type systems and Resolution Rule. Part II. Logic Colloquium '90." Lecture Notes in Logic, 2, 1994, 163-190
• "Gentzen-type Systems and Hilbert's Epsilon Substitution Method. I." In: D.Prawitz, B. Skyrms, D. Westerstahl (eds.), Logic, Method. and Philos. of Sci. IX, Elsevier Science B.V., 1994, 91-122
• G. Mints, S. Tupailo, W. Buchholz, "Epsilon Substitution Method for Elementary Analysis," Archive for Math. Logic (1996), 35, 103-130
• "Normal forms for sequent derivations, " Kreiseliana, edited by P. Odifreddi, A.K. Peters, 1996, 469-492
• "Strong Termination for the epsilon-substitution method," Journal of Symbolic Logic , 61, no.4, 1996, 1193-1205
• "Indexed systems of sequents and cut-elimination," Journal of Philosophical Logic, v. 26, no 6, 1997, p. 671-696
• "Thoralf Skolem and the epsilon substitution method for predicate logic," Nordic Journal of Philosophical Logic, v.1 no.1, 1997, 133-146
• "Cut-elimination for Simple Type Theory with an Axiom of Choice," abstract, Bulletin of Symbolic Logic, 1997, no 2, p. 271-272
• "Three faces of natural deduction, in Automated Reasoning with Analytic Tableaux and Related Methods, " Lecture Notes in AI, 1227, 1997, 16-30
• "Existential instantiation and strong normalization, in Logical Foundations of Computer Science," Lecture Notes in Computer Science, 1997, v. 1234, 258-265
• "Dynamic topological logic," Bull.Symb. Logic v.3 no 3, 1997, 371-372 (with P. Kremer)
• "Axiomatizing the next-interior fragment of dynamic topological logic," Bull.Symb. Logic v.3 no 3, 1997, 376-377 (with P. Kremer,V. Rybakov) ASL meeting, MIT March 1997 abstract
• "A method of epsilon substitution for predicate logic with equality," Journal of Mathematical Sciences, 87,no 1, October 1997, 3234-3252 Consultants Bureau, NY [Translation of the Russian original published in 1995]
• "Normal deduction in the intuitionistic linear logic," Archive for Mathematical Logic, 37, no 5/6, 1998, 415-426
• "Linear Lambda-terms and natural deduction," Studia Logica, 60, 1998, 209-231
• "A completeness proof for propositional S4 in Cantor space." Orlowska, Ewa (ed.), Logic at work. Essays dedicated to the memory of Helena Rasiowa. Heidelberg: Physica-Verlag. Stud. Fuzziness Soft Comput. 24, 79-88 (1999). [ISBN 3-7908-1164-5/hbk]
• "The complexity of the disjunction and existence properties in intuitionistic logic" (joint with S. Buss), Annals of Pure and Applied Logic, 99, no 1-3, 1999, 93-304
• "Cut-elimination for simple type theory with an axiom of choice," JSL, 64, no.2, June 1999, 479-486
• "Epsilon-substitution method for ramified language and Delta-1-1 Comprehension axiom" (with S. Tupailo), in: A. Cantini etc (eds.), Logic and Foundations of Mathematics, 1999, 107-130, Kluwer Academic Publishers, Netherlands
• "In Memoriam: A.G. Dragalin." Bulletin of ASL, SL 1999, no.3, 389-391 (joint with S.Artemov, B. Kushner, E. Nogina, A. Troelstra) , JSL, 2000
• "Extended normal form theorems for logical proofs from axioms" (joint with T. Arai), Theoretical Computer Science, 232,121-132, 2000
• "Axiomatization of a Skolem function in intuitionistic logic," in: Faller, Martina, Stefan Kaufmann, and Marc Pauly, eds., Formalizing the Dynamics of Information. Stanford, CA: CSLI Publications, pp. 195-114, 2000.
• "Reductions of finite and infinite derivations," Annals of Pure and Applied Logic, v.104, no 1-3, 2000, 167-188
• "Russell's anticipation of intuitionistic logic," Bulletin of ASL, 2001
• "Quick and slow cut elimination," Bulletin of ASL, 2000
• "An approach to an epsilon-substitution method for ID1". Preprint, Institute Mittag-Leffler, no 45, MLI, Stockholm 2001.
• "Interpolation Theorems for Intuitionistic Logic," APAL 113, 2002, 225-242
• "Incomplete Proofs and Program synthesis," Extended abstract,in: Logic-Based Program Synthesis: State of the Art and Future Trends, AAAI Press, Menlo Park, California, 2002, p.13-16

To appear:
• "Quick cut-elimination for monotone cuts," CSLI Workshop Proceedings
• "The Epsilon Substitution Method and Continuity," Feferman Festschrift
• "Notes on Constructive Negation," Tubingen Proceedings
• "A Termination Proof for Epsilon Substitutions Using Partial Derivations," submitted to TCS

MEMBER OF EDITORIAL BOARDS:

Annals of Pure and Applied Logic (1975-1985)
Journal of Symbolic Logic (1980-1985)
Journal of Functional Programming 1990-1994
Journal of Symbolic Computation 1986-1996
Mathematical Structures in Computer Science 1992-2002
Journal of Philosophical Logic 1982-
Journal of Logic and Computation 1991-
Logic Journal of IGPL 1997-

COURSES TAUGHT at Stanford

Modal logic, Model Theory, First Order Logic, Computability and Logic, Proof theory, Topics in Logic, Philosophy of Mathematics, Freshman Seminar: What is the Truth, Recursion Theory, Graduate seminar on Negation (joint with J. Moravcsik)

Interpolation Theorems (master's course, University of Amsterdam)

Modal Logic (graduate course,Royal Inst. of Technology, Stockholm)

Graduate Seminar on Negation (with J. Moravcsik) Stanford, w. 2000

Epsilon Calculus with Applications