A Logical Framework with Infinitary Terms
Abstract
Logical frameworks are successful in modeling proof systems. Recently, CoLF extended the logical framework LF to support higher-order rational terms that enable adequate encoding of circular objects and derivations. In this paper, we propose CoLF as an alternative interpretation of CoLF-style signatures where terms are taken to be all possibly infinitary terms that are consistent with a given signature. In particular, we propose the notion of productive B\"ohm trees, a particular kind of typed -free B\"ohm trees that are closed under hereditary substitution. We show that the productive B\"ohm trees are capable of meta-encoding their own structure. Overall, we hope to establish CoLF as a new formal framework for the encoding of infinitary regular and non-regular structures.
Cite
@article{arxiv.2312.05919,
title = {A Logical Framework with Infinitary Terms},
author = {Zhibo Chen},
journal= {arXiv preprint arXiv:2312.05919},
year = {2023}
}