评论删除后，数据将无法恢复
Coq 是一款交互式证明辅助工具，采用OCaml开发。Coq提供一套证明系统，可以编写证明，检查证明。Coq也提供一套形式化语言，可编写数学算法、定义、定理。Coq也可以用于程序的正确性证明（比如操作系统的安全性和编译器的正确性）。
加载中
删除一条评论
Coq 8.6 rc1 发布，交互式证明辅助工具
Coq 8.6 rc1 发布了，Coq 是一款交互式证明辅助工具，采用OCaml开发，提供一套证明系统，可以编写证明，检查证明。Coq 也提供一套形式化语言，可编写数学算法、定义、定理。Coq也可以用于程序...
没有更多内容
加载失败，请刷新页面
没有更多内容
暂无问答
一个很“水”的Python爬虫入门代码文件
转
``` # _*_ coding: utf-8 _*_ """ python_spider.py by xianhu """ import urllib.error import urllib.parse import urllib.request import http.cookiejar # 首先定义下边可能需要的变量 ...
[转]Scala是个有趣的语言
转
经常读我的博客的人应该知道，我最喜欢的编程语言是Haskell。我喜欢函数式编程，Haskell是一个能把函数式编程推向极致的语言。虽然如此，我仍然时刻关注着其它新兴的和即将产生的编程语言，特...
谈语法
转
使用和研究过这么多程序语言之后，我觉得几乎不包含多余功能的语言，只有一个：Scheme。所以我觉得它是学习程序设计最好的入手点和进阶工具。当然 Scheme 也有少数的问题，而且缺少一些我想要...
BBS时代落幕？我们还有“下一代的论坛”——Discourse
原
在中国有着20年历史的网易论坛本周宣布将在下个月关闭服务，很多媒体称此举预示着中国传统BBS时代的日渐沉沦，还有网友担心天涯、豆瓣、西祠还能坚持多久？ 
中科大linux用户组推荐的linux相关书目
原
大都是比较知名的书，豆瓣都可以找到，上网时发现科大的同学整理了出来，比较系统。另外，科大LUG的每周小聚分享的slides也在网上共享了，挺不错。 Linux入门 书名 作者 定价（￥） 备注 借阅...
信息系统项目管理师---案例分析知识点
原
整体管理 项目整体管理的过程包括如下内容 ： ① 制定项目章程 —通过发布项目章程，正式地批准项目并授权项目经理在项目活动中使用组织资 源。 ② 制定项目管理计划 —定义、准备和协调所有...
干货|公有链的8大挑战及其解决方案
转
区块链存在一些技术壁垒，这导致难以有效地将它应用到主流人群里。本文不仅指出了这些技术壁垒，同时提出了解决方案。
没有更多内容
加载失败，请刷新页面
评论(0)
暂无评论