search

septract / starling-tool

An automatic verifier for concurrent algorithms.
MIT License
7 stars 4 forks source link

Type system rewrite? #70

Open MattWindsor91 opened 8 years ago

MattWindsor91 commented 8 years ago

The current Starling type system, which insists on expressions being partitioned into strongly typed classes of sub-expression, may become very unwieldy as we add n-ary arrays. We need to consider whether we need to make Starling's type system less internally strong (so it allows badly typed expressions in the middle of the Starling proof process, and type-checks them on-demand when it needs to know the type of them).

MattWindsor91 commented 8 years ago

This seems to have been staved off for now with the current array encoding, as shonky as it is. Kicking into the long grass for now.

MattWindsor91 commented 7 years ago

Reopening because of talk between myself and @BenSimner about this.