A Core Calculus for Type-safe Product Lines of C Programs
- URL: http://arxiv.org/abs/2603.04013v1
- Date: Wed, 04 Mar 2026 12:51:23 GMT
- Title: A Core Calculus for Type-safe Product Lines of C Programs
- Authors: Ferruccio Damiani, Daisuke Kimura, Luca Paolini, Makoto Tatsuta,
- Abstract summary: Lightweight C (LC) is a calculus that formalizes a proper subset of the calculus C without preprocessor directives.<n> Colored LC (CLC) is endowed with C preprocessor directives.<n>We believe that the simple formalization provided by CLC could be useful also for teaching purposes.
- Score: 2.1757527612572316
- License: http://creativecommons.org/licenses/by/4.0/
- 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.
Related papers
- C*: Unifying Programming and Verification in C [15.531046191957529]
C* is a proof-integrated language design for C programming.<n>It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code.<n>C* unifies implementation and proof code development by using C as the common language.
arXiv Detail & Related papers (2025-04-03T03:22:22Z) - Scaffolding Research Projects in Theory of Computing Courses [0.30458514384586394]
Theory of Computing (ToC) is an important course in CS curricula because of its connections to other CS courses as a foundation for them.
Recent work experimented with a new type of assignment, namely a mock conference'' project wherein students approach and present ToC problems as if they were submitting to a real'' CS conference.
arXiv Detail & Related papers (2024-10-02T16:20:27Z) - Designing Theory of Computing Backwards [0.30458514384586394]
Theory of computing (ToC) courses within undergraduate CS programs are often placed near the end of the program.
What is often intuitive for students about what a computer'' is--a Turing machine--is taught at the end of the course, which necessitates motivation for earlier models.
This poster contains our experiences in designing a ToC course that teaches the material effectively backwards''
arXiv Detail & Related papers (2023-11-13T23:32:41Z) - C-Procgen: Empowering Procgen with Controllable Contexts [62.84544720338002]
C-Procgen is an enhanced suite of environments on top of the Procgen benchmark.
It provides access to over 200 unique game contexts across 16 games.
arXiv Detail & Related papers (2023-11-13T13:07:48Z) - Hierarchical Programmatic Reinforcement Learning via Learning to Compose
Programs [58.94569213396991]
We propose a hierarchical programmatic reinforcement learning framework to produce program policies.
By learning to compose programs, our proposed framework can produce program policies that describe out-of-distributionally complex behaviors.
The experimental results in the Karel domain show that our proposed framework outperforms baselines.
arXiv Detail & Related papers (2023-01-30T14:50:46Z) - Flexible Correct-by-Construction Programming [2.8798933523190327]
We compare Correctness-by-Construction (CbC) with CbC-Block and TraitCbC.
CbC allows to develop software in a structured and incremental way to ensure correctness.
We provide for both approaches a programming guideline, which similar to CbC, leads to well-structured programs.
arXiv Detail & Related papers (2022-11-28T12:28:38Z) - Bayes risk CTC: Controllable CTC alignment in Sequence-to-Sequence tasks [63.189632935619535]
Bayes risk CTC (BRCTC) is proposed to enforce the desired characteristics of the predicted alignment.
By using BRCTC with another preference for early emissions, we obtain an improved performance-latency trade-off for online models.
arXiv Detail & Related papers (2022-10-14T03:55:36Z) - LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement
Learning [78.2286146954051]
LCRL implements model-free Reinforcement Learning (RL) algorithms over unknown Decision Processes (MDPs)
We present case studies to demonstrate the applicability, ease of use, scalability, and performance of LCRL.
arXiv Detail & Related papers (2022-09-21T13:21:00Z) - CLICKER: A Computational LInguistics Classification Scheme for
Educational Resources [47.48935730905393]
A classification scheme of a scientific subject gives an overview of its body of knowledge.
A comprehensive classification system like CCS or Mathematics Subject Classification (MSC) does not exist for Computational Linguistics (CL) and Natural Language Processing (NLP)
We propose a classification scheme -- CLICKER for CL/NLP based on the analysis of online lectures from 77 university courses on this subject.
arXiv Detail & Related papers (2021-12-16T02:40:43Z) - How could Neural Networks understand Programs? [67.4217527949013]
It is difficult to build a model to better understand programs, by either directly applying off-the-shelf NLP pre-training techniques to the source code, or adding features to the model by theshelf.
We propose a novel program semantics learning paradigm, that the model should learn from information composed of (1) the representations which align well with the fundamental operations in operational semantics, and (2) the information of environment transition.
arXiv Detail & Related papers (2021-05-10T12:21:42Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.