Abstract



This thesis studies full reduction in lambda calculi and the lambda theories involving it. The work departs from a systematic way of synthesising reduction strategies, which reveals a recurrent feature of the fullreducing ones: they present a layered structure where a hybrid strategy depends on one or more subsidiary strategies. Hybridisation pervades the theory and the practice of full reduction and constitutes the guiding theme in this thesis. The contributions are twofold. As for the theoretical contributions, the fullreducing strategies are studied in detail and their hybrid nature is formally characterised, and a novel theory in the lambdavalue calculus is introduced, which is the natural counterpart of the standard theory in the pure untyped lambda calculus. This theory, which was missing, allows to equate the undefined terms in a consistent and complete way, giving rise to notions of solvability and sensibility in the lambdavalue calculus which are more refined than the existing ones. As for the practical contributions, efficient implementations of the fullreducing strategies considered in the theoretical part are interderived by program transformation. To this aim, the hybrid nature of these strategies is used to adjust the existing techniques for program transformation to obtain firstorder abstract machines with a single control stack, and a novel calculus of closures is introduced which allows to reason locally on the implementations of fullreducing operational semantics. The novel calculus of closures eases the mechanical proofchecking of fullreducing environmentbased machines. As a corollary, the generality of the practical contributions is showcased by interderiving operational semantics of the graduallytyped lambda calculus, which presents a layered structure in which a coercion calculus is plugged into a host simplytyped lambda calculus.  
International

Si 


Type

Doctoral 
Mark Rating

Sobresaliente 
Date

09/06/2014 