[isabelle] 2 new AFP entries



Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
by Peter Gammie, Tony Hosking, and Kai Engelhardt

Abstract:
  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
  on x86-TSO.

  This development accompanies the PLDI 2015 paper of the same name.

http://afp.sf.net/entries/ConcurrentGC.shtml


Concurrent IMP
by Peter Gammie

Abstract:
  ConcurrentIMP extends the small imperative language IMP with control
  non-determinism and constructs for synchronous message passing.

http://afp.sf.net/entries/ConcurrentIMP.shtml


Enjoy!
Gerwin


________________________________

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 MHonArc.