| Home |
| About |
| Submission Guidelines |
| Search |
| Download |
project summary
Jinja with Threads
| Title: | Jinja with Threads |
| Author: | Andreas Lochbihler |
| Submission date: | 2007-12-03 |
| Abstract: | 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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|