Verified Programs with Binders

Martin Clochard 1, 2 Claude Marché 1, 2 Andrei Paskevich 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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 metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-00913431
Contributor : Claude Marché <>
Submitted on : Tuesday, December 3, 2013 - 4:38:06 PM
Last modification on : Thursday, April 5, 2018 - 12:30:22 PM
Long-term archiving on : Monday, March 3, 2014 - 11:25:58 PM

File

plpv03-clochard.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00913431, version 1

Collections

Citation

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

Share

Metrics

Record views

863

Files downloads

407