一句话：将强和（strong sum）引入聚焦逻辑，并指出其右投影类型依赖被投影项所带来的适配难题。
本文关注强和（strong sum）在聚焦逻辑中的适配问题。强和是一种依赖和类型，其消去通过投影而非模式匹配完成，因而表达力强，但也更难与聚焦证明论结合。核心障碍在于：强和的右投影类型会引用被投影的项，而在聚焦逻辑的结构中，当需要形成右投影规则时，该被投影项并不可用，导致通常的聚焦方法无法直接处理。摘要未给出具体解决方案、元定理或实现评估，但将该问题作为使强和融入聚焦逻辑的关键困难提出。
A useful connective that has not previously been made to work in focused logic is the strong sum, a form of dependent sum that is eliminated by projection rather than pattern matching. This makes strong sums powerful, but it also creates a problem adapting them to focusing: The type of the right projection from a strong sum refers to the term being projected from, but due to the structure of focused logic, that term is not available.
DOI 原文 ·
@inproceedings{paperbot4357,
title = {Strong Sums in Focused Logic},
author = {Karl Crary},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209145}
}