Preliminary data-cost examples
allProgScript.sml: A data-cost example of a list sum function using fold
allProofScript.sml: Prove of sum space consumption
costLib.sml: Tactics and utilities for data-cost proofs
costPropsScript.sml:
Proofs about size_of and size_of_heap
cyesProgScript.sml: A data-cost example of a non-terminating function (cyes) that prints a character indefinitely
cyesProofScript.sml: Prove that cyes never exits prematurely.
lcgLoopProgScript.sml: A data-cost example of a non-terminating function that generates entries of a Linear Congruential Generator (LCG) indefinitely.
lcgLoopProofScript.sml: Prove that lcgLoop never exits prematurely.
miniBasisProgScript.sml: Explicit construction of mini-basis, to support CF reasoning.
pureLoopProgScript.sml: A data-cost example of a non-terminating function (pureLoop)
pureLoopProofScript.sml: Prove that pureLoop never exits prematurely.
reverseProgScript.sml: A data-cost example of a reverse
reverseProofScript.sml: A data-cost example of a reverse (proofs)
size_ofPropsScript.sml: Lemmas about size_of
sumProgScript.sml: A data-cost example of a list sum function using fold
sumProofScript.sml: Prove of sum space consumption
yesProgScript.sml: A data-cost example of a non-terminating function (cyes) that prints a character indefinitely
yesProofScript.sml: Prove that yes never exits prematurely.
yes_ffi.c: Implements the foreign function interface (FFI) used in the yes program, as a thin wrapper around the relevant system calls.