Type Safety via Hoare Logic with Separation and Pure Types

Wenhua Li, Darius Foo, Quang Trung Ta +1

Type safety has traditionally rested on carefully crafted type systems, under the motto "well-typed programs cannot go wrong". Modern demands push type systems past this basic guar…