A polarized version of Girard, Scedrov and Scott's Bounded Linear Logic is introduced and its normalization properties studied. Following Laurent, the logic naturally gives rise to a type system for the λμ-calculus, whose derivations reveal bounds on the time complexity of the underlying term. This is the first example of a type system for the λμ-calculus guaranteeing time complexity bounds for typable programs.
展开▼
机译：介绍了吉拉德（Girard），希德罗夫（Scedrov）和斯科特（Scott）的有界线性逻辑（Bounded Linear Logic）的极化版本，并研究了其归一化特性。遵循Laurent，逻辑自然产生了λμ演算的类型系统，其推导揭示了底层项时间复杂性的界限。这是用于λμ演算的类型系统的第一个示例，该系统保证了可键入程序的时间复杂度范围。
展开▼
