Write a Blog >>
Tue 20 Jun 2017 14:00 - 14:20 at Vertex WS217 - C Chair(s): Martin Berger

In this paper we consider the problem of certified static checking of module-like constructs of programming languages. We argue that there are algorithms and properties related to modules that can be defined and proven in abstract way. We advocate the design of a generic Coq library, which is aimed to provide three building blocks for each checking mechanism: propositional, computable, and correctness proofs. Implemented part of the library is justified by applying it to a certified static checker of an extension of STLC.

Tue 20 Jun

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

14:00 - 15:30
14:00
20m
Talk
Generic Approach to Certified Static Checking of Module-like Constructs
FTfJP
Julia Belyakova Southern Federal University
Pre-print
14:20
35m
Talk
Tracing sharing in an imperative pure calculus
FTfJP
Paola Giannini Universita' del Piemonte Orientale, Marco Servetto Victoria University of Wellington, Elena Zucca University of Genova
14:55
35m
Talk
Mutable WadlerFest DOT
FTfJP
Marianna Rapoport University of Waterloo, Ondřej Lhoták University of Waterloo, Canada