A Theory Of Variable Types.
A well-ordering proof for Feferman's theory To.
Constructing Kripke models of certain fragments of Heyting's arithmetic.
Definitions: the primitive concept of logics or The Leśniewski-Tarski legacy [Book]
Einstein Structures: Existence Versus Uniqueness.
Expressions indéterminées, constructivisme et axiome du choix
Integrating intuitionistic and classical theories
Interpretationen der Heyting-Arithmetik endlicher Typen.
Numerology in topoi.
On a weakening of Markov's principle.
Presentation of Natural Deduction
Strong normalization of barrecursive terms without using infinite terms.
The "World's Simplest Axiom of Choice" Fails.
Базы допустимых правил логик S4 и Int
Георг Кантор как автор конструкций, играющих фундаментальные роли в конструктивной математике
Критерий допустимости правил в модальной системе S4 и интуиционистской логике.