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.