The $K_\infty$ Homotopy $λ$-Model
This work addresses foundational issues in lambda calculus semantics for theoretical computer science, but appears incremental as it builds on existing models.
The authors tackled the problem of interpreting higher-order conversions in lambda calculus by extending Dana Scott's D∞ to a complete weakly ordered Kan complex K∞, resulting in a model that guarantees non-equivalence for certain βη-conversions.
We extend the complete ordered set Dana Scott's $D_\infty$ to a complete weakly ordered Kan complex $K_\infty$, with properties that guarantee the non-equivalence of the interpretation of some higher conversions of $βη$-conversions of $λ$-terms.