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 Jun
|14:00 - 14:20|
Julia BelyakovaSouthern Federal UniversityPre-print
|14:20 - 14:55|
|14:55 - 15:30|