| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Multi-focusing on extensional rewriting with sums
Abstract : We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley [Lin07]. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley's rewriting closely corresponds to preemptive rewriting [CMS08], a technical device used in the meta-theory of maximal multi-focus.
Cited literature [11 references]
https://hal.inria.fr/hal-01235372
Contributor : Scherer Gabriel <>
Submitted on : Monday, November 30, 2015 - 10:17:13 AM
Last modification on : Tuesday, November 20, 2018 - 11:06:03 PM
Long-term archiving on: : Saturday, April 29, 2017 - 1:01:51 AM
Contributor : Scherer Gabriel <>
Submitted on : Monday, November 30, 2015 - 10:17:13 AM
Last modification on : Tuesday, November 20, 2018 - 11:06:03 PM
Long-term archiving on: : Saturday, April 29, 2017 - 1:01:51 AM
File
multifoc_sums-long.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License