PLDI, ECOOP, Curry On, DEBS, LCTES and ISMM (series) / ECOOP 2017 (series) / FTfJP 2017 (series) / (Formal Techniques for Java-like Programs) /
Generic Approach to Certified Static Checking of Module-like Constructs
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 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 20 Jun
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | |||
14:00 20mTalk | Generic Approach to Certified Static Checking of Module-like Constructs FTfJP Julia Belyakova Southern Federal University Pre-print | ||
14:20 35mTalk | 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 35mTalk | Mutable WadlerFest DOT FTfJP | ||
