论文标题
用于分类网络的算法的形式化
A Formalisation of Algorithms for Sorting Network
论文作者
论文摘要
该注释说明了如何使用SSSREFLECT扩展名在COQ证明助手中对构建排序网络进行形式化并正确证明的标准算法如何正确。
This notes explains how standard algorithms that construct sorting networks have been formalised and proved correct in the Coq proof assistant using the SSReflect extension.
