# Generic Approach to Certified Static Checking of Module-like Constructs

## TL;DR

This paper proposes a generic Coq library framework for certified static checking of module-like constructs in programming languages, providing abstract algorithms and proofs, demonstrated through an extension of STLC.

## Contribution

It introduces a novel, abstract approach and a reusable Coq library for certified static checking of modules, applicable across different language extensions.

## Key findings

- Successfully implemented a certified static checker for an extension of STLC.
- The library provides propositional, computable, and correctness proof components.
- Framework enhances modularity and reusability of static checkers in formal verification.

## Abstract

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 an 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.