[TYPES/announce] New Lambda Calculus book

[Henk Barendregt]

Dear colleagues,

We are delighted to announce that our new book
"A Lambda Calculus Satellite"
has been recently published. This book presents the state of the art
of research in lambda calculus in 2022, including the solutions to most open
problems raised in "The Lambda Calculus, its syntax and semantics"
(1981/84).
It contains many examples, exercises, and open problems for you to solve.
Further details are provided below.

Best wishes,

Henk Barendregt and Giulio Manzonetto

=================================================================

*** BOOK ANNOUNCEMENT ***

A Lambda Calculus Satellite - 1st Edition

Henk Barendregt, Radboud University
Giulio Manzonetto, University Sorbonne Paris Nord
with chapters by
Stefano Guerrini and Vincent Padovani

College Publications, October 2022

602 pages, ISBN 978-1-84890-415-6

https://urldefense.com/v3/__https://tinyurl.com/mryxjksn__;!!IBzWLUs!TDSYugG1yjtKvhrRBdf0bb_0WSoSgUqgLbDyROIL60x2LaZ1_wBpzW7soGm7dNxRzivOt79uM22YVlvrn8bX5DqY_psOPLLsG1E$ 

=================================================================

DESCRIPTION:

In 1936 the notion of intuitive computability was operationalized in
two different ways: via Turing machines and via lambda-calculus. The
difference consisted in manipulating beads (bits) for the former
approach versus manipulating trees (rewriting lambda-terms) for the
latter. Both proposals turned out to formalize the same notion of
computability, and led to the Church-Turing Thesis, claiming that
intuitive computability is captured in the correct way.

This resulted in the foundation of imperative and functional
programming. Variants of lambda-calculus are being used in another
powerful field of applications, namely proof-checking, the basis for
certifying mathematical theorems and thereby high tech industrial
products. These two areas of research are still being actively
investigated and make lambda-calculus a major tool in the present
stages of science and of the industrial revolution.

In this book lambda-calculus is considered from another angle: as a
study of these tree-like structures, investigating the relation
between their shape and their action. This is like studying numbers
qualitatively, rather than for their applications dealing
quantitatively with objects and phenomena in the world.

Barendregt's book 'The Lambda Calculus, its Syntax and Semantics?
(1981/84), does treat the subject from the same methodological
viewpoint, and includes several open conjectures. In the more than
four decades that have passed, most---but not all---of these
conjectures have been solved, sometimes in ingenious PhD theses. This
'Satellite' to the aforementioned book presents these solutions in a
uniform style and adds other topics of interest.

=================================================================

CONTENTS:

Acknowledgements
About lambda-calculus
About this book
General notations
I) Preliminaries
1 The lambda-calculus in a nutshell
2 Böhm trees and variations
3 Theories and models of  lambda-calculus
II) Reduction
4 Leaving a beta-reduction plane
5 Optimal lambda reduction (chapter by Stefano Guerrini)
6 Infinitary lambda calculus
7 Starlings (chapter by Vincent Padovani)
III) Conversion
8 Perpendicular Lines Property
9 Bijectivity and invertibility in lambda-eta
IV) Theories
10 Sensible theories
11 The kite
V) Models
12 Ordered models and theories
13 Filter models
14 Relational models
15 Church algebras for lambda-calculus
VI) Open Problems
16 Open Problems
VII) Appendix A
Mathematical background

References
Indices
===================================================
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20221129/2cbddeeb/attachment.htm>