Yuki Nishida

Nondeterministic Manifest Contracts

2018

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 …

Law and Order for Typestate with Borrowing

2024 · arXiv (Cornell University)

Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for …