AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Expert Audience

English

90 Minutes

Saarbrücken

The foundations both of first-order imperative languages and of
higher-order functional ones have been fairly well understood since
the 1970s. But good models and reasoning principles for the mix of
higher-order features and dynamically allocated mutable storage have
proved hard to find, although most programming languages, from machine
code to C# and ML, feature just such a combination. A number of
exciting logical and semantic developments, including separation,
relational program logics and step-indexing, have now started to let
us model, specify and verify programs in these languages. At the same
time, advances in mechanized reasoning (both automatic theorem provers
and proof assistants) are making it more feasible to apply our
theories to realistic programs and systems. In this talk, I'll survey
some of these theoretical ideas and show how we have applied them in
machine-formalized proofs of compiler correctness, addressing the
question of just what it means for a piece of machine code to
implement correctly a phrase of a typed high-level language.

Claudia Richter

688

--email hidden

Yes

Kaiserslautern

G26

206

passcode not visible

logged in users only