一句话：提出扩展 Nuprl 类型论的新类型论 BITT，用 Beth 式语义嵌入自由选择序列并验证其关键公理。
经典可计算性由 Church-Turing 论题刻画，而 Brouwer 提出的自由选择序列允许非律则的、逐步自由选择且非确定地扩展的无穷序列，从而超出该框架。为在构造性类型论中容纳此类对象，本文提出 BITT——Nuprl 类型论的扩展。为支持选择序列不断演化且非确定的性质，BITT 对底层类型论作了重要修改：利用底层库作为状态存储已作出的选择，以保证后续选择与既有选择一致；同时采用 Beth 式语义刻画其动态性。作者形式定义 BITT，并用它解释和验证支配选择序列的基本公理，为完全直觉主义的 Nuprl 奠定基础。
Church-Turing computability was extended by Brouwer who considered non-lawlike computability in the form of free choice sequences. Those are essentially unbounded sequences whose elements are chosen freely, i.e. not subject to any law. In this work we develop a new type theory BITT, which is an extension of the type theory of the Nuprl proof assistant, that embeds the notion of choice sequences. Supporting the evolving, non-deterministic nature of these objects required major modifications to the underlying type theory. Even though the construction of a choice sequence is non-deterministic, once certain choices were made, they must remain consistent. To ensure this, BITT uses the underlying library as state and store choices as they are created. Another salient feature of BITT is that it uses a Beth-like semantics to account for the dynamic nature of choice sequences. We formally define BITT and use it to interpret and validate essential axioms governing choice sequences. These results provide a foundation for a fully intuitionistic version of Nuprl.