Proving the Correctness of Fractional Permissions for a Java-like Kernel Language
John Boyland and Chao Sun
Abstract
We announce mechanical proofs of soundness for a type system using
fractional permissions with nesting for single-threaded programs in a kernel language,
and for a simple non-null system that piggy-backs on the first system. The proofs are all done using Twelf.
The (concurrent) kernel language and fractional permission system are pre-existing.
We describe the type system linking these two, and the purpose in building one type system on top of another.
Along the way, we describe our experiences using Twelf.
Presented at FOOL 2011; Sunday, 23 October 2011;
Portland, Oregon, USA