Toward a Robust and Generalizable Metamaterial Foundation Model
Gachon University（嘉泉大学）；Korea Advanced Institute of Science and Technology（韩国科学技术院）；Seoul National University（首尔大学）
针对AI驱动超材料设计存在的任务专属重训练、OOD泛化差及正反设计需独立模型等问题，提出基于贝叶斯Transformer的超材料基础模型MetaFO，实现零样本预测与OOD下的逆向设计，拓展设计空间并推动范式转变。
2025-07-03 cs.AI cs.CE physics.optics
Threaded Code Generation with a Meta-Tracing JIT Compiler
语言实现框架，例如，RPython和Truffle/Graal是创建高效虚拟机的实用工具，包括功能良好的即时（JIT）编译器。在这样的框架中支持多层JIT编译对语言开发者来说是一个很高的要求。本文提出了一种通过重用现有的元跟踪JIT编译器来生成线程代码的思想，并给出了相应的解释器设计。我们的方法并没有对RPython本身进行很大的修改，而是构造了一个有效的解释器定义，从而在RPython中实现线程代码生成。我们希望我们的系统能够扩展到支持RPython框架中的多级JIT编译。我们通过在PyPy中模拟线程化代码生成的行为来测量其潜在性能。我们证实，与PyPy的JIT编译器相比，我们的方法平均将代码大小减少了80%，编译时间减少了60%，并且比仅解释器执行快了约7%。
2022-01-19 cs.PL
Metacognition in LLMs: Foundations, Progress, and Opportunities
Yale University（耶鲁大学）；University of California, Irvine（加利福尼亚大学欧文分校）
本文全面概述大语言模型元认知知识现状，分析分类该领域，总结技术进展，涵盖测量评估方法、引发改进应用技术等，还讨论相关应用、问题挑战及未来方向，为该主题研究提供综述与指引。
2026-07-14 cs.AI cs.CL
Solving the TTC 2011 Compiler Optimization Task with metatools
作者的“元工具”是一个泛型编程工具的集合。这包括从数学上建立良好的规范生成Java源代码，以及为XML编码文本创建严格类型化的文档对象模型。在这种背景下，几乎每一个计算机内部结构都被视为一个“模型”，每一次计算都是一种模型转换。这个概念与由专门的工具和语言执行的“经典模型转换”有很大的不同。因此，对于TTC 2011的组织者以及作者来说，将元工具应用于其中一个挑战，即“编译器优化任务”，似乎很有希望。这是一份关于由此产生的经验的报告。
2011-11-21 cs.PL cs.SE
InCoder-32B: Code Foundation Model for Industrial Scenarios
Beihang University（北京航空航天大学）；IQuest Research；Shanghai Jiao Tong University（上海交通大学）；ELLIS；University of Manchester（曼彻斯特大学）；Shanghai Artificial Intelligence Laboratory（上海人工智能实验室）；Langboat（朗博特）
本文提出InCoder-32B，首个统一芯片设计、GPU内核优化等工业领域的32B参数代码基础模型，通过高效架构和多阶段训练方法，在通用和工业任务中均取得优异性能。
2026-03-31 cs.AI cs.SE
Rethinking LLM-Based RTL Code Optimization Via Timing Logic Metamorphosis
school of Computer Science and Engineering（计算机科学与工程学院）
本文提出新的RTL优化评估基准和基于变形的方法，系统评估LLM在复杂时序逻辑RTL代码优化中的能力，发现LLM在逻辑运算上优于编译器方法，但在时序控制流和时钟域优化上仍存在不足。
2025-07-22 cs.AI cs.SE
Pyrosome: Verified Compilation for Modular Metatheory
Pyrosome 是一个 Coq 实现的模块化元理论框架，通过归纳等价保持实现可扩展的验证编译，支持特性扩展和编译器垂直组合，并展示了从 System F 到 CPS 及闭包转换的多遍编译案例。
2025-07-08 cs.PL
Visualizing The Intermediate Representation of Just-in-Time Compilers
即时（JIT）编译器被许多现代编程系统用来提高性能。JIT编译器中的错误提供了可利用的安全漏洞，并且由于它们庞大，复杂和动态，因此调试它们是困难的。目前的调试和可视化工具处理静态代码，并不适合在这个领域。我们描述了一种新的方法来简化大型和复杂的中间表示，生成的JIT编译器和可视化它与地铁地图的比喻，以帮助开发人员在调试。在Google的V8 JavaScript解释器和TurboFan JIT编译器上使用我们的原型实现的实验表明，它可以帮助识别和定位错误代码。
2021-06-09 cs.PL
Throughput Optimization as a Strategic Lever in Large-Scale AI Systems: Evidence from Dataloader and Memory Profiling Innovations
Amazon Robotics（亚马逊机器人）
本文通过数据加载器和内存优化创新，探讨吞吐量优化在大规模AI系统中的战略作用，分析架构改进、内存优化及编译器优化对训练效率的影响。
2026-03-27 cs.AI cs.LG cs.PF
Unlocking Tuning-Free Few-Shot Adaptability in Visual Foundation Models by Recycling Pre-Tuned LoRAs
Nanyang Technological University（南洋理工大学）；Tsinghua University（清华大学）；Sun Yat-sen University（中山大学）
本文提出 LoRA Recycle 框架，利用预调优 LoRA 逆向生成替代数据并蒸馏 meta-LoRA，使视觉基础模型无需调优即可单次前向完成少样本任务。
2024-12-03 cs.AI cs.CV cs.LG
Accurate Coverage Metrics for Compiler-Generated Debugging Information
针对优化程序调试信息不完整且现有覆盖率度量方法粗糙不可比的问题，提出可由工具计算的新度量标准，以激励语言实现提升调试质量。
2024-02-07 cs.PL cs.SE
Copy-and-Patch Compilation: A fast compilation algorithm for high-level languages and bytecode
当编译发生在运行时时，快速编译是很重要的，例如现代数据库系统中的查询编译器和现代浏览器中的WebAssembly虚拟机。我们提出了复制和补丁，一个非常快速的编译技术，也产生高质量的代码。它能够将高级语言和低级字节码程序降低到二进制代码，通过将来自二进制实现变体的大型库的代码拼接在一起。我们称这些二进制实现为stendable，因为它们有漏洞，在代码生成过程中必须插入缺失值。我们展示了如何构建一个模板库，并描述了复制和补丁算法，生成优化的二进制代码。我们演示了两个使用情况下的复制和补丁：一个编译器的高级C语言的元编程和WebAssembly的编译器。我们的高级语言编译器的编译成本可以忽略不计：它从AST生成代码所用的时间比构造AST所用的时间要少。我们已经实现了一个SQL数据库查询编译器上的元编程系统，并表明，在TPC-H数据库基准测试，复制和补丁生成的代码比LLVM -O 0快两个数量级，比更高的优化水平快三个数量级。生成的代码比解释快一个数量级，比LLVM -O 0快14%。我们的WebAssembly编译器生成代码的速度比Liftoff快4.9 - 6.5倍，Liftoff是Google Chrome中的WebAssembly基线编译器。生成的代码在Coremark和PolyBenchC WebAssembly基准测试中的性能也超过了Liftoff的39%-63%。
2021-09-15 cs.PL
RPyForth: Exposing a Call-Shared Data Stack to a Meta-Tracing JIT Compiler
Tokyo Metropolitan University（东京都立大学）；Heinrich-Heine-Universität Düsseldorf（杜塞尔多夫大学）
本文提出RPyForth，通过向元追踪JIT编译器暴露固定宽度窗口和共享溢出区，实现Forth数据栈的有效编译，无需静态栈效应分析，显著提升性能。
2026-09-22 cs.PL
Grokking the Sequent Calculus (Functional Pearl)
本文面向编译器黑客与编程语言爱好者，通过编写将小型表层语言转换为 λμμ-calculus 的编译器，首次以非逻辑学家的视角介绍了 sequent calculus 及其作为编译器中间语言的优势。
2024-06-20 cs.PL
Verified VCG and Verified Compiler for Dafny
ETH Zurich Switzerland；Chalmers University of Technology\ of Gothenburg Sweden；Institute for Infocomm Research (I 2 R), A STAR Singapore；Nanyang Technological University Singapore；ETH Zurich；Chalmers University of Technology\ of Gothenburg；Institute for Infocomm Research (I 2 R), A STAR；Nanyang Technological University
本文提出通过形式化方法验证Dafny语言的VCG和编译器，确保程序的正确性并生成可执行代码。
2025-12-04 cs.LO cs.PL
The CoCompiler: DSL Lifting via Relational Compilation
Galois, Inc.（Galois公司）
本研究提出CoCompiler双向工具，通过关系编译思路改写Vélus编译器，结合规范化处理，实现真实反应式C代码到Lustre DSL的提升，为复用现有编译器构建DSL提升器提供实用基础。
2025-10-28 cs.PL
OpenMP Meta-Lowering: A Declarative Approach to Performance Portable Parallel Code Generation
University of Bologna（博洛尼亚大学）
本文提出 OpenMP 元降级方法，利用 MLIR 和 DSL 将降级可编程化，在保持性能的同时减少代码量，实现跨目标的高效并行代码生成。
2026-10-05 cs.DC cs.PL
Row-Polymorphic Types for Strategic Rewriting
我们提出了一个类型系统的战略语言，表达程序转换重写规则的组合物。我们的行多态类型系统有助于编译器工程师编写正确的策略，静态拒绝重写，否则将在重写过程中失败的无意义的组合物在运行时。此外，我们的类型系统能够推理重写如何改变计算程序的形状。我们提出了一个形式化的语言在其类型系统，并展示了它的实际用途表示编译器优化策略。我们的类型系统为许多有趣的未来应用程序奠定了基础，包括验证程序转换的正确性和从编码为类型的规范合成程序转换。
2021-03-23 cs.PL
On the Implementation of GNU Prolog
University of Paris 1（巴黎第一大学）；Universidade de Évora（埃武拉大学）；CENTRIA FCT/UNL（新里斯本大学科学技术中心）；JFLI CNRS（法国国家科学研究中心日本-法国联合实验室）；University of Tokyo（东京大学）
GNU Prolog是Prolog语言的通用实现，它与大多数其他系统的区别在于，首先是一个本机代码编译器，它产生独立的可执行文件，不依赖于任何字节码仿真器或元解释器。其他突出的方面包括Prolog系统作为多遍编译器的显式组织，其中中间表示被物化，在Unix编译器传统中。GNU Prolog还包括一个可扩展的高性能有限域约束求解器，它与Prolog语言集成，但使用独立的低级机制实现。本文讨论了设计和实现GNU Prolog所涉及的主要问题：需求、系统组织、性能和可移植性问题，以及它相对于其他Prolog系统实现和ISO标准化倡议的地位。
2010-12-15 cs.AI cs.PL
Pydrofoil: accelerating Sail-based instruction set simulators
提出多阶段编译器Pydrofoil，结合AOT编译与基于PyPy的追踪JIT及领域特定优化，从Sail规范生成指令集模拟器，比Sail生成的C模拟器提速超230倍。
2025-03-06 cs.PL
Defunctionalization with Dependent Types
本文首次提出依赖类型语言的正式去函数化翻译，确立健全性与类型保持等元理论性质，适用于保持类型的编译器。
2023-04-10 cs.PL
Automated Code Optimization with E-Graphs
本文提出了一个先进的，通用的和高层次的代码重写和分析系统的Julia程序设计语言，提供应用的平等饱和存在的多重分派和元编程。我们展示了我们的系统如何实际解决一些具有挑战性的问题：程序员可以实现自己的高层次的编译器优化其特定领域的科学计划，而不要求他们在所有的编译器专家？这些优化器是否可以由用户在相同的语言和他们想要优化的相同程序中实现，从而解决两种语言的问题？这些编译器优化器是否可以以高级方式编写，如方程式，而无需担心重写顺序？因此，符号数学可以进行高级编译器优化，反之亦然吗？
2021-12-30 cs.PL cs.SC
Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens
Argot Collective；National Technical University of Athens（雅典国立技术大学）
该研究构建了Lean框架EquiVM，利用前沿LLM以代币为代价，为EVM上23个真实合约生成了可复现的基础精化机器证明，实现了此前技术未达的特性组合，重塑验证框架架构。
2026-10-21 cs.PL
Compiling Language Definitions: The ASF+SDF Compiler
ASF+SDF元环境是一个交互式语言开发环境，其主要应用领域是领域专用语言的定义、程序分析和转换工具的生成、软件更新工具的生成以及通用规范和原型。它使用条件重写规则来定义语言的动态语义和其他面向工具的方面，因此生成的工具的有效性严重依赖于重写规则实现的质量。ASF+SDF重写规则编译器生成C代码，从而利用C的可移植性和当前C编译器的复杂优化能力，并避免潜在的抽象机器接口瓶颈。它可以处理大型（10 000+规则）的语言定义，并使用一个有效的运行时存储方案能够处理大型（1 000 000+节点）的条款。术语存储使用最大子术语共享（hash-consing），这在ASF+SDF中比在Lisp或SML中更有效。广泛的基准测试表明，生成的代码的时间和空间性能与当前最好的重写规则和函数式语言编译器一样好，甚至更好。
2000-07-06 cs.PL cs.SE
Reinforcement Learning from Compiler and Language Server Feedback
Princeton University（普林斯顿大学）
本文提出RLCSF方法和Lanser-CLI工具，通过编译器和语言服务器的反馈信号提升编码代理的可靠性，利用确定性奖励函数和分析捆绑技术实现过程监督。
2026-05-01 cs.AI cs.CL cs.PL
A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
我们认为，功能性程序设计语言的编译器的实现和验证大大简化了采用高阶表示的语法称为高阶抽象语法或HOAS。HOAS的基本思想是使用一种元语言，它为绑定相关概念提供内置的逻辑处理。通过将元语言嵌入到更大的编程或推理框架中，可以将对象语言中的绑定结构的处理吸收到系统的元理论中，从而大大简化整体实现和推理过程。我们在这篇论文中提出并证明了上述论点的有效性的方法来验证执行的编译器转换的函数程序，利用HOAS。在这种方法中，函数程序的转换首先以基于规则的关系规范的形式表达。这些规范被渲染成语言lambda Prolog的程序。一方面，这些程序直接作为实现。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。lambda Prolog和Abella都支持使用HOAS方法。因此，它们构成了一个框架，可用于在验证编译中测试HOAS方法的好处。我们用它们来实现和验证一个编译器的代表性的功能程序设计语言，体现了许多编译器的核心，这些语言的转换。在这两个编程和推理阶段，我们展示了如何使用的HOAS方法显着简化了绑定结构的表示，操作，分析和推理。
2017-02-11 cs.LO cs.PL
Meta-Monomorphizing Specializations
Università degli Studi di Milano（米兰大学）
本文提出元多态化特殊化框架，通过编译时元编程重用多态化实现零成本特殊化，解决条件编译与静态分发的冲突问题，提升类型安全性和代码效率。
2026-04-13 cs.PL
COGENT: Certified Compilation for a Functional Systems Language
我们提出了一个自证明编译器的COGENT系统语言。COGENT是一种受限制的、多态的、高阶的、纯函数式的语言，具有线性类型，不需要可信的运行时或垃圾收集器。它编译成高效的C代码，旨在与现有的C函数互操作。该语言适用于具有最小共享的分层系统代码，例如文件系统或网络协议控制代码。对于类型良好的COGENT程序，编译器生成C代码，在Isabelle/HOL中对其语义进行高级浅嵌入，并证明C代码正确实现了此嵌入。其目的是让证明工程师能够高效地、均衡地推理真实世界系统代码的全部语义，同时保持C语言的互操作性和简洁性。我们描述了编译器的形式化验证阶段，其中包括自动化的形式化细化演算，从命令式更新语义到函数值语义的切换，以及一些标准的编译器阶段，如类型检查和单态化。编译器证书是一系列语言级的Meta证明和每个程序的翻译验证阶段，在Isabelle/HOL中组合成一个连贯的顶级定理。
2016-01-21 cs.LO cs.PL
Compiling Gradual Types with Evidence
University of Chile（智利大学）
本文提出GrEv编译器，基于证据实现高效渐进类型化，实验显示其性能优于基于转换的编译器。
2025-12-27 cs.PL
A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning
许多OO传统的程序设计语言现在都以某种形式支持模式匹配。历史上的例子包括Scala和Ceylon，以及最近增加的Java，Kotlin，TypeScript和Flow。但是，目前在这些语言中，泛型类层次结构上的模式匹配会导致令人费解的类型错误。然而，这种特性的组合在许多场景中会自然发生，比如在操作类型化的AST时。为了正确地支持它，编译器需要实现一种形式的子类型重构：重构在运行时在模式匹配期间未发现的子类型信息的能力。我们介绍cDOT，一个新的演算在家庭的依赖对象类型（DOT）打算作为一个正式的基础子类型重建。作为pDOT的后代，cDOT本身是Scala的正式基础，cDOT可用于编码高级面向对象功能，如泛型继承，类型构造函数变化，F有界多态性和第一类递归模块。我们证明了子类型重建包含GADT编码$λ_{2,Gμ}$，一个经典的基于约束的GADT演算，到cDOT。
2023-02-23 cs.PL
Systolic Computing on GPUs for Productive Performance
Intel（英特尔公司）；Peking University（北京大学）
我们提出了一种语言和编译器来高效地构建在GPU上运行的高性能{ \it软件脉动阵列}。基于严格的数学基础（均匀递归方程和时空变换），我们的语言具有很高的抽象水平，涵盖了广泛的应用。程序员{ \it}指定将并行计算投影到线性脉动阵列上，同时将投影的详细实现留给编译器;编译器实现指定的投影并将线性脉动阵列映射到GPU的SIMD执行单元和向量寄存器。通过这种方式，生产力和性能同时实现。这种方法巧妙地将循环转换、数据混洗和向量寄存器分配组合到一个框架中。同时，也可以应用许多其他优化;编译器将优化组合在一起以生成高效的代码。我们在英特尔GPU上实现了该方法。这是第一个允许在GPU上高效构建脉动阵列的系统。我们允许多个投影，任意投影方向和线性时间表，这可以表示大多数，如果不是全部，脉动阵列在实践中。在英特尔GEN9.5 GPU上进行的一维和二维卷积实验证明了该方法的通用性，以及其在表达各种脉动设计以找到最佳候选者方面的生产力。虽然我们的脉动阵列是在通用SIMD硬件上运行的纯软件，但与执行相同卷积的GPU专用硬件采样器相比，我们的一些最佳设计的速度高达59%。总的来说，这种方法有望在GPU上实现高效的高性能计算。
2020-10-29 cs.CL cs.PL
LoopTune: Optimizing Tensor Computations with Reinforcement Learning
Rice University（莱斯大学）；Meta AI；Dabun AI
针对传统编译器性能不足、自动调优耗时长等问题，提出深度强化学习编译器LoopTune，结合图表示与LoopNest代码生成器，可快速针对CPU优化张量计算，性能比肩手动调优库。
2023-11-08 cs.LG cs.PL
Dr Wenowdis: Specializing dynamic language C extensions using type information
本文提出 typed methods 技术，通过为 C 扩展函数附加向后兼容的类型元数据，显著降低动态语言运行时中 C 扩展调用的开销，并在 PyPy 中验证了其有效性。
2024-03-04 cs.PL
Galley: Modern Query Optimization for Sparse Tensor Programs
University of Washington（华盛顿大学）；Massachusetts Institute of Technology（麻省理工学院）
本研究提出声明式张量编程系统Galley，通过扩展FAQ框架分解程序、基于代价优化稀疏张量算子，在机器学习和子图计数任务中实现显著性能提升且优化开销极小。
2025-10-02 cs.DB cs.PL
The Design and Implementation of an Extensible System Meta-Programming Language
针对系统编程语言编译流水线封闭、难以元编程和扩展的问题，本文提出将程序定义作为脚本并通过元对象协议暴露完整编译流水线，且以 Sysmel 的自举自编译实现验证可行性。
2023-09-27 cs.PL cs.SE
Insum: Sparse GPU Kernels Simplified and Optimized with Indirect Einsums
Massachusetts Institute of Technology（麻省理工学院）；Georgia Institute of Technology（佐治亚理工学院）；NVIDIA（英伟达）
本文提出 Insum 编译器，将与格式无关的稀疏 Einsum 重写为间接 Einsum，并配合 GroupCOO、BlockGroupCOO 生成优化 GPU 代码，实现显著加速与代码量缩减。
2025-10-20 cs.PF cs.PL
Reflective Metagraph Rewriting as a Foundation for an AGI "Language of Thought"
MeTTa（Meta Type Talk）是一种新的程序设计语言，用于OpenCog Hyperon AGI系统。它被设计为一种元语言，具有非常基本和通用的设施，用于处理符号、接地、变量、类型、替换和模式匹配。原语的存在是为了创建新的类型系统和相关的DSL。非正式地说，MeTTa是Hyperon最低级的“思想语言”--学习更具体知识表示的算法将在其中操作的元语言，并且这些算法本身可以在其中表示。在这里，我们解释了如何将MeTTa语言形式化为元数据重写规则系统，这种方法自然适合Hyperon框架，因为后者的核心组件是分布式元数据知识存储（Atomspace）。构成MeTTa程序的元图重写规则也可以表示为元图，为MeTTa反射和自修改代码提供了自然模型。考虑到MeTTa程序计算其他MeTTa程序的执行轨迹之间的等价性，允许我们使用同伦类型论来建模MeTTa执行轨迹的空间。考虑到在MeTTa程序的执行轨迹之间映射的MeTTa程序的限制，我们发现，给定的MeTTa码基被有效地建模为无穷广群，并且所有MeTTa码基的空间被建模为（无穷，1）-topis。在离散物理学上下文中，该拓扑基本上与先前从关于超图的重写规则导出的所谓的“Ruliad”相同。作为元数据重写规则的MeTTA的形式化还可以提供有用的框架，用于在MeTTa解释器内构造用于模式匹配和等式推断的有效方法的实现。
2021-12-12 cs.PL
Lava: Foundations for Liquid Haskell via Translation to Rocq
IMDEA Software Institute（IMDEA软件研究所）；Inria（法国国家信息与自动化研究所）；Stevens Institute of Technology（史蒂文斯理工学院）
本文提出工具Lava，通过将Liquid Haskell转换为Rocq建立其形式化语义，明确了该语言计算与逻辑语义层面的差异，可作为所支持Liquid Haskell子集的证书检查器。
2026-10-14 cs.PL
Moebius: Metaprogramming using Contextual Types -- The stage where System F can pattern match on itself (Long Version)
我们描述的元编程语言，Moebius，它支持生成多态代码，更重要的是通过模式匹配多态代码的分析的基础。Moebius有两个主要成分：1）我们利用上下文模态类型来描述开放代码以及它有意义的上下文。在Moebius中，开放代码可以依赖于类型和术语变量（级别0），其值在稍后阶段提供，以及代码变量（级别1），代表在稍后阶段提供的代码模板。这就产生了一个多层次的模态演算，它支持System-F风格的多态性，并形成了多态代码生成的基础。2)我们扩展了多级模态模式演算以支持代码上的模式匹配。由于多态代码上的模式匹配可以细化多态类型变量，因此我们扩展了类型理论基础，以生成和跟踪出现的类型约束。我们还给出了一个操作语义并证明了类型保持性。我们的Moebius多层次模态基础为开放代码的生成和模式匹配提供了适当的抽象，而无需提交变量绑定和上下文的具体表示。因此，我们的工作是一个步骤，建立一个通用的类型理论的基础，多阶段的元编程，一方面，强制执行强类型保证，另一方面，使其易于生成和操作代码。这将使我们能够充分利用元编程的潜力，而不会牺牲我们正在生产和运行的代码的可靠性和信任。
2021-11-15 cs.PL
The Mathematical Foundations of Physical Systems Modeling Languages
用于一般物理系统的现代建模语言，例如Modelica、Amesim或Simscape，依赖于微分代数方程（DAE），即，形式f（dot{x}，x，u）=0的约束。这极大地促进了从物理学的第一原理建模和模型的重用。在本文中，我们开发的数学理论需要建立基于DAE的物理建模语言的编译器和工具的发展坚实的数学基础。与常微分方程不同，DAE表现出微妙的问题，因为微分指数和相关潜方程的概念- ODE是指数为零的DAE，不需要考虑潜方程。在生成执行代码和调用求解器之前，此类语言的编译需要一个重要的\emph{structural analysis}步骤，该步骤将微分索引降低到DAE求解器可接受的水平。Modelica类工具支持的模型涉及多个模式，这些模式具有基于模式依赖DAE的动态特性和状态依赖模式切换。多模式DAE比DAE困难得多。主要的困难是模式改变事件的处理。不幸的是，大量的文献致力于DAE的数学分析不包括多模情况下，通常没有说模式的变化。这种基础的缺乏给现有的建模工具带来了许多困难。有些模型处理得很好，有些则不然，两个类之间没有明确的界限。在本文中，我们开发了一个全面的数学方法支持编译和代码生成这类语言。其核心是多模DAE系统的结构分析。作为这种结构分析的副产品，我们提出了接受或拒绝模型的合理标准。对于我们的数学发展，我们依赖于非标准分析，这使我们能够铸造混合动力系统的动态离散时间动态与…
2021-01-19 cs.PL
Formal Metatheory of Second-Order Abstract Syntax
尽管在理论和实践方面都进行了广泛的研究，但形式化，推理和实现具有变量绑定的语言仍然是一项艰巨的工作-重复的样板文件和过于复杂的捕获避免替换元理论经常阻碍语言的实际有趣属性。现有的发展提供了一些缓解，但代价是不方便和容易出错的术语编码和缺乏正式的基础。我们提出了一个启发性的语言形式化框架中实现的Agda。该系统将具有变量绑定运算符的语法签名的描述转换为内部编码的归纳数据类型，该数据类型配备有语法操作，例如弱化和替换，以及它们的正确性属性。所生成的元理论进一步结合了元变量及其相关的元替换操作，这使得二阶方程/重写推理。该框架的基础数学基础-初始代数语义-通过构造将语言的组合解释导出到满足语义替换引理的模型中。
2022-01-10 cs.DM cs.LO cs.PL
