[isabelle] 2 new AFP entries
- To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] 2 new AFP entries
- From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
- Date: Thu, 16 Apr 2015 08:31:34 +0000
- Accept-language: en-AU, en-US
- Thread-index: AQHQeB+/zgcffenA6EeAvijVtqDfbA==
- Thread-topic: 2 new AFP entries
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
by Peter Gammie, Tony Hosking, and Kai Engelhardt
We use ConcurrentIMP to model Schism, a state-of-the-art real-time
garbage collection scheme for weak memory, and show that it is safe
This development accompanies the PLDI 2015 paper of the same name.
by Peter Gammie
ConcurrentIMP extends the small imperative language IMP with control
non-determinism and constructs for synchronous message passing.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and