Seminario del grupo de Lógica y Computación: Interpreting Lambda Calculus via Category Theory

[Andrés Sicard-Ramírez]

Buenos días,

Elisabet Lobo (actualmente estudiante de doctorado en Chalmers) está
visitando la ciudad en estos días. A nombre del seminario del grupo
los
invito a la siguiente conferencia que ella ofrecerá:

Fecha: viernes, marzo 6 de 2018
Hora: 11 a.m. - 12 m.
Lugar: 29-205

Title: Interpreting Lambda Calculus via Category Theory (A pragmatic
programming guide for the non-expert)

Abstract: The programming language Haskell is well-known for easily
embedding domain-specific languages (EDSLs) via libraries. Many EDSLs
are designed as tools to easily express programs in other platforms.
The goal is to enjoy the features provided by the EDSLs and the host
language (e.g., types, compositionality, etc.) in order to obtain
well-behaved code in some low-level language. Such EDSLs are
implemented in a deep embedded fashion in order to enable
optimizations. Unfortunately, this kind of EDSLs sooner or later end
up repeating the work of the host compiler. Recently, a new approach
called Compiling to Categories [1] has emerged and promises to avoid
such replication of work. It relies on understanding the categorical
model of Cartesian Closed Categories (CCC). That means that, to use
this new technique, it becomes necessary to understand basic category
theory and CCC. Unfortunately, when learning about such topics and its
relation to functional programs, one faces the risk of diving into
mathematical books with difficult-to-penetrate notation, getting lost
in abstract notions, and eventually giving up. Instead, this pearl
aims to guide Haskell developers to the understanding of all of such
abstract concepts via Haskell code. We present two EDSLs in Haskell:
one for simply-typed lambda terms and another for CCC and show how to
translate programs from one into the other---a well-known result [2].
We also show how to execute CCC programs via the categorical abstract
machine (CAM). Moreover, we extend our implementation of simply-typed
lambda calculus with primitive operators, branching, and fix points
via appropriate enhancements to our EDSL of CCC and CAM based on
category theory concepts. All this journey is going to be grounded in
Haskell code, so that developers can experiment and stop fearing such
abstract concepts as we did.

[1] Conal Elliott. 2017. Compiling to categories. Proc. ACM Programing
Languages 1, ICFP, Article 48 (Sept. 2017), 24 pages.
https://doi.org/10.1145/3110271 .

[2] Joachim Lambek. 1986. Cartesian Closed Categories and Typed
Lambda-Calculi. In Proceedings of the Thirteenth Spring School of the
LITP on Combinators and Functional Programming Languages.
Springer-Verlag, 136–175.


This talk is based on a joint-work with Solène Mirliaz and Alejandro Russo.


La programación del seminario, así como las charlas de años
anteriores, se pueden consultar en

http://www.eafit.edu.co/investigacion/grupos/logica-y-computacion/seminar/Paginas/default.aspx


Si está interesado en recibir los anuncios de las futuras charlas,
favor inscribirse al grupo

https://groups.google.com/forum/#!forum/eafit-logic-and-computation


Favor compartir está invitación con las personas interesadas.


Un saludo,

Juan Francisco Cardona McCormick
Francisco José Correa Zabala
Andrés Sicard Ramírez


--
Andrés

[Andrés Sicard-Ramírez]

Buenos días,

Corrección. La conferencia será en las siguientes coordenadas:

Fecha: viernes, abril 6 de 2018

Hora: 11 a.m. - 12 m.
Lugar: 29-205

Un saludo,

On 3 April 2018 at 09:29, Andrés Sicard-Ramírez

--
Andrés