Reflections
on Type Theory, Lambda Calculus, and the Mind

Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday

Erik Barendsen, Herman Geuvers, Venanzio Capretta, Milad Niqui (Eds.)

Contents

Preliminary pages (Title, Preface, PhD Students of Henk Barendregt, Essays)

Classical Sequents and Computation : An Overview
Steffen van Bakel

Strictness Analysis via Resource Typing
Erik Barendsen and Sjaak Smetsers

Sharing in the Weak Lambda-Calculus Revisited
Tomasz Blanc, Jean-Jacques Lévy and Luc Maranget

Common Knowledge as a Coinductive Modality
Venanzio Capretta

Subtyping à la Church
Adriana Compagnoni and Healfdene Goguen

Intersection and Reference Types
Mariangiola Dezani-Ciancaglini and Simona Ronchi Della Rocca

Proving Lazy Folklore with Mixed Lazy/Strict Semantics
Marko van Eekelen and Maarten de Mol

Iteration and Primitive Recursion in Categorical Terms
Herman Geuvers and Erik Poll

Terms for Natural Deduction, Sequent Calculus and Cut Elimination in Classical Logic
Silvia Ghilezan

Lambda Calculus for Engineers
Pieter H. Hartel and Willem G. Vree

Intonation and Temperament: A Special Orchestral Rehearsal
Aline Honingh

Permission Specifications for Common Multithreaded Programming Patterns
Marieke Huisman and Clément Hurlin

Phine Numbers
Tonny Hurkens

On Henk Barendregt’s Favorite Open Problem
Benedetto Intrigila and Richard Statman

Semantics of Grammars and Attributes via Initiality
Bart Jacobs and Tarmo Uustalu

New Fixed Point Combinators from Old
Jan Willem Klop

Systematic Synthesis of Lambda-Terms
Pieter Koopman and Rinus Plasmeijer

Binary Relations as a Foundation of Mathematics
Jan Kuper

DNA, Differential Methods and the Böhm-out Technique
Giuseppe Longo and Pierre-Emmanuel Tendero

Infinite Multi-bases
Paula Severi

Sequent Calculus, Dialogues, and Cut-Elimination
Morten Heine Sørensen and Pawel Urzyczyn

A Strong Normalisation Condition for Pure Type Systems
Milena Stefanova and Silvio Valentini

Barendregt’s Lemma
Roel de Vrijer