Substitutions for Lambda-Free Higher-Order Terms

Vincent TrĂ©lat đŸ“§

April 25, 2024


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