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 properties, while negative formulae allow for greatest fixpoints and define compact-saturated properties. A realizability implication with the usual (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.

翻译：我们关注于证明处理无限数据（如流或非良基树）的函数的输入输出性质。我们提出了一种有限精化类型系统，该系统对于在类不动点逻辑中定义的Scott开性质是可靠且完全的。基于Abramsky的逻辑形式域理论，我们从已知事实出发：解释递归类型的Scott域是谱空间。Scott开集与紧饱和集之间通常的对称性反映在逻辑极性中：正公式允许最小不动点并定义Scott开性质，而负公式允许最大不动点并定义紧饱和性质。具有通常（反）变极性的可实现蕴含允许将非平凡的输入输出性质表述为函数类型上的正公式。