Induction in Proofs about Programs
Four methods for proving equivalence of programs by induction are described and compared. They are recursion induction, structural induction, mu-rule induction, and truncation induction. McCarthy's formalism for conditional expressions as function definitions is used and reinterpreted in view...
| Main Author: | |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149405 |
| _version_ | 1811091762560630784 |
|---|---|
| author | Greif, Irene Gloria |
| author_facet | Greif, Irene Gloria |
| author_sort | Greif, Irene Gloria |
| collection | MIT |
| description | Four methods for proving equivalence of programs by induction are described and compared. They are recursion induction, structural induction, mu-rule induction, and truncation induction. McCarthy's formalism for conditional expressions as function definitions is used and reinterpreted in view of Park's work on results on results in lattice theory as related to proofs about programs. The possible application of this work to automatic program verification is commented upon. |
| first_indexed | 2024-09-23T15:07:30Z |
| id | mit-1721.1/149405 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T15:07:30Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1494052023-03-30T03:17:50Z Induction in Proofs about Programs Greif, Irene Gloria Four methods for proving equivalence of programs by induction are described and compared. They are recursion induction, structural induction, mu-rule induction, and truncation induction. McCarthy's formalism for conditional expressions as function definitions is used and reinterpreted in view of Park's work on results on results in lattice theory as related to proofs about programs. The possible application of this work to automatic program verification is commented upon. 2023-03-29T14:55:48Z 2023-03-29T14:55:48Z 1972-02 https://hdl.handle.net/1721.1/149405 02527977 MIT-LCS-TR-093 MAC-TR-093 application/pdf |
| spellingShingle | Greif, Irene Gloria Induction in Proofs about Programs |
| title | Induction in Proofs about Programs |
| title_full | Induction in Proofs about Programs |
| title_fullStr | Induction in Proofs about Programs |
| title_full_unstemmed | Induction in Proofs about Programs |
| title_short | Induction in Proofs about Programs |
| title_sort | induction in proofs about programs |
| url | https://hdl.handle.net/1721.1/149405 |
| work_keys_str_mv | AT greifirenegloria inductioninproofsaboutprograms |