Static analysis of functional programs via Linear Logic

This thesis investigates aspects of the general relationship between simply typed lambda-calculus and a linear term calculus based on Intuitionistic Linear Logic. It introduces a notion of minimization on linear lambda-terms that removes super ous nonlinear operations (storage). Two different embeddings of the simply typed lambda-calculus into the linear term calculus are studied with respect to their properties under minimization. We define operational semantics for both term calculi. In support of Abramsky's thesis, that linear types are useful in doing abstract interpretation of functional programs, we demonstrate - using translation together with minimization - a syntactic method to do strictness analysis on lambda-terms, via the linear typing calculus. This leads to useful optimizations of call-by-name reduction on lambda-terms