IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2009 > The beta-cube. A space of evaluation strategies for the untyped lambda-calculus

Álvaro García Pérez

Tuesday, December 15, 2009

11:00am Meeting room 302 (Mountain View), level 3

Álvaro García Pérez, PhD Student, IMDEA Software Institute

The beta-cube. A space of evaluation strategies for the untyped lambda-calculus

Abstract:

Different evaluation orders for the untyped(1) lambda-calculus exists (call-by-value, call-by-name, normal order, applicative order…), reflecting the nuances in the evaluation of a system which serves as the foundation of functional programming languages.

In this talk, I will introduce a generic evaluator (written in Haskell) which can be instantiated to any evaluator realising a particular evaluation order. For this purpose, I will recall some notions of the untyped lambda-calculus, give an algebraic data type representing lambda-terms, present the big-step semantics of the evaluation orders using natural deduction rules, implement them (using CPS following Reynolds’ advice and showing alternative solutions in Haskell), show how monads can help to write neater code, present a way to hybridate existing evaluation orders to produce new ones, comment about an absortion theorem regarding hybridation and describe something I call the “beta-cube”.

(1) We prefer to use “untyped” rather than “pure” so as to avoid recent controversy regarding the latter word.