[isabelle] New AFP article: Jinja With Threads

We are pleased to announce that a new article has made it into the Archive of Formal Proofs:

Jinja With Threads
Andreas Lochbihler

We extend the Jinja source code semantics by Klein and Nipkow with Java-style arrays and threads. Concurrency is captured in a generic framework semantics for adding concurrency to a sequential semantics, which features dynamic thread creation, inter-thread communication via shared memory and lock synchronisation. Also, threads can suspend themselves and be notified by others. We instantiate the framework with the adapted Jinja source code semantics and show type safety for the multithreaded case. For explanations see the FOOL 2008 paper by A. Lochbihler.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.