A reflection−based proof tactic for lattices in Coq
Daniel W.H. James and Ralf Hinze
Abstract
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.
Details
| Book Title |
Post−symposium proceedings of the 10th Symposium on Trends in Functional Programming |
| Chapter |
7 |
| Editor |
Horváth‚ Zoltán and Zsόk‚ Viktόria |
| ISBN |
9781841504056 |
| Location |
Komárno‚ Slovakia |
| Month |
June |
| Note | |
| Pages |
97–112 |
| Publisher |
Intellect |
| Series |
TFP'09 |
| Year |
2009 |
Links
Related pages
|
People |