Loading...
Please wait, while we are loading the content...
Similar Documents
Verified programs with binders
| Content Provider | ACM Digital Library |
|---|---|
| Author | Paskevich, Andrei Clochard, Martin Marché, Claude |
| Abstract | Programs that treat datatypes with binders, such as theorem provers or higher-order compilers, are regularly used for mission-critical purposes, and must be both reliable and performant. Formally proving such programs using as much automation as possible is highly desirable. In this paper, we propose a generic approach to handle datatypes with binders both in the program and its specification in a way that facilitates automated reasoning about such datatypes and also leads to a reasonably efficient code. Our method is implemented in the Why3 environment for program verification. We validate it on the examples of a lambda-interpreter with several reduction strategies and a simple tableaux-based theorem prover. |
| Starting Page | 29 |
| Ending Page | 40 |
| Page Count | 12 |
| File Format | |
| ISBN | 9781450325677 |
| DOI | 10.1145/2541568.2541571 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2014-01-11 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Automated theorem proving Binders Formal verification Verified symbolic computations |
| Content Type | Text |
| Resource Type | Article |
