Title: A Lazy, Concurrent Convertibility Checker Show Chinese title

Title: 一种懒惰的并发可转换性检查器

Abstract: Convertibility checking - determining whether two lambda-terms are equal up to reductions - is a crucial component of proof assistants and dependently-typed languages. Practical implementations often use heuristics to quickly conclude that two terms are or are not convertible without reducing them to normal form. However, these heuristics can backfire, triggering huge amounts of unnecessary computation. This paper presents a novel convertibility-checking algorithm that relies crucially on laziness and concurrency} Laziness is used to share computations, while concurrency is used to explore multiple convertibility subproblems in parallel or via fair interleaving. Unlike heuristics-based approaches, our algorithm always finds an easy solution to the convertibility problem, if one exists. The paper presents the algorithm in process calculus style and discusses its mechanized proof of partial correctness, its complexity, and its lightweight experimental evaluation. Show Chinese abstract

Abstract: 可转换性检查——确定两个lambda项在归约下是否相等——是证明助手和依赖类型语言中的关键组成部分。实际实现通常使用启发式方法快速得出两个项是否可转换，而无需将它们归约到规范形式。然而，这些启发式方法可能会产生反效果，引发大量不必要的计算。本文提出了一种新颖的可转换性检查算法，该算法关键地依赖于惰性求值和并发性。惰性求值用于共享计算，而并发性用于并行或通过公平交错探索多个可转换性子问题。与基于启发式的方法不同，我们的算法如果存在简单的解决方案，总能找到解决可转换性问题的简单方法。本文以进程演算风格介绍了该算法，并讨论了其机械化的部分正确性证明、复杂度以及轻量级的实验评估。