| Home |
| About |
| Submission Guidelines |
| Search |
| Download |
project summary
AVL Trees
| Title: | AVL Trees |
| Author: | Tobias Nipkow and Cornelia Pusch |
| Submission date: | 2004-03-19 |
| Abstract: | Two formalizations of AVL trees with room for extensions. The first formalization is monolithic and shorter, the second one in two stages, longer and a bit simpler. The final implementation is the same. If you are interested in developing this further, please contact gerwin.klein@nicta.com.au. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|