Viðburðadagatal TD

ICE-TCS seminar: Álvaro García Pérez

  • 24.10.2014, 14:00 - 15:00

ICE-TCS-logo-200pxWhere: M109, Reykjavík University, Menntavegur 1.
When: Friday, 24 October 2014, at 2pm
Title: Operational Aspects of Full Reduction in Lambda Calculi
Speaker: Álvaro García Pérez

My thesis studies full reduction in lambda calculi. In a nutshell, full reduction consists on evaluating the body of the functions in a functional programming language with binders. The classical (i.e., pure untyped) lambda calculus is set as the formal system that models the functional paradigm. Full reduction is a prominent technique when programs are treated as data objects, for instance when performing optimisations by partial evaluation, or when some attribute of the program is represented by a program itself, like the type in modern proof assistants.

A notable feature of many full-reducing operational semantics is its hybrid nature, which I introduce and which constitutes the guiding theme of the thesis. The hybrid nature amounts to a `phase distinction' in the treatment of binders when considered either from outside or from inside the abstractions.

From a programming languages standpoint, I show how to derive implementations of full-reducing operational semantics from their specifications, by using program transformations techniques. The program transformation techniques are syntactical equivalence-preserving transformations of semantic artefacts. I also show how full reduction impacts the semantics that use the environment technique. The environment technique is a key ingredient of real-world implementations of abstract machines which circumvents the issue with binders.

From a formal systems standpoint, I disclose a novel consistent theory for the call-by-value variant of the lambda calculus which accounts for full reduction. This novel theory entails a notion of observationality which distinguishes more points than other existing theories for the call-by-value lambda calculus. This contribtion helps to establish a `standard theory' in that calculus which consitutes the analogous of the `standard theory' advocated by Barendregt in the classical lambda calculus. I present some proof-theoretical results and give insights on the model-theoretical study, which is future work.