Search papers, labs, and topics across Lattice.
The paper introduces Lightweight C (LC), a core calculus formalizing a subset of ANSI C, and Colored LC (CLC), an extension of LC with ANSI C preprocessor directives. A type system for CLC is defined to ensure that all programs generated by the C preprocessor are well-typed C programs. This provides a formal foundation for type-safe product lines of C programs.
Guarantee type safety across product lines of C programs using a novel calculus with preprocessor directives.
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.
