Cálculo lambda con tipos

Opiniones de los lectores

Actualmente no hay opiniones de lectores. La calificación se basa en 3 votos.

Título original:

Lambda Calculus with Types

Contenido del libro:

Este manual con ejercicios revela en los formalismos, hasta ahora utilizados principalmente para el diseño y la verificación de hardware y software, una belleza matemática inesperada. El cálculo lambda constituye un prototipo de lenguaje de programación universal, que en su versión no tipada está emparentado con Lisp, y fue tratado en el clásico del primer autor The Lambda Calculus (1984).

Desde entonces, el formalismo se ha ampliado con tipos y se ha utilizado en programación funcional (Haskell, Clean) y asistentes de pruebas (Coq, Isabelle, HOL), empleados en el diseño y la verificación de productos informáticos y pruebas matemáticas. En este libro, los autores se centran en tres clases de tipado para términos lambda: tipos simples, tipos recursivos y tipos de intersección.

Es en estos tres formalismos de términos y tipos donde se revela la inesperada belleza matemática. El tratamiento es autorizado y completo, complementado con una bibliografía exhaustiva, y se proporcionan numerosos ejercicios para profundizar en la comprensión de los lectores y aumentar su confianza en el uso de los tipos.