TWAM: A Certifying Abstract Machine for Logic Programs
| Autor: | Karl Crary, Brandon Bohrer |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Soundness
Metatheorem Correctness Programming language Computer science 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Dependent type Warren Abstract Machine Abstract machine 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Compiler computer Logic programming |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030035914 VSTTE |
| DOI: | 10.1007/978-3-030-03592-1_7 |
| Popis: | Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a typed compiler for an idealized logic programming language 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 show programs obey a semantics based on provability in first-order logic (FOL). We present a soundness metatheorem which (going beyond the guarantees provided by most typed compilers) constitutes a partial behavior correctness guarantee: well-typed TWAM programs are sound proof search procedures with respect to a FOL signature. We argue why this guarantee is a natural choice for significant classes of logic programs. This metatheorem justifies our design and implementation of a certifying compiler from T-Prolog to TWAM. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|