Executing
Formal Specifications by Translation to Higher Order Logic Programming
presented
by Jamie Andrews
| |
Executing
Formal Specifications by Translation to Higher Order Logic Programming
presented
by Jamie Andrews
|
| formalWARE
project
formalWARE
formalWARE
|
Presented by James H. Andrews
at the 1997 International Conference
on Theorem Proving in Higher
Order Logics,
Bell Labs, Murray Hill, 19-22
August 1997.
We describe the construction and use of a system for translating higher order logic-based specifications into programs in the higher order logic programming language Lambda Prolog. The translation improves on previous work in the field of executing specifications by allowing formulas with quantifiers to be executed, and by permitting users to pose Prolog-style queries with free variables to be instantiated by the system. We also discuss various alternative target languages and design decisions in emplementing the translator. Presentation Slides (Thumbnails) Presentation Slides (PDF) Presented at the 1997 International Conference
on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, 19-22
August 1997.
. |
