Book

A reflection−based proof tactic for lattices in Coq

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.

Actions

Email

Email this record

Send the bibliographic details of this record to your email address.

Your Email
Please enter the email address that the record information will be sent to.

-
Your message (optional)
Please add any additional information to be included within the email.
Share
Cite

Cite this record

APA Style

James, D., & Hinze, R. (2009). A reflection−based proof tactic for lattices in Coq (Z. Horváth & V. Zsόk, Eds.; pp. 97–112).

MLA Style

James, D, and R Hinze. A Reflection−Based Proof Tactic for Lattices in Coq. Edited by Z Horváth and V Zsόk, 2009, pp. 97–112.

Chicago Style

James, D, and R Hinze. 2009. A Reflection−Based Proof Tactic for Lattices in Coq. Edited by Z Horváth and V Zsόk.
Print

Authors

+ James, D More by this author

Role:: Author

+ Hinze, R More by this author

Role:: Author

Contributors

Role:: Editor

Role:: Editor

Host title:: Post−symposium proceedings of the 10th Symposium on Trends in Functional Programming
Pages:: 97-112
Publication date:: 2009-06-01
ISBN:: 9781841504056

UUID:: uuid:0625d982-ebd1-4dd1-a9dc-a83802c68212
Local pid:: cs:4882
Deposit date:: 2015-03-31
ARK identifier:: ark:/29072/ora_0625d982ebd14dd1a9dca83802c68212

Terms of use

Copyright date:: 2009

Licence:: Terms and Conditions of Use for Oxford University Research Archive

Views and Downloads

About 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