[master] formally verified hash-consing

Hash-consing is a very useful technique for implementing certain kinds of algorithms, particularly in program analysis, logic, symbolic computation. Since it is very imperative, it is difficult to formalize in a purely functional setting. The goal of the internship is to apply new approaches to achieve this goal.

Various workarounds have been devised (see e.g. https://hal.archives-ouvertes.fr/ha...).

Recent additions to Coq (native integers, native arrays) are likely to make it feasible to formalize hash-consing natively and efficiently. The topic of the internship is to do achieve such formalization and apply it to useful sample use cases.

Contact | Site Map | Site powered by SPIP 3.2.19 + AHUNTSIC [CC License]

info visites 2086177