Lean reimplementation of PEDANTIC
This is an unfinished work. It is a reimplementation of PEDANTIC. For more information, check out www.cs.jhu.edu/~roe.
Files:
PEDANTIC2.lean - header to include all files of separation logic framework
traversal.lean - tree traversal example
Source files of framework:
absState.lean
impHeap.lean
absExecute.lean
Random testing:
test.lean