Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proof systems, making the formalization of circular proof systems in such logical frameworks a cumbersome and awkward task. To address this issue, we propose CoLF, a conservative extension of LF with higher-order rational terms and mixed inductive and coinductive definitions. In this framework, two terms are equal if they unfold to the same infinite regular B\"ohm tree. Both term equality and type checking are decidable in CoLF. We illustrate the elegance and expressive power of the framework with several small case studies.

翻译：逻辑框架为演绎系统的规约与推理提供了自然且直接的方式。逻辑框架LF及其后续发展主要聚焦于有限证明系统，使得在此类逻辑框架中形式化循环证明系统成为一项繁琐而不便的任务。为解决这一问题，我们提出CoLF——一种对LF的保守扩展，引入高阶有理项及混合归纳与余归纳定义。在该框架中，两个项相等当且仅当它们展开为相同的无限正则Böhm树。CoLF中的项相等性及类型检查均可判定。通过若干小型案例研究，我们展示了该框架的优雅性与表达能力。