A Core Calculus for Type-safe Product Lines of C Programs

TL;DR

This paper introduces a formal core calculus for C programming that ensures type safety across preprocessor variants, aiding both theoretical understanding and educational purposes.

Contribution

It formalizes Lightweight C and Colored Lightweight C, providing a type system that guarantees well-typed programs after preprocessing.

Findings

Formalization of a subset of C without preprocessor directives

Type system guarantees well-typedness of preprocessed programs

Potential usefulness for teaching C programming and analysis

Abstract

In this paper we: (1) propose Lightweight C (LC), namely a core calculus that formalizes a proper subset of the ANSI C without preprocessor directives; (2) define Colored LC (CLC), namely LC endowed with ANSI C preprocessor directives; and (3) define a type system for CLC that guarantees that all programs to be generated by the C preprocessor are well-typed C programs. We believe that the simple formalization provided by CLC could be useful also for teaching purposes. Stefano Berardi spent most of his academic career at the Department of Computer Science of the University of Turin, where he conducts outstanding research on the logical foundations of computer science and on type-based program analyses. Over the years, he taught many courses, from BSc courses on programming with C to PhD courses on program analysis. Therefore, this paper fully falls within Stefano Berardi's research and teaching activities.