We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent nondeterministic programs are formalised by rather usual techniques, opaque nondeterministic programs are formalised by introducing in the syntax oracle constants, the behaviour of which is governed by oracular functions. The generality of these functions and the fact that their values are determined by the form of the whole term inside which the relative oracle occurs also enable us to simulate learning-like behaviours. We then extend the calculus in order to define a computational trustworthiness predicate. The extension of the calculus does not only enable us to precisely formalise a notion of trustworthiness and to encode the procedures required to test it on programs, but also to reason, by means of the type system, on the behaviour of programs with respect to trustworthiness.

翻译：我们定义了一个带依赖类型的λ演算扩展，该扩展使我们能够编码透明与不透明的概率程序，并通过可归约性技术为其证明了强规范化结果。虽然透明的非确定性程序可通过较为常规的技术形式化，但不透明的非确定性程序则通过在语法中引入预言机常数来形式化，其行为由预言函数所支配。这些函数的通用性，以及其值由相关预言机所在整个项的形式所决定这一事实，也使我们能够模拟类学习行为。随后我们扩展该演算以定义一个计算可信度谓词。该演算的扩展不仅使我们能够精确定义可信度的概念并编码测试程序可信度所需的流程，还能借助类型系统对程序在可信度方面的行为进行推理。