Substitutions for Lambda-Free Higher-Order Terms

Vincent TrĂ©lat đŸ“§

April 25, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This theory provides a formalization of substitutions on \(\lambda\)-free higher-order terms, establishing a structured framework with the expected algebraic properties. It introduces a type construction for the rigorous definition and manipulation of substitutions. The main theorem of this theory proves the existence of fixed-point substitutions under acyclicity, a theorem that is too often regarded as trivial in the literature.


BSD License


Session Substitutions_Lambda_Free