We propose a calculus for modeling implicit programming that supports first-class, overlapping, locally scoped, and higher-order instances with higher-kinded types. We propose a straightforward generalization of the well-established System $F^\omega$ to implicit parameters, with a uniform treatment of type and term abstractions. Unlike previous works, we give a declarative specification of unambiguous, and thus coherent, resolution without introducing restrictions motivated by an algorithmic formulation of resolution.

翻译：我们提出了一种用于建模隐式编程的演算，该演算支持具有高阶类型的一等、重叠、局部作用域及高阶实例。我们对已确立的系统 $F^ω$ 进行了直接推广，以支持隐式参数，并对类型抽象和项抽象进行了统一处理。与先前工作不同，我们给出了无歧义（因而也是一致性）解析的声明式规范，而无需引入由解析的算法化表述所驱动的限制。