论文标题
打开高阶逻辑（长版）
Open Higher-Order Logic (Long Version)
论文作者
论文摘要
我们对Barthe等人的高阶逻辑引入了一种变体，其中公式被解释为谓词，而不是封闭的对象。这样，遵循基础程序的结构，可以以非常自然的方式表达和推理具有内在功能性质的概念，例如连续性，可怜性或单调性。我们以不同的风味给出了开放的高阶逻辑，尤其是在其关系和本地版本中，后者是针对属性仅在基础函数的一部分定义域中量身定制的。
We introduce a variation on Barthe et al.'s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function's domain of definition.
