HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

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


Files produced by the author(s)


  • HAL Id : hal-00913431, version 1


Martin Clochard, Claude Marché, Andrei Paskevich. Verified Programs with Binders. Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ⟨hal-00913431⟩



Record views


Files downloads