Spy game: verifying a local generic solver in Iris

Paulo Emílio de Vilhena, François Pottier, Jacques-Henri Jourdan. Spy game: verifying a local generic solver in Iris. Proceedings of the ACM on Programming Languages, 4(POPL), 2020. [doi]

Abstract

Abstract is missing.