Preface – Prefacio

Abstract

The preface of the latest volume of Theoretical Computer Science was dedicated to Jean-Yves Girard and as a short essay in French on the relation between proof theory and programming languages. This section described that the period of the 1980s led to increased co-ordinated between the fields of mathematics and computer science resulting in the establishment of Curry Howard isomorphism as a major backbone for research in this area. The rise of linear logic followed Girard's revisitation of system F while Girard constructed the first denotational model of polymorphism in 1984, reinventing Berry's stable functions for this purpose. A simplification of Berry/Winskel's framework of dI-domains and event structures led to coherence spaces and to the seminal decomposition of implication into a linear implication and an exponential modality, leading to a procedural, resource conscious vision of logic.