Student Work
Formal Verification of Boolean Unification Algorithms with Coq
PubblicoContenuto scaricabile
open in viewerWe report on a verified implementation of two (well-known) algorithms for unification modulo the theory of Boolean rings: Lowenheim's method and the method of Successive Variable Elimination. The implementations and proofs of correctness were done in the Coq proof assistant; we view this contribution as an early step in a larger project of developing a suite of verified implementations of equational unification algorithms.
- This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.
- Creator
- Publisher
- Identifier
- E-project-042419-212433
- Advisor
- Year
- 2019
- Date created
- 2019-04-24
- Resource type
- Major
- Rights statement
Relazioni
- In Collection:
Articoli
Elementi
Thumbnail | Titolo | Visibilità | Embargo Release Date | Azioni |
---|---|---|---|---|
report_final.pdf | Pubblico | Scaricare | ||
coq_source.zip | Pubblico | Scaricare |
Permanent link to this page: https://digital.wpi.edu/show/wh246v71v