We formulate a framework for describing behaviour of effectful higher-order recursive programs. Examples of effects are implemented using effect operations, and include: execution cost, nondeterminism, global store and interaction with a user. The denotational semantics of a program is given by a coinductive tree in a monad, which combines potential return values of the program in terms of effect operations. Using a simple test logic, we construct two sorts of predicate liftings, which lift predicates on a result type to predicates on computations that produce results of that type, each capturing a facet of program behaviour. Firstly, we study inductive predicate liftings which can be used to describe effectful notions of total correctness. Secondly, we study coinductive predicate liftings, which describe effectful notions of partial correctness. The two constructions are dual in the sense that one can be used to disprove the other. The predicate liftings are used as a basis for an endogenous logic of behavioural properties for higher-order programs. The program logic has a derivable notion of negation, arising from the duality of the two sorts of predicate liftings, and it generates a program equivalence which subsumes a notion of bisimilarity. Appropriate definitions of inductive and coinductive predicate liftings are given for a multitude of effect examples. The whole development has been fully formalized in the Agda proof assistant.

翻译：我们设计了一个框架来描述具有效果的更高阶递归程序的行为。 效果实例是使用效果操作来执行的, 包括: 执行成本、 非确定性、 全球存储和与用户的互动。 一个方案的批注性语义是由一双月圆形的硬树给出的, 它结合了该方案在效果操作方面的潜在回报值。 使用简单的测试逻辑, 我们建造两种上游升降, 将结果类型的上游升到产生该类型结果的计算结果的上游, 每一个都捕捉到程序行为的表面。 首先, 我们研究可用于描述完全正确性效果概念的初始升降。 第二, 我们研究一个可追溯性上游升升降, 描述部分正确性的效果概念。 这两种构造是双重的, 其含义是: 一种可以用来扭曲另一个的。 上游升升升, 用作更高级方案的内在行为特性的内在逻辑基础。 程序逻辑有一个可衍生的否定概念, 由两种形式上的双向升动性升动概念概念的双重性概念概念, 其尾部位化的亚, 它具有一个正式性等级概念的双重性定义, 的后级, 它具有双重的翻升的翻级的序。