search

delcypher / freeboogie

Automatically exported from code.google.com/p/freeboogie
0 stars 1 forks source link

type encoding #39

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
Withe the Boogie 2 type system it is not safe to erase types. Instead they
need to be encoded, as explained here:
  http://research.microsoft.com/en-us/um/people/leino/papers/krml186.pdf

Original issue reported on code.google.com by radugrig...@gmail.com on 26 Aug 2009 at 4:13