Manifest Contracts with Intersection Types

Yuki Nishida, Atsushi Igarashi

We present a manifest contract system PCFv$\Delta$H with intersection types. A manifest contract system is a typed functional calculus in which software contracts are integrated into a…