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开性质是（可靠且）完备的。基于Abramsky的逻辑形式域理论，我们从已知事实出发：解释递归类型的Scott域是谱空间。Scott开集与紧饱和集之间通常的对称性反映在逻辑极性上：正公式允许最小不动点并定义Scott开集，而负公式允许最大不动点并定义紧饱和集。具有预期（反）变极性可实现性蕴涵，使得非平凡的输入输出性质能够被表述为函数类型上的正公式。