This is the first part of a two-part special issue of Mathematical Structures in Computer Science dedicated to the memory of our friend and colleague, Martin Hofmann.
On 21 January 2018, Martin Hofmann died in a tragic mountain hiking accident in Japan. He was there to attend a workshop at NII Shonan and arrived early for the workshop in order to spend a day climbing Mount Nikkō-Shirane. On his way down from the 2578-m summit, he was caught in a severe snowstorm and lost his way back to safety.
Martin Hofmann studied for a Diplom in Informatics at Universität Erlangen-Nürnberg from November 1984 until August 1991. During an exchange visit at the Université de Nice from October 1987 to June 1988, he obtained in addition the ‘Maitrise de Mathematiques’. In 1991, he joined the Laboratory for Foundations of Computer Science at the University of Edinburgh. He obtained his PhD in June 1995 with a dissertation entitled ‘Extensional Concepts in Intensional Type Theory’, which won the Distinguished Dissertation Award from the British Computer Society.
From September 1995 to March 1998, Martin Hofmann was a Research Assistant at the Department of Mathematics of the Technische Universität Darmstadt, where he obtained the Habilitation degree in February 1999, with a thesis entitled ‘Type Systems for Polynomial-time Computation’.
In 1998, he returned to the University of Edinburgh, first as Lecturer, then Reader at the School of Informatics. After a short stay in Darmstadt with a position as Assistant Professor from April 2001, he became Full Professor for Theoretical Computer Science at Ludwig-Maximilians-Universität München in September 2001.
His scientific interests covered a broad range of topics involving the application of logic and type theory to programming and programming languages. These covered a spectrum from deep theoretical work on Martin-Löf type theory and topics in programming language semantics, to application-driven work on resource-bounded computation for mobile code and embedded systems. His work at the applied end of the spectrum was firmly supported by and grew directly from his work at the theoretical end of the spectrum, demonstrating the truth of the claim ‘There is nothing as practical as a good theory’. He was the author of over 150 articles in journals and top international conferences.
Martin Hofmann was most known for his research on the relationship between extensional properties (input/output semantics) and intensional properties (relating to the code/algorithm) of computation. This started with his PhD thesis, which showed how the convenience and power of extensional reasoning could be soundly obtained within intensional type theory. One idea in this work was an early version of the univalence principle which later came to fame through Voevodsky’s Homotopy Type Theory.
His later research concerned ‘implicit computational complexity’, again involving the extensional/intensional distinction, in which particular complexity classes are shown to correspond with the programs that are expressible in particular (fragments of) programming languages. This led directly to the design of type systems for programming languages in which a close upper bound on the heap space consumption of a program could be obtained from its type. Remarkably, types incorporating this information can be inferred automatically from code. The same ideas apply to time complexity, and he pursued practical applications to situations in which resource bounds are important, for instance, embedded systems.
The relationship between intensional and extensional aspects of computation was the topic of the workshop that he was in Japan to attend due to start the day after his fatal accident.
Martin Hofmann was in demand worldwide as a scientific collaborator, invited speaker, project partner, and for service on journal editorial boards and conference programme committees. On his return from Japan, his work as programme chair of LICS 2018 was scheduled to begin. He was an immensely creative and mathematically talented scientist, whose formidable intellectual power wasmasked by his friendly, generous and modest personality. He left us at the age of only 52 years, in his scientific prime.
Both parts of this special issue in Martin Hofmann’s memory contain contributions from collaborators and scientific friends on topics related to his own work. In some cases, these are finished versions or continuations of work that was begun with Martin himself, and he appears as an author. A few papers offer overviews of some of his particular areas of interest, rather than offering novel scientific contributions. The papers on type theory find their place in this first part, while those dealing with resources will be included in the second part. Other ‘miscellaneous’ contributions will be found in both parts.
Acknowledgements
We would like to thank the authors for their contributions and the referees for their help with quality control. We would like to thank Sabine Broda for the photograph ofMartin and Annette Hofmann and Sandra Alves for their help in tracing it back to Sabine.
