List.sort done in in-place array sort - #1349

Open

talsewell wants to merge 39 commits into

CakeML:masterfrom

talsewell:array-heap-sort-cleanup

Commits on Apr 11, 2026

monadic translator: More type-variable handling
talsewell
committed
500af34
monadic translator: less dependent on const naming
talsewell
committed
c4b6ccd
monadic translator: polymorphism debug and bugfix
talsewell
committed
517a77d
Add a pure model of heap-sort-in-array (#979)
talsewell
committed
5630e67
Convert heap-sort to monad, but fail to translate
talsewell
committed
25504e2
Heap sort via array apparently translating
talsewell
committed
bcd2491
Alternative heap-sort approach, mostly verified
talsewell
committed
0487b97
Verify and translate monadic versions
talsewell
committed
e5ce0a5
Clean up experiments and previous versions
talsewell
committed
7d33006
Try predicative/hoare monadic sort verification
talsewell
committed
c2367ba
Some parts proven via mini-sep-logic
talsewell
committed
0ee3c38
A better proof
talsewell
committed
269e4eb
Reduce to the better proof
talsewell
committed
aed3ba8
Prove remaining cheats
talsewell
committed
0d29e0c
Start cleaning up "pure" part
talsewell
committed
20ecc34
Move monadic defs and equiv to basis/monadic
talsewell
committed
9228966
Connect heap-list-sort into ListProg
talsewell
committed
92e1535
list sort: use a more sensible variable type
talsewell
committed
ed1e54d
list sort: flip translation/definition of sort
talsewell
committed
3e1e5e6
Add basis/monadic to build-sequence
talsewell
committed
3babd6f
monad translator: fix up store_inv confusion
talsewell
committed
58c9669
mllist: use heap-list-sort
talsewell
committed
56b5b71
Rename Triviality->Theorem[local]
talsewell
committed
d5f75a5
heap-list-sort: adjust translation steps
talsewell
committed
b5feea5
cleanup: remove previous version
talsewell
committed
c36ecf9
sort: derive sort [x] = [x] a different way
talsewell
committed
bf242a1
heap-list-sort: make CV-friendly definitions
talsewell
committed
dfc3329
Commit README.md update in basis
talsewell
committed
97e313f
candle: use the previous mergesort
talsewell
committed
5343be7
candle: same sort change in "overloading"
talsewell
committed
8651497
run-finding merge-sort verification
talsewell
committed
9aec59e
monadic (array) variant of sort and equiv proof
talsewell
committed
d141430
merge_run sort: post-facto translation
talsewell
committed
f61480a
heap_list_sort: matching translation file
talsewell
committed
88e8ec1
array-sorts: move to translator/monadic/examples
talsewell
committed
8def96b
also detach heap_list_sort from ListProg
talsewell
committed
b356076
Add readme/README files to new dir
talsewell
committed
fa65476

Commits on Apr 14, 2026

Also add Holmakefile
talsewell
committed
f35d3bc

Commits on Apr 15, 2026

Also add to build-sequence
talsewell
committed
9fc401d