Place: Depto. de Computación, FCEyN, UBA.

Room: Tu 9/10 and Wed 10/10 in AULA 8 and Thu 11/10 in AULA 4.

Slides: Part 1, Part 2, Part 3, Part 4

Abstract:

In this mini-course we shall present a new simple theory of explicit
substitutions for the lambda calculus. The course is organized in
three parts:

1) Logical foundations. The theory originates from a detailed analysis
of lambda-calculus via Linear Logic. We introduce Linear Logic and
Proof-Nets, the graphical syntax for Linear Logic. Then, we show how
to represent the lambda-calculus and its dynamics inside Linear Logic.

2) Rewriting theory. We overview the rewriting theory (confluence,
termination, factorization, developments, residuals) of a family of
explicit substitution calculi "at a distance". Pleasantly, such
rewriting theory admit simple and elegant proofs, based on few simple
concepts.

3) Applications. We show some applications of the developed theory.
Historically, the theory of explicit substitutions was conceived to
relate the lambda calculus to its implementation. In contrast, the new
theory is a sophisticated tool to study the lambda-calculus itself. We
shall show results about cost-models, call-by-value/need evaluation,
and refinements of lambda calculus with permutative conversions.

Capsule bio:

Currently, I am post-doc at Carnegie Mellon University (Pittsburgh, PA),
working with Frank Pfenning on the meta-CLF project. Previously, I have
been post-doc in the PARSIFAL INRIA team (2011-2012), ATER at Paris 13
University in the LIPN lab (2010-2011), and ATER at Paris 7 University in
the PPS lab (2009-2010). I did my Ph.D. in Computer Engineering at
University La Sapienza (Rome, Italy) under the supervision of prof.
Stefano Guerrini. Here you find some information concerning my research:
https://sites.google.com/site/beniaminoaccattoli/