Inaugural Lectures: Glynn Winskel & Thomas Jensen

To celebrate their appointments as Professors at the Department of Computer Science at the University of Copenhagen, Glynn Winskel and Thomas Jensen will give their inaugural lectures on 12 May 2022 at 1 and 2:15 PM, followed by a reception.

Glynn Winskel: Making concurrency functional

This talk bridges between two major paradigms in computation, the *functional*, at basis computation from input to output, and the *interactive*, where computation reacts to its environment while underway. Central to any compositional theory of interaction is the dichotomy between a system and its environment. Concurrent games and strategies address the dichotomy in fine detail, very locally, in a distributed fashion, through distinctions between Player moves (events of the system) and Opponent moves (those of the environment). A functional approach has to handle the dichotomy much more ingeniously, through its blunter distinction between input and output. This has led to a variety of functional approaches, specialised to particular interactive demands. Through concurrent games we can more clearly see what separates and connects the differing paradigms, and show how:

— several paradigms of functional programming and logic arise naturally as subcategories of concurrent games, including stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics; and their extensions to containers in dependent lenses and optics.

— to transfer enrichments of strategies (such as to probabilistic, quantum or real-number computation) to functional cases.

Bio

On 1 October, Glynn started as a part-time Professor in the PLTC section. Besides this, he is a part-time Professor at the University of Strathclyde, Scotland, and is an Emeritus Professor and distinguished visitor at the University of Cambridge, UK.

Originally, Glynn studied Mathematics at the University of Cambridge, and Mathematical Logic at Oxford, UK, before turning to Computer science for his PhD at Edinburgh. Afterward, he worked as a Royal Society Postdoc at Carnegie Mellon University, US, invited by Dana Scott. Then he took up a lectureship at the University of Cambridge and a professorship at Aarhus University. At Aarhus University, he was awarded funding by Denmark's Grundforskning foundation to head a research centre in Basic Research in Computer Science (BRICS).

Glynn rejoined the University of Cambridge as a Professor of Computer Science in 2000. He was awarded an Advanced Grant by the European Research Council for his project 'Events, Causality and Symmetry – the next generation semantics' in 2011. Also, he is a member of the Academia Europaea.

At DIKU, Glynn has worked with researchers with structural game theory, in particular in the semantics and analysis of quantum computation.

Thomas Jensen: Software security from program analysis

Software is the core of all digital technologies. Engineering secure software is therefore a key challenge for constructing IT infrastructures, services and products that we can trust.  Secure software must enforce security polices that protect the confidentiality, the integrity and the availability of data and services against attacks but implementing such protection mechanisms is difficult and errors may have serious security implications. In this talk, I will argue that this challenge can be addressed from a programming language perspective, through improved language design and automatic program analysis techniques.  I will show how different kinds of attacks on software have lead to a number of fundamental security properties, whose verification, in turn, have given rise to novel data, control and information flow analyses.  Using static program analysis as guardians in a security architecture puts strong requirements on their correctness, and raises the question: who guards the guards? In the second part of the talk, I will outline how formal semantics combined with automated reasoning can be used to obtain increased confidence in these key software components.

Bio

Thomas Philip Jensen is a Professor at the Programming Languages and Theory of Computing Section of the Department of Computer Science at the University of Copenhagen. His area of research is semantics-based program analysis and software security. He has made contributions to the foundations of static program analysis, the relationship between types and abstract interpretation, certification of static analyses and analysis of Java. He has been involved in several industrial technology transfers around Java smart cards, the most recent of which is a tool for the automated certification of Java Card applications against NFC industry norms for secure programming.

Programme

13:00 - 14:00	Inaugural lecture by Professor Glynn Winskel
14:00 - 14:15	Break
14:15 - 15:15	Inaugural lecture by Professor Thomas Jensen
15:15 - 16:00	Joint reception

The lectures will take place at:

Auditorium 1

August Krogh Institute

Universitetsparken 13

2100 Copenhagen