- Laowai Guide
Formal Techniques for Java-like Programs (FTfJP)
- Wei-Ngan Chin (co-Chair and primary contact), National U Singapore
- Aquinas Hobor (co-Chair), National U Singapore
- Sophia Drossopoulou, Imperial College, UK
- Susan Eisenbach, Imperial College, UK
- Gary T. Leavens, U Central Florida, USA
- Peter Müller, ETH Zürich, Switzerland
- Arnd Poetzsch-Heffter, U Kaiserslautern, Germany
- Erik Poll, Radboud U Nijmegen, The Netherlands
Formal techniques can help analyze programs, precisely describe program be- havior, and verify program properties. Newer languages such as Java, C# and Scala provide good platforms to bridge the gap between formal techniques and practical program development, because of their reasonably clear semantics and standardised libraries. Moreover, these languages are interesting targets for formal techniques, because the novel paradigm for program deployment introduced with Java, with its improved portability and mobility, opens up new possibilities for abuse and causes concern about security.
Work on formal techniques and tools for programs and work on the formal underpinnings of programming languages themselves naturally complement each other. This workshop aims to bring together people working in both these fields, on topics such as:
- formal techniques for object-oriented languages
- specification techniques and interface specification languages
- specification of software components and library packages
- automated checking and verification of program properties
- verification logics
- language semantics
- type systems
- dynamic linking and loading
|Tuesday, 12 June|
|10:00–11:00||Invited Tutorial: Tom Van Cutsem - AmbientTalk: Modern Actors for Modern Networks - (slides)|
Corecursive Featherweight Java
Encoding Featherweight Java with Assignment and Immutability using The Coq Proof Assistant
|13:30–14:30||Keynote: Jens Palsberg - Featherweight X10: a core calculus for async-finish parallelism|
A type system for regular expressions
Verifying the reflective visitor pattern
Verifying Backwards Compatibility of Object-Oriented Libraries Using Boogie
Verification Games: Making Verification Fun!
AmbientTalk: Modern Actors for Modern Networks
Tom Van Cutsem
We introduce AmbientTalk, a dynamic, object-oriented, distributed programming language.AmbientTalk focuses primarily on the domain of mobile peer-to-peer applications, which are becoming more and more widespread in the wake of smartphone platforms such as iOS and Android. AmbientTalk runs on Android, and can be thought of as a scripting language for that platform. We will discuss AmbientTalk~Rs roots and devote special attention to its concurrent and distributed language features, which are founded on the actor model. Next, we will showcase the language by explaining a peer-to-peer application. We show how resilient mobile applications can be constructed with familiar building blocks like objects and messages, but also in what way these building blocks have to be adapted to fit the characteristics of mobile networks.
Featherweight X10: a core calculus for async-finish parallelism
We present a core calculus with two of X10's key constructs for parallelism, namely async and finish. Our calculus forms a convenient basis for type systems and static analyses for languages with async-finish parallelism. For example, we present a type system for context-sensitive may-happen-in-parallel analysis, along with experimental results of performing type inference on 13,000 lines of X10 code. Our analysis runs in polynomial time and produces a low number of false positives, which suggests that our analysis is a good basis for other analyses such as race detectors. Our calculus is also a good basis for tractable proofs of correctness. For example, we give a one-page proof of the deadlock-freedom theorem of Saraswat and Jagadeesan, and we prove the correctness of our type system.
Jens Palsberg is Professor and Chair of Computer Science at the University of California, Los Angeles. He is the editor-in-chief of ACM Transactions of Programming Languages and Systems and a member of the editorial board of Information and Computation.