weakmemory.github.io

Формальные методы дизайна и верификации программного обеспечения: семантики языков программирования

Задания для знакомых с Coq:

  1. Доказать существование отсортированной перестановки списка так, чтобы при экстракции получался Mergesort.
  2. Доказать полноту исчисления резолюций.

Задания для знакомых с Coq и семантиками:

  1. Реализовать операционную модель x86+FPGA из статьи Iorga-al:OOPSLA21.

По всем вопросам обращайтесь к Антону и Егору