Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over w...
Abstract. Coordination languages are often used to describe open ended systems. This makes it challenging to develop tools for guaranteeing security of the coordinated systems and ...
This paper presents the first type system for statically analyzing security protocols that are based on zero-knowledge proofs. We show how several properties offered by zero-knowl...
We propose a type system for lock-freedom in the -calculus, which guarantees that certain communications will eventually succeed. Distinguishing features of our type system are: it...
We introduce a type system providing a guarantee of client progress for a fragment of CaSPiS, a recently proposed process calculus for serviceoriented applications. The interplay o...
This paper introduces a new type system designed for safe systems programming. The type system features a new mutability model that combines unboxed types with a consistent typing ...
Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smi...
A new framework for higher-order program verification has been recently proposed, in which higher-order functional programs are modelled as higher-order recursion schemes and then ...
We present a new approach to the polymorphic typing of data accepting in-place modification in ML-like languages. This approach is based on restrictions over type generalization,...
Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accep...
Linear type systems permit programmers to deallocate or explicitly recycle memory, but they are severly restricted by the fact that they admit no aliasing. This paper describes a ...