Projects per year
We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our approach is well adapted to deal with extensions of the call-by-name and call-by-value λ-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with β-reduction. We then closely analyze some common factorization schemas for the λ-calculus. Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno’s non-deterministic λ-calculus and - for call-by-value - Carraro and Guerrieri’s shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
|Title of host publication||29th EACSL Annual Conference on Computer Science Logic (CSL 2021)|
|Editors||Christel Baier, Jean Goubault-Larrecq|
|Publisher||Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing|
|Number of pages||25|
|Publication status||Published - 15 Jan 2021|
|Event||29th EACSL Annual Conference on Computer Science Logic (CSL 2021) - Lubijana, Slovenia|
Duration: 25 Jan 2021 → 28 Jan 2021
|Name||Leibniz International Proceedings in Informatics (LIPIcs)|
|Conference||29th EACSL Annual Conference on Computer Science Logic (CSL 2021)|
|Period||25/01/21 → 28/01/21|
FingerprintDive into the research topics of 'Factorize Factorization'. Together they form a unique fingerprint.
- 1 Active
1/01/19 → 30/07/22
Project: Research council