We present System F°, an extension of System F that uses kinds to distinguish between
linear and unrestricted types, simplifying the use of linearity for general-purpose …

We develop a general method for proving properties of programs under arbitrary contexts–
including (but not limited to) observational equivalence, space improvement, and a form of …

This paper proposes a type-and-effect system called Teqt, which distinguishes terminating
terms and total functions from possibly diverging terms and partial functions, for a lambda …

Pointer analysis statically approximates the heap pointer structure during a program
execution in order to track heap objects or to establish alias relations between references …

To formally verify behavioral properties of programs, stating complex first-order formulas as
data invariants proves useful. In the context of pointer programs, such invariants are hard to …

Component software has many benefits, most notably increased software re-use; however,
the component software process places heavy burdens on programming language …

We study SlPCF⋆, namely a Turing-complete programming language inspired by a
semantic notion of linearity. SlPCF⋆ is based on a linear core of PCF and some operators …

This paper proposes a type-and-effect system called Teq↓, which distinguishes terminating
terms and total functions from possibly diverging terms and partial functions, for a lambda …

We develop a general method of proving properties of programs under arbitrary contexts—
including (but not limited to) observational equivalence, space improvement, and memory …

Restricting destructive update to values of a distinguished reference type prevents functions
from being polymorphic in the mutability of their arguments. This restriction makes it easier to …