Some publications:

• V.N. Krupski. On Symbolic Models for Single-Conclusion Logic of Proofs. Matematicheskii Sbornik, 202:5, 63-67, 2011 (In Russian). English translation: Sbornik: Mathematics, 202:5, 683-695
• V.N. Krupski. Symbolic Models for Single-Conclusion Proof Logics.- In F.Ablaev, E.W. Mayr (Eds.) : CSR 2010, LNCS 6072, 276-287, 2010
• V.N. Krupski, V.E. Plisko. Theory of Algorithms M.: Academia, 2009 (book, in Russian). ISBN 978-5-7695-5293-9
• V.N. Krupski. Introduction to computational complexity. M.: Factorial Press, 2006 (book, in Russian). ISBN 5-88688-083-6
• Vladimir N. Krupski. Reference Constructions in the Single-conclusion Proof Logic (pdf) Journal of Logic and Computation v. 16, No.5, October 2006, 645-661 ; doi: 10.1093/logcom/exl028
• Vladimir N. Krupski. Referential Logic of Proofs (pdf) Theoretical Computer Science v. 357, No.1-3, 2006, pp.143-166. (elsevier.com)
• Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, and Aleksey Nogin. Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant. In David Basin and Burkhart Wolff, editors, 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, pages 29-39. Universitat Freiburg, 2003.
• Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu MetaPRL — A Modular Logical Environment. In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of Lecture Notes in Computer Science, pages 287--303. Springer-Verlag, 2003.
• V.N. Krupski.   Effective simultaneous approximability of reals (ps). Theoretical Computer Science, v. 284/2, 2002, pp 397-417
• V.N. Krupski.  The single-conclusion proof logic and inference rules specification (ps).   Annals of Pure and Applied Logic, v.113, No. 1-3, 2002, pp.181-206
• V.N. Krupski.  Operational Logic of Proofs with Functionality Condition on Proof Predicate (ps)  Lect. Notes Comput. Sci., 1997, v.1234, pp. 167-177
• S.N. Artemov, V.N. Krupski.  Data storage interpretation of labeled modal logic (ps).  Annals of Pure and Applied Logic, v.78, 1996, pp.57-71
• V.N. Krupski.   Efficient coding of approximations of real numbers (ps.gz) //  Mat. Zametki. 1990, v. 47, N 2, 46-57 (in Russian). English translation: Math. Notes 47, No. 2, 143-152 (1990)
• V.N. Krupski.  On simultaneous approximability of real numbers (ps.gz) // Doklady Akademii Nauk SSSR, 267, N.1, 1982, pp 45-48, (in Russian). English translation: Sov. Math. Dokl. 26, 545-547 (1982)
• V.N. Krupski.. On the complexity of description of computable approximations for points in metric spaces (ps.gz)  // Vestnik MGU, ser.1, 1981, N. 5, pp 3-9 (in Russian)

Some reports:

• V.N. Krupski. Reference constructions in the logic of proofs. III Moscow-Vienna Workshop on Logic and Computation, 31.04-01.05, 2004, Moscow. Slides (80K, pdf)