Linear Logic, Lambda-calculus, and Explicit SubstitutionsDates: 9, 10 and 11 of October, from 15hs to 17hs. 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. 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/ |