On Tuesday 08/12/2009, at 15h30, in room Byron Blanc.
Speaker: Evgeny Makarov.
Abstract:
We propose a monadic higher-order language with recursion and mutable references where types can be annotated with pre- and postconditions in a manner similar to Hoare logic. Specifications in Hoare triples are written using separation logic, which allows expressing behavior of programs working with data structures stored in the heap, such as linked lists and trees, in a succinct local manner. Effect-free program terms may be freely used specifications, resulting in dependent types. We also describe an embedding in Coq and construction of a formalized proof of type safety.
