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.
Type de document :
Communication dans un congrès
Typed Lambda Calculi and Applications, Jun 2015, Warsaw, Poland. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), 2015, <http://drops.dagstuhl.de/portals/extern/index.php?semnr=15006>
Liste complète des métadonnées


https://hal.inria.fr/hal-01235372
Contributeur : Scherer Gabriel <>
Soumis le : lundi 30 novembre 2015 - 10:17:13
Dernière modification le : mercredi 2 décembre 2015 - 01:08:45
Document(s) archivé(s) le : samedi 29 avril 2017 - 01:01:51

Fichier

multifoc_sums-long.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

  • HAL Id : hal-01235372, version 1

Collections

Citation

Gabriel Scherer. Multi-focusing on extensional rewriting with sums. Typed Lambda Calculi and Applications, Jun 2015, Warsaw, Poland. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), 2015, <http://drops.dagstuhl.de/portals/extern/index.php?semnr=15006>. <hal-01235372>

Partager

Métriques

Consultations de
la notice

117

Téléchargements du document

39