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.

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