Wed 22 Nov 2023 09:10 - 10:10 at My (MDU Campus) - Keynote 1 Chair(s): Cristina Seceleanu

We present a direct-style denotational semantics of imperative programming languages in terms of finite maximal traces from initial to final states, and illustrate it on the While programming language.We prove that the new semantics agrees with a standard SOS. We then present a logic over finite traces, essentially an Interval Temporal Logic with recursion, and also provide it with a denotational semantics. The latter makes explicit the close connection between the logical operators and the statements of While. Based on this, we design a compositional proof calculus for proving finite-trace properties of While programs, and prove its soundness and relative completeness. Hence we achieve compositionality on all levels: semantics, logic, proof calculus.

I am Professor of Computer Science at TU Darmstadt, Germany. I received a PhD from University of Karlsruhe (now KIT) and a Habilitation from TU Vienna. From 2000 to 2011 I worked as an Associate, then Full Professor at Chalmers University of Technology.

Wed 22 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:10 - 10:10
Keynote 1NWPT 2023 at My (MDU Campus)
Chair(s): Cristina Seceleanu Mälardalen University
A Denotational Finite-Trace Semantics and Logic for While
NWPT 2023
Reiner Hähnle Technical University of Darmstadt