Skip to content

Latest commit

 

History

History
69 lines (52 loc) · 2.75 KB

README.md

File metadata and controls

69 lines (52 loc) · 2.75 KB

Examples of using the CakeML translator on functional programs based on the algorithms in "Purely Functional Data Structures" by Chris Okasaki (1996).

BankersQueueScript.sml: This is an example of applying the translator to the Bankers Queue algorithm from Chris Okasaki's book.

BatchedQueueScript.sml: This is an example of applying the translator to the Batched Queue algorithm from Chris Okasaki's book.

BinaryRandomAccessListsScript.sml: This is an example of applying the translator to the Binary Random Access Lists algorithm from Chris Okasaki's book.

BinomialHeapScript.sml: This is an example of applying the translator to the Binomial Heap algorithm from Chris Okasaki's book.

BottomUpMergeSortScript.sml: This is an example of applying the translator to the Bottom Up Merge Sort algorithm from Chris Okasaki's book.

HoodMelvilleQueueScript.sml: This is an example of applying the translator to the Hood Melville Queue algorithm from Chris Okasaki's book.

ImplicitQueueScript.sml: This is an example of applying the translator to the Implicit Queue algorithm from Chris Okasaki's book.

LazyPairingHeapScript.sml: This is an example of applying the translator to the Lazy Pairing Heap algorithm from Chris Okasaki's book.

LeftistHeapScript.sml: This is an example of applying the translator to the Leftist Heap algorithm from Chris Okasaki's book.

PairingHeapScript.sml: This is an example of applying the translator to the Pairing Heap algorithm from Chris Okasaki's book.

PhysicistsQueueScript.sml: This is an example of applying the translator to the Physicists Heap algorithm from Chris Okasaki's book.

RealTimeQueueScript.sml: This is an example of applying the translator to the Real-Time Heap algorithm from Chris Okasaki's book.

RedBlackSetScript.sml: This is an example of applying the translator to the Red-Black Set algorithm from Chris Okasaki's book.

SplayHeapScript.sml: This is an example of applying the translator to the Splay Heap algorithm from Chris Okasaki's book.

UnbalancedSetScript.sml: This is an example of applying the translator to the Unbalanced Set algorithm from Chris Okasaki's book.

benchmarkScript.sml: This file contains parts of the Splay Heap and Implicit Queue examples. This file has been used to generate benchmark programs.

okasaki_miscScript.sml: Lemmas used in Okasaki examples.