A new coinductive confluence proof for infinitary lambda calculus
arXiv:1808.05481 · doi:10.23638/LMCS-16(1:31)2020
Abstract
We present a new and formal coinductive proof of confluence and normalisation of Böhm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this result. The technique of the proof is new, i.e., it is not merely a coinductive reformulation of any earlier proofs. We formalised the proof in the Coq proof assistant.
arXiv admin note: text overlap with arXiv:1501.04354
References in corpus (5)
- Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction
- Nominal Coalgebraic Data Types with Applications to Lambda Calculus
- Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
- Partial Order Infinitary Term Rewriting
- Coinduction: an elementary approach