TWAM: A Certifying Abstract Machine for Logic Programs
TWAM: A Certifying Abstract Machine for Logic Programs
复制标题
TWAM：逻辑程序的验证抽象机
DOI：
10.1007/978-3-030-03592-1_7
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Karl Crary
中科院分区：
文献类型：
--
作者：
Rose Bohrer;Karl Crary
类型保存（或键入）汇编使用键入派生来证明汇编的正确性属性。我们已经为我们称为T-Prolog的Prolog的简单方言设计并实施了一个类型的编译器。我们方法的症结是一台新的认证抽象机器，我们称之为键入的沃伦抽象机（TWAM）。 TWAM具有足够强的依赖类型系统，可以在逻辑框架LF中指定逻辑程序的语义。我们提出了构成部分正确性保证的合理性元素：良好的程序实施了由其类型指定的逻辑程序。这种Metatheorem证明了我们从T-Prolog到Twam的认证编译器的设计和实施是合理的。
Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a type-preserving compiler for a simply-typed dialect of Prolog we call T-Prolog. The crux of our approach is a new certifying abstract machine which we call the Typed Warren Abstract Machine (TWAM). The TWAM has a dependent type system strong enough to specify the semantics of a logic program in the logical framework LF. We present a soundness metatheorem which constitutes a partial correctness guarantee: well-typed programs implement the logic program specified by their type. This metatheorem justifies our design and implementation of a certifying compiler from T-Prolog to TWAM.