该信息库包含ITP'21论文的扩展报告 经过验证的进度跟踪,可 作者:Matthias Brun,SáraDecova,Andrea Lattuada和Dmitriy Traytel。 该报告提供了安全特性的证明草图以及有关形式化的其他详细信息( rep.pdf )。 本文中描述的Isabelle形式化可以在“形式证明档案”中找到: