- This paper presents a new proof tactic that decides equalities and inequalities 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.
- Publication date:
- Local pid:
- Copyright date:
A reflection−based proof tactic for lattices in Coq
Views and Downloads
If you are the owner of this record, you can report an update to it here: Report update to this record