A Deforestation of Reducts: Refocusing
Olivier Danvy

TL;DR
This paper provides a formal proof, using Coq, of the refocusing transformation in small-step semantics, connecting reduction-based and reduction-free normalization methods, enhancing the rigor of prior informal proofs.
Contribution
It offers the first formal, Coq-based proof of refocusing, clarifying its correctness and formalizing an important concept in semantics.
Findings
Formal proof of refocusing using Coq
Clarification of the correctness of the transformation
Alignment with original simple idea of refocusing
Abstract
In a small-step semantics with a deterministic reduction strategy, refocusing is a transformation that connects a reduction-based normalization function (i.e., a normalization function that enumerates the successive terms in a reduction sequence -- the successive reducts) and a reduction-free normalization function (i.e., a normalization function that does not construct any reduct because all the reducts are deforested). This transformation was introduced by Nielsen and the author in the early 2000's with an informal correctness proof. Since then, it has been used in a variety of settings, starting with Biernacka and the author's syntactic correspondence between calculi and abstract machines, and several formal proofs of it have been put forward. This article presents a simple, if overdue, formal proof of refocusing that uses the Coq Proof Assistant and is aligned with the simplicity of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies
