Document Open Access Logo

Multi-Focusing on Extensional Rewriting with Sums

Author Gabriel Scherer

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.317.pdf
  • Filesize: 473 kB
  • 15 pages

Document Identifiers

Author Details

Gabriel Scherer

Cite As Get BibTex

Gabriel Scherer. Multi-Focusing on Extensional Rewriting with Sums. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 317-331, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.317

Abstract

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.

Subject Classification

Keywords
  • Maximal multi-focusing
  • extensional sums
  • rewriting
  • natural deduction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In LICS, 2001. Google Scholar
  2. Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In POPL, 2004. Google Scholar
  3. Taus Brock-Nannestad and Carsten Schürmann. Focused natural deduction. In LPAR (Yogyakarta), 2010. Google Scholar
  4. Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. In 21st EACSL Annual Conference on Computer Science Logic, volume 16, September 2012. Google Scholar
  5. Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In IFIP TCS, 2008. Google Scholar
  6. N Ghani. Beta-eta equality for coproducts. In Proceedings of TLCA'95, number 902 in Lecture Notes in Computer Science. Springer-Verlag, 1995. Google Scholar
  7. Neelakantan R. Krishnaswami. Focusing on pattern matching. In POPL, 2009. Google Scholar
  8. Sam Lindley. Extensional rewriting with sums. In TLCA, 2007. Google Scholar
  9. Dale Miller and Alexis Saurin. From proofs to focused proofs: A modular proof of focalization in linear logic. In CSL, 2007. Google Scholar
  10. Alexis Saurin. Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique). PhD thesis, École Polytechnique, 2008. Google Scholar
  11. Robert J. Simmons. Structural focalization. CoRR, abs/1109.6273, 2011. Google Scholar
  12. Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact