Конструктивная теория множеств с типами, совместность с тезисом Чёрча

Сформулирована интуиционистская теория с типами для множеств и функций, которая предназначена для формализации конструктивного анализа. Доказана совместность этой теории с некоторым вариантом тезиса Чёрча и ее интерпретируемость в классической арифметике второго порядка.
Библиогр. 2.