Book icon

Book

A reflection−based proof tactic for lattices in Coq

Abstract:
This paper presents a new proof tactic that decides equalities and in­equalities between terms over lattices. It uses a decision procedure that is a variation on Whitman’s algorithm and is implemented using a technique known as proof by reflection. We will paint the essence of the approach in broad strokes and discuss the use of certified functional programs to aid the automation of formal reasoning.

Actions


Authors


Contributors

Role:
Editor
Pages:
97-112
Publication date:
2009-06-01
URN:
uuid:0625d982-ebd1-4dd1-a9dc-a83802c68212
Local pid:
cs:4882
ISBN:
9781841504056

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP