2020/01/06 by Olimpieri, Federico
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2001.01619
The aim of this work is to characterize three fundamental normalization proprieties in lambda-calculus trough the Taylor expansion of λ-terms. The general proof strategy consists in stating the dependence of ordinary reduction strategies on their resource counterparts and in finding a convenient resource term in the Taylor expansion that behaves well under the considered kind of reduction.