@inproceedings{bbf229d5607d49569fe4730572dd7f23,
title = "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 [8]. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley's rewriting closely corresponds to preemptive rewriting [5], a technical device used in the meta-theory of maximal multi-focus.",
keywords = "Extensional sums, Maximal multi-focusing, Natural deduction, Rewriting",
author = "Gabriel Scherer",
note = "Publisher Copyright: {\textcopyright} Gabriel Scherer;.; 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 ; Conference date: 01-07-2015 Through 03-07-2015",
year = "2015",
month = jul,
day = "1",
doi = "10.4230/LIPIcs.TLCA.2015.317",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
pages = "317--331",
editor = "Thorsten Altenkirch",
booktitle = "13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015",
}