一句话：为最小主义基础内涵层 mtt 扩展归纳形式拓扑、Church 论题与选择公理，构造 Kleene 可实现性语义并在 CZF+REA 中形式化。
本文针对最小主义基础（Minimalist Foundation）的内涵层 mtt，在加入归纳生成的形式拓扑、Church 论题与选择公理后，如何保持构造性语义与一致性这一问题。作者提出一种 Kleene 可实现性语义，它扩展了此前用于证明 mtt 与选择公理、形式 Church 论题相容的可实现性解释。主要新颖之处在于，该语义不是在非形式元理论中描述，而是在 Aczel 构造集合论 CZF 加上正则扩张公理（REA）这一构造性理论中形式化。由此，论文为这些扩展提供可实现性语义基础，并延续通过构造集合论验证其一致性的路线。
We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mtt, extended with inductively generated formal topologies, Church's thesis and axiom of choice. This semantics is an extension of the one used to show consistency of the intensional level of the Minimalist Foundation with the axiom of choice and formal Church's thesis in previous work. A main novelty here is that such a semantics is formalized in a constructive theory represented by Aczel's constructive set theory CZF extended with the regular extension axiom.
@article{paperbot1308,
title = {A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice},
author = {Maria Emilia Maietti and Samuele Maschio and Michael Rathjen},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 2},
year = {2021},
doi = {10.23638/lmcs-17(2:21)2021}
}