These are the proceedings of the 16th Workshop on Formal Techniques for Java-like Programs (FTfJP 2014) held together with ECOOP 2014 in Uppsala, Sweden.
Proceeding Downloads
How to prove type soundness of Java-like languages without forgoing big-step semantics
Small-step operational semantics is the most commonly employed formalism for proving type soundness of statically typed programming languages, because of its ability to distinguish stuck from non-terminating computations, as opposed to big-step ...
Constraint Semantics for Abstract Read Permissions
The concept of controlling access to mutable shared data via permissions is at the heart of permission logics such as separation logic and implicit dynamic frames, and is also used in type systems, for instance, to give a semantics to "read-only" ...
Tinygrace: A Simple, Safe, and Structurally Typed Language
Grace is a new gradually, structurally typed object-oriented programming language. Formal models of existing languages provide a rigorous base for claiming type soundness, so we have set about creating a model of a subset of Grace. While much of the ...
Verifying Functional Behaviour of Concurrent Programs
Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying ...
Rationally Reconstructing the Escrow Example
The Escrow Exchange Contract has been used as a case study of building up complex and trustworthy systems from basic object capabilities, in the context of concurrent and distributed programming. In this short paper we present a Rational Reconstruction ...
Index Terms
Proceedings of 16th Workshop on Formal Techniques for Java-like Programs