Observatorio de I+D+i UPM

Memorias de investigación
Thesis:
OPERATIONAL ASPECTS OF FULL REDUCTION IN LAMBDA CALCULI
Year:2014
Research Areas
  • Engineering
Information
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 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.
International
Si
Type
Doctoral
Mark Rating
Sobresaliente
Date
09/06/2014
Participants
  • Director: Juan Jose Moreno Navarro (UPM)
  • Director: Pablo Nogueira Iglesias (UPM)
  • Autor: Alvaro Garcia Perez (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2019 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)