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.
https://hal.inria.fr/hal-01235372
Contributeur : Scherer Gabriel
<>
Soumis le : lundi 30 novembre 2015 - 10:17:13
Dernière modification le : mardi 20 novembre 2018 - 23:06:03
Document(s) archivé(s) le : samedi 29 avril 2017 - 01:01:51
