Gentzen-Style and Novikov-Style Cut-Elimination. - Sergei Tupailo (LFCS, 1992)

On a Proof-Theoretical Analysis of Sigma-1, 1-AC, Sigma-1, 1-DC and Delta-1, 1-CA. - Sergei Tupailo (LPAR, 1994)

Epsilon substitution method for elementary analysis. - Grigori Mints; Sergei Tupailo; Wilfried Buchholz (Arch. Math. Log., 1996)

Realization of Analysis into Explicit Mathematics. - Sergei Tupailo (J. Symb. Log., 2001)

Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe. - Sergei Tupailo (Ann. Pure Appl. Log., 2003)

Epsilon Substitution Method for Delta11-CR: a Constructive Termination Proof. - Sergei Tupailo (Log. J. IGPL, 2003)

On the intuitionistic strength of monotone inductive definitions. - Sergei Tupailo (J. Symb. Log., 2004)

Characterizing the interpretation of set theory in Martin-Löf typetheory. - Michael Rathjen; Sergei Tupailo (Ann. Pure Appl. Log., 2006)

Consistency of strictly impredicative NF and a little more ... - Sergei Tupailo (J. Symb. Log., 2010)