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.

翻译：本文中我们：(1)提出轻量级C语言(LC)，即一种形式化ANSI C语言无预处理器指令子集的核心演算；(2)定义着色LC语言(CLC)，即在LC基础上扩展ANSI C预处理器指令的语言；(3)为CLC设计类型系统，确保所有通过C预处理器生成的程序均为良类型的C程序。我们认为CLC提供的简洁形式化框架同样适用于教学目的。Stefano Berardi在都灵大学计算机科学系度过了其大部分学术生涯，他在计算机科学逻辑基础与基于类型的程序分析领域开展了卓越研究。多年来，他教授了从C语言编程本科课程到程序分析博士课程在内的多门课程。因此，本文完全属于Stefano Berardi的研究与教学活动范畴。