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
14:00 - 15:30
|Generic Approach to Certified Static Checking of Module-like Constructs|
Julia Belyakova Southern Federal UniversityPre-print
|Tracing sharing in an imperative pure calculus|
|Mutable WadlerFest DOT|