sf.tar
所属分类：matlab编程
开发工具：Others
文件大小：611KB
下载次数：5
上传日期：2011-01-25 20:26:53
上 传 者：
wangyongzhao
说明： 携带证明的代码的例子,在安装coq之后可以直接运行的,入门级别的
(Examples of proof carrying code, directly after the installation to run coq, entry-level)
文件列表:
sf (0, 2010-05-03)
sf\Basics.v (51037, 2010-05-03)
sf\Equiv.v (42694, 2010-05-03)
sf\Hoare.v (52033, 2010-05-03)
sf\html (0, 2010-05-03)
sf\html\Basics.html (165172, 2010-05-03)
sf\html\coqdoc.css (5854, 2010-05-03)
sf\html\coqindex.html (407588, 2010-05-03)
sf\html\Equiv.html (223658, 2010-05-03)
sf\html\Hoare.html (235013, 2010-05-03)
sf\html\Imp.html (227931, 2010-05-03)
sf\html\ImpParser.html (77961, 2010-05-03)
sf\html\Ind.html (251079, 2010-05-03)
sf\html\index.html (1237, 2010-05-03)
sf\html\Lists.html (140628, 2010-05-03)
sf\html\Logic.html (161549, 2010-05-03)
sf\html\MoreHoare.html (261799, 2010-05-03)
sf\html\MoreStlc.html (155374, 2010-05-03)
sf\html\Poly.html (207787, 2010-05-03)
sf\html\Preface.html (10600, 2010-05-03)
sf\html\Records.html (476616, 2010-05-03)
sf\html\References.html (295489, 2010-05-03)
sf\html\Rel.html (50284, 2010-05-03)
sf\html\SfLib.html (27943, 2010-05-03)
sf\html\Smallstep.html (245666, 2010-05-03)
sf\html\Stlc.html (216433, 2010-05-03)
sf\html\Subtyping.html (162419, 2010-05-03)
sf\html\Template.html (14461, 2010-05-03)
sf\html\toc.html (20753, 2010-05-03)
sf\Imp.v (53784, 2010-05-03)
sf\ImpParser.v (14129, 2010-05-03)
sf\Ind.v (71761, 2010-05-03)
sf\LICENSE (1043, 2010-05-03)
sf\Lists.v (35729, 2010-05-03)
sf\Logic.v (44994, 2010-05-03)
sf\Makefile (5639, 2010-05-03)
sf\MoreHoare.v (41537, 2010-05-03)
sf\MoreStlc.v (36355, 2010-05-03)
sf\Poly.v (50268, 2010-05-03)
sf\Preface.v (8271, 2010-05-03)
... ...
近期下载者：
相关文件：
收藏者：