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.