Scholarlink

<p>We define a parameterized system for propositional Linear Logic which allows for a formalization in <Emphasis FontCategory="NonProportional">Rocq</Emphasis> which can be instantiated to the specific needs of the user. Parameters control the use of the exchange and mix rules in particular. The induced <Emphasis FontCategory="NonProportional">Rocq</Emphasis> library provides basic key properties of the system (and of some variants) such as cut admissibility, focusing, etc.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

YALLA: Yet Another Deep Embedding of Linear Logic in Rocq

  • 期刊论文

  • 发表日期：

    2026年5月21日

查看全文
  • Olivier Laurent

摘要

We define a parameterized system for propositional Linear Logic which allows for a formalization in Rocq which can be instantiated to the specific needs of the user. Parameters control the use of the exchange and mix rules in particular. The induced Rocq library provides basic key properties of the system (and of some variants) such as cut admissibility, focusing, etc.