| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Verified Programs with Binders
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 \Why 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.
Cited literature [26 references]
https://hal.inria.fr/hal-00913431
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Tuesday, December 3, 2013 - 4:38:06 PM
Last modification on : Thursday, July 8, 2021 - 3:48:45 AM
Long-term archiving on: : Monday, March 3, 2014 - 11:25:58 PM
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Tuesday, December 3, 2013 - 4:38:06 PM
Last modification on : Thursday, July 8, 2021 - 3:48:45 AM
Long-term archiving on: : Monday, March 3, 2014 - 11:25:58 PM
File
plpv03-clochard.pdf
Files produced by the author(s)