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
CentraleSupélec (3, rue Joliot Curie,
Plateau de Moulon,
91192 GIF-SUR-YVETTE Cedex - France)
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.
Type de document :
Communication dans un congrès
Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ACM Press, 2014
https://hal.inria.fr/hal-00913431
Contributeur : Claude Marché <>
Soumis le : mardi 3 décembre 2013 - 16:38:06
Dernière modification le : jeudi 9 février 2017 - 16:01:30
Document(s) archivé(s) le : lundi 3 mars 2014 - 23:25:58
Martin Clochard, Claude Marché, Andrei Paskevich. Verified Programs with Binders. Programming Languages meets Program Verification, Jan 2014, San Diego, United States. ACM Press, 2014. <hal-00913431>
