显性审计
Explicit Auditing
摘要：
审计单位演算（英语：Calculus of Audited Units，CAU）是一种类型化的λ演算，源自于在Curry-Howard同构下对Artemov的证明逻辑的计算解释;它通过提供审计类型来扩展简单类型化的λ演算，这些审计类型由携带其过去计算历史的表达式占据。与大多数其他审计技术不同，CAU允许在运行时检查踪迹作为一流的操作，并应用于科学计算的安全性、调试和透明度。CAU的有效实现是具有挑战性的：不仅轨迹的大小快速增长，而且在每次beta缩减后都需要对其进行归一化。在本文中，我们研究了如何减少条款更有效地在无类型的变体CAU通过显式替换和显式审计操作，最后得出一个按值调用抽象机。
英文摘要：
The Calculus of Audited Units (CAU) is a typed lambda calculus resulting from a computational interpretation of Artemov's Justification Logic under the Curry-Howard isomorphism; it extends the simply typed lambda calculus by providing audited types, inhabited by expressions carrying a trail of their past computation history. Unlike most other auditing techniques, CAU allows the inspection of trails at runtime as a first-class operation, with applications in security, debugging, and transparency of scientific computation. An efficient implementation of CAU is challenging: not only do the sizes of trails grow rapidly, but they also need to be normalized after every beta reduction. In this paper, we study how to reduce terms more efficiently in an untyped variant of CAU by means of explicit substitutions and explicit auditing operations, finally deriving a call-by-value abstract machine.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
