論文の概要: A Core Calculus for Type-safe Product Lines of C Programs

• arxiv url: http://arxiv.org/abs/2603.04013v1
• Date: Wed, 04 Mar 2026 12:51:23 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-05 21:29:15.308579
• Title: A Core Calculus for Type-safe Product Lines of C Programs
• Title（参考訳）: Cプログラムのタイプセーフな製品ラインのためのコア計算
• Authors: Ferruccio Damiani, Daisuke Kimura, Luca Paolini, Makoto Tatsuta,
• Abstract要約: 軽量 C (Lightweight C, LC) は、プリプロセッサディレクティブを使わずに、C の固有部分集合を形式化する電卓である。 カラーLC(CLC)にはCプリプロセッサディレクティブが付与されている。 我々は,CLCが提供する単純な形式化は,教育にも有用であると考えている。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 本稿では,(1)プリプロセッサディレクティブを使わずにANSI Cの固有部分集合を形式化するコア計算,(2)ANSI Cプリプロセッサディレクティブを付与したLCであるColored LC(CLC)を定義し,(3)Cプリプロセッサが生成するすべてのプログラムが十分に型付けされたCLCの型システムを定義する。 我々は,CLCが提供する単純な形式化は,教育にも有用であると考えている。 ステファノ・ベラルディはチューリン大学のコンピュータ科学科で学業の大半を過ごし、コンピュータ科学の論理的基礎と型ベースのプログラム分析に関する卓越した研究を行った。 長年にわたって、彼はBScのプログラミングコースからプログラム分析のPhDコースまで、多くのコースを教えてきた。 したがって,本論文はステファノ・ベラルディの研究・教育活動に完全に該当する。

関連論文リスト

• C*: Unifying Programming and Verification in C [15.531046191957529]
  C* は C プログラミングのための言語設計の証明である。 プログラマが実装コードと並行して証明コードブロックを埋め込むことで、リアルタイムの検証を可能にする。 C* は C を共通言語として使用することで実装と証明コード開発を統合する。
  論文  参考訳（メタデータ） (2025-04-03T03:22:22Z)
• Scaffolding Research Projects in Theory of Computing Courses [0.30458514384586394]
  The Theory of Computing (ToC) はCSカリキュラムにおいて重要なコースである。 最近の研究は、学生が実際のCSコンファレンスに応募しているかのようにToCの問題にアプローチし、提示するモック・カンファレンス・プロジェクトという、新しいタイプの課題を実験した。
  論文  参考訳（メタデータ） (2024-10-02T16:20:27Z)
• Designing Theory of Computing Backwards [0.30458514384586394]
  CSプログラムにおけるコンピュータ理論(ToC)コースは、しばしばプログラムの終わり近くに置かれる。 コンピュータが何をしているのかについて、学生にとって直感的であるもの - コースの終わりに教えられるチューリングマシン - は、初期のモデルのモチベーションを必要とする。 このポスターには、素材を効果的に後ろ向きに教えるToCコースの設計の経験が含まれています。」
  論文  参考訳（メタデータ） (2023-11-13T23:32:41Z)
• C-Procgen: Empowering Procgen with Controllable Contexts [62.84544720338002]
  C-Procgenは、Procgenベンチマーク上に拡張された環境スイートである。 16のゲームで200以上のユニークなゲームコンテキストにアクセスすることができる。
  論文  参考訳（メタデータ） (2023-11-13T13:07:48Z)
• Hierarchical Programmatic Reinforcement Learning via Learning to Compose Programs [58.94569213396991]
  プログラムポリシーを作成するための階層型プログラム強化学習フレームワークを提案する。 提案するフレームワークは,プログラム作成の学習を通じて,アウト・オブ・ディストリビュータの複雑な動作を記述するプログラムポリシーを作成することができる。 Karel ドメインの実験結果から,提案するフレームワークがベースラインより優れていることが示された。
  論文  参考訳（メタデータ） (2023-01-30T14:50:46Z)
• Flexible Correct-by-Construction Programming [2.8798933523190327]
  CbC と CbC-Block と TraitCbC を比較した。 CbCは、ソフトウェアを構造化されたインクリメンタルな方法で開発することで、正確性を保証する。 我々は、CbCと同様のプログラミングガイドラインを両方のアプローチで提供し、十分に構造化されたプログラムへと導く。
  論文  参考訳（メタデータ） (2022-11-28T12:28:38Z)
• Bayes risk CTC: Controllable CTC alignment in Sequence-to-Sequence tasks [63.189632935619535]
  予測アライメントの望ましい特性を強制するためにベイズリスクCTC(BRCTC)を提案する。 BRCTCを他の早期排出の選好と組み合わせることで、オンラインモデルの性能・遅延トレードオフが改善される。
  論文  参考訳（メタデータ） (2022-10-14T03:55:36Z)
• LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning [78.2286146954051]
  LCRLは未知決定プロセス(MDP)上でのモデルフリー強化学習(RL)アルゴリズムを実装している 本稿では,LCRLの適用性,使いやすさ,拡張性,性能を示すケーススタディを提案する。
  論文  参考訳（メタデータ） (2022-09-21T13:21:00Z)
• CLICKER: A Computational LInguistics Classification Scheme for Educational Resources [47.48935730905393]
  科学的主題の分類スキームは、その知識の体系の概要を与える。 計算言語学(CL)と自然言語処理(NLP)には、CCSや数学科目分類(MSC)のような包括的分類体系は存在しない。 そこで本研究では,77の大学におけるオンライン講義の分析に基づいて,CL/NLPのCLICKERを分類する手法を提案する。
  論文  参考訳（メタデータ） (2021-12-16T02:40:43Z)
• How could Neural Networks understand Programs? [67.4217527949013]
  ソースコードにnlpプリトレーニング技術を直接適用するか、あるいはtheshelfによってモデルに機能を追加するかで、プログラムをより理解するためのモデルを構築するのは難しい。 本研究では,(1)操作セマンティクスの基本操作とよく一致する表現と(2)環境遷移の情報からなる情報から,モデルが学ぶべき新しいプログラムセマンティクス学習パラダイムを提案する。
  論文  参考訳（メタデータ） (2021-05-10T12:21:42Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。