Thomas Sewell
Thomas Sewell
The SharingTables structure is used to compress the terms and types that appear in a theory's signature. The compression ensures that repeated terms and types are only stored once. This...
Something I thought of a while ago. HOL4 error messages tend to be very terse, for instance, if MATCH_MP fails, you might get an error message like "different constructors" with...
I'm experimenting with adjusting a Z3-based tool to produce bitvector encodings of its problems rather than integer encodings. This is producing surprising performance regressions. The tool I'm working on is...
The original implementation of toSortedAList was overcomplicated, using auxiliary run-length-encoding functions to carry across the idea of the algorithm from one that works on a dense structure. After a couple...
I'm hoping to start a discussion about a possible feature, motivated by CakeML build times. In some Holmake runs, a large fraction of the CPU time is spent loading. I...
It happens that pancake doesn't support `if ( ) { } else if ( ) { } else { }`, that is, the `else if` pair is not supported and...
Spotted while poking around in the l4v repository. If a thread attempts to receive on a notification object, and the notification object is bound to a different thread, this fails....
It's common to want the top-level translated functions to not have pre-conditions or side-conditions. The CakeML development indirectly requires this with the top-level CF theorems stated about the final toplevel...