EN | DE
Theoretische Informatik

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

theses [2019/01/24 20:37]
tadeusz [Dr. Tadeusz Litak's proposals]
theses [2019/05/16 21:58] (current)
tadeusz [Dr. Tadeusz Litak In Kooperation mit Technische Hochschule N├╝rnberg]
Line 235: Line 235:
 === Rebasing from VST to Iris ======= === Rebasing from VST to Iris =======
  
-At present, the development of VeriGHC is done in the framework of [[http://vst.cs.princeton.edu/|VST]] by Appel et al. However, in principle nothing would prevent using another major, European framework of the [[https://iris-project.org/|Iris project]] (currently used, e.g., in the [[http://plv.mpi-sws.org/rustbelt/|RustBelt]] project. In general, the degree of portability between these two projects is an important challenge for the community, which has not been fully clarified yet. VeriGHC may provide an important case study.+At present, the development of VeriGHC is done in the framework of [[http://vst.cs.princeton.edu/|VST]] by Appel et al. However, in principle nothing would prevent using another major, European framework of the [[https://iris-project.org/|Iris project]]currently used, e.g., in the [[http://plv.mpi-sws.org/rustbelt/|RustBelt]] project. In general, the degree of portability between these two projects is an important challenge for the community, which has not been fully clarified yet. VeriGHC may provide an important case study.