Campus Event Calendar
Event Entry
What and Who
Step-indexed Semantic Models for Functional and Imperative Objects
Catalin Hritcu
IMPRS-CS
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 26 February 2007
08:00
-- Not specified --
E1 4
024
Saarbrücken
Abstract
Recently, deductive verification has witnessed significant progress
> towards local and modular reasoning about stateful programs. However,
> the usual semantic models one employs to prove soundness of program
> logics can become highly complex in the presence of realistic memory
> models. Based on previous results by A. Appel, A. Ahmed and others, we
> have developed step-indexed semantic models of types for the
> functional and imperative object calculi. Using only the small-step
> operational semantics, types are interpreted as sets of indexed
> values. Informally, an expression has a certain type, if it behaves
> like an element of that type for a fixed number of steps. This
> technique gives rise to simple, purely set-theoretic models of general
> references, recursive and polymorphic types. Our work extends these
> results to object types, subtyping, bounded quantification and self
> types. We believe that this can be the first step towards a new
> separation logic for object-oriented programs.
> towards local and modular reasoning about stateful programs. However,
> the usual semantic models one employs to prove soundness of program
> logics can become highly complex in the presence of realistic memory
> models. Based on previous results by A. Appel, A. Ahmed and others, we
> have developed step-indexed semantic models of types for the
> functional and imperative object calculi. Using only the small-step
> operational semantics, types are interpreted as sets of indexed
> values. Informally, an expression has a certain type, if it behaves
> like an element of that type for a fixed number of steps. This
> technique gives rise to simple, purely set-theoretic models of general
> references, recursive and polymorphic types. Our work extends these
> results to object types, subtyping, bounded quantification and self
> types. We believe that this can be the first step towards a new
> separation logic for object-oriented programs.
Contact
IMPRS
225
--email hidden
passcode not visible
logged in users only
Andrea Primm, 02/20/2007 11:17 -- Created document.