We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system which is (sound and) complete for Scott-open properties defined in a fixpoint-like logic. Working on top of Abramsky's Domain Theory in Logical Form, we build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets. A realizability implication with the expected (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.

翻译：我们致力于证明处理无限数据（如流或非良基树）的函数的输入输出性质。我们提出了一种有限精化类型系统，该系统对于以不动点风格逻辑定义的Scott-Open性质是（可靠且）完备的。基于Abramski的"逻辑中的域理论"框架，我们从递归类型解释的Scott域是谱空间这一众所周知的事实出发。Scott-Open集与紧饱和集之间通常的对称性体现在逻辑极性上：正公式允许最小不动点并定义Scott-Open集，而负公式允许最大不动点并定义紧饱和集。利用具有预期极性（逆）变差的可实现性蕴含关系，可以将非平凡的输入输出性质表述为函数类型上的正公式。