Relational Semantics of Linear Logic and Higher-order Model Checking

摘要

In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any hig