[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 | Plan du site | Site réalisé avec SPIP 3.1.15 + AHUNTSIC [CC License]

info visites 1803430