Abstract: Simple type systems perform compositional reasoning in that the type of a term depends only on the types of its subterms, and not on their semantics. Contracts offer more expressive abstractions, but static contract checking systems typically violate those abstractions and base their reasoning directly upon the semantics of terms. Pragmatically, this noncompositionality makes the decidability of static checking unpredictable.

We first show how compositional reasoning may be restored using standard type-theoretic techniques, namely existential types and subtyping. Despite its compositional nature, our type system is exact, in that the type of a term can completely capture its semantics, hence demonstrating that precision and compositionality are compatible. We then address predictability of static checking for contract types by giving a type-checking algorithm for an im- portant class of programs with contract predicates drawn from a decidable theory. Our algorithm relies crucially on the fact that the type of a term depends only the types of its subterms (which fall into the decidable theory) and not their semantics (which will not, in general).

Abstract: Writing and reasoning about concurrent programs remains notoriously dicult despite the proliferation of type systems, static analyses, and dynamic analyses targeting concurrent programs. There are examples of veried developments for concurrent languages and programs but most analyses - especially dynamic analyses - have not been subjected to mechanical rigor. We report on our partial mechanization in Coq of the recently released Velodrome dynamic atomicity checker.

Abstract: Classical first-order logic has the pleasant property that a formula can be reduced to an elegant implicative normal form through a series of syntactic simplifications. Using these transformations as a vehicle, this article demonstrates how to use Haskell’s type system, specifically a variation on Swierstra’s “Data Types à la Carte” method, to enforce the structural correctness property that these constructors are, in fact, eliminated by each stage of the transformation.

Abstract: General refinement types allow types to be refined by predicates written in a general-purpose programming language, and can express function preconditions and postconditions and data structure invariants. In this setting, with expressive and possibly verbose types, type reconstruction is particularly valuable, yet typeability is undecidable because it subsumes type checking. Using a generalized notion of type reconstruction, we present the first type reconstruction algorithm for a type system with base types refined by abitrary program terms. Our algorithm is a typeability-preserving transformation and defers type checking to a subsequent phase. The algorithm generates and solves a collection of implication constraints over refinement predicates, inferring maximally precise refinement predicates in a largely syntactic manner that is reminiscent of strongest postcondition calculation. Perhaps surprisingly, our notion of type reconstruction is decidable even though type checking is not.

Abstract: Software systems typically contain large APIs that are informally specified and hence easily misused. This paper presents the Sage programming language, which is designed to enforce precise interface specifications in a flexible manner. The Sage type system uses a synthesis of the type Dynamic, first-class types, and arbitrary refinement types. Since type checking for this expressive language is not statically decidable, Sage uses hybrid type checking, which extends static type checking with dynamic contract checking, automatic theorem proving, and a database of refuted subtype judgments.