首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:Multi-Focusing on Extensional Rewriting with Sums
  • 本地全文:下载
  • 作者:Gabriel Scherer
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:38
  • 页码:317-331
  • DOI:10.4230/LIPIcs.TLCA.2015.317
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley's rewriting closely corresponds to preemptive rewriting, a technical device used in the meta-theory of maximal multi-focus.
  • 关键词:Maximal multi-focusing; extensional sums; rewriting; natural deduction
国家哲学社会科学文献中心版权所有