Nondeterministic Manifest Contracts

We study a manifest contract system---a typed calculus of higher-order contracts where contracts are tightly integrated into a refinement type system---for a functional language with nondeterministic choice. The extension is not trivial, especially in the presence of dependent function types, because a naive extension would lead to inconsistent type equivalence, which makes contract information in refinement types meaningless.