|
Descripción
|
|
|---|---|
| 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 full-reducing 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 full-reducing strategies are studied in detail and their hybrid nature is formally characterised, and a novel theory in the lambda-value 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 lambda-value calculus which are more refined than the existing ones. As for the practical contributions, efficient implementations of the full-reducing strategies considered in the theoretical part are inter-derived by program transformation. To this aim, the hybrid nature of these strategies is used to adjust the existing techniques for program transformation to obtain first-order abstract machines with a single control stack, and a novel calculus of closures is introduced which allows to reason locally on the implementations of full-reducing operational semantics. The novel calculus of closures eases the mechanical proof-checking of full-reducing environment-based machines. As a corollary, the generality of the practical contributions is showcased by inter-deriving operational semantics of the gradually-typed lambda calculus, which presents a layered structure in which a coercion calculus is plugged into a host simply-typed lambda calculus. | |
|
Internacional
|
Si |
|
ISBN
|
|
|
Tipo de Tesis
|
Doctoral |
|
Calificación
|
Sobresaliente |
|
Fecha
|
09/06/2014 |