This paper is concerned with the synthesis of invariants in programs with arrays. More specifically, we consider properties concerning array contents up to a permutation. For inst...
We propose a dependent type theory that integrates programming, specifications, and reasoning about higher-order concurrent programs with shared transactional memory. The design ...
Aleksandar Nanevski, Paul Govereau, Greg Morrisett
Type-and-effect systems are a natural approach for statically reasoning about a program’s execution. They have been used to track a variety of computational effects, for example...
Storing state in the client tier (in forms or cookies, for example) improves the efficiency of a web application, but it also renders the secrecy and integrity of stored data vul...
We present a possible world semantics for a call-by-value higherorder programming language with impredicative polymorphism, general references, and recursive types. The model is o...
Object-oriented programs are notable for making use of both rder abstractions and mutable, aliased state. Either feature alone is challenging for formal verification, and the com...
Neelakantan R. Krishnaswami, Jonathan Aldrich, Lar...
For many object-oriented systems, it is often useful to have a runtime architecture that shows networks of communicating objects. But it is hard to statically extract runtime obje...
The importance of distributed systems is growing as computing devices become ubiquitous and bandwidth becomes plentiful. Concurrency and distribution pose algorithmic and implemen...
Syntax Arthur Baars Doaitse Swierstra Technical Report UU-CS-2008-021 July 2008 Department of Information and Computing Sciences Utrecht University, Utrecht, The Netherlands www.cs...
Arthur I. Baars, S. Doaitse Swierstra, Marcos Vier...