Coq 正在参加 2020 年度 OSC 中国开源项目评选,请投票支持!
Coq 在 2020 年度 OSC 中国开源项目评选 中已获得 {{ projectVoteCount }} 票,请投票支持!
投票让它出道
已投票
Coq 获得 2020 年度 OSC 中国开源项目评选「最佳人气项目」 !
Coq 获得 2020 年度 OSC 中国开源项目评选「最佳人气项目」「最积极运营项目」 !
Coq 获得 2020 年度 OSC 中国开源项目评选「最积极运营项目」 !

软件简介

Coq 是一款交互式证明辅助工具,采用OCaml开发。Coq提供一套证明系统,可以编写证明,检查证明。Coq也提供一套形式化语言,可编写数学算法、定义、定理。Coq也可以用于程序的正确性证明(比如操作系统的安全性和编译器的正确性)。

展开阅读全文

代码

的 Gitee 指数为
超过 的项目

评论 (0)

加载中
更多评论
发表了资讯
2016/12/10 07:26

Coq 8.6 rc1 发布,交互式证明辅助工具

Coq 8.6 rc1 发布了,Coq 是一款交互式证明辅助工具,采用OCaml开发,提供一套证明系统,可以编写证明,检查证明。Coq 也提供一套形式化语言,可编写数学算法、定义、定理。Coq也可以用于程序的正确性证明(比如操作系统的安全性和编译器的正确性)。 更新内容: A new, faster state-of-the-art universe constraint c...

0
2
没有更多内容
加载失败,请刷新页面
点击加载更多
加载中
下一页
发表了博客
2019/09/22 22:45

Coq基础(一) - 基础

定义一个类型 在coq中,一个变量的类型往往表示为 var_name : var_type,即变量名后面的一个冒号后是变量的类型 Inductive type_name : Type :=   constructor 1   constructor 2   ...   constructor n. (*注意最后一个constructor的后面还有一个 . *) 即创建一个名为 type_name 的类型,该类型的变量的取值只能...

0
0
发表了博客
2018/08/02 18:06

数据和函数

1、枚举类型 Inductive day : Type := | monday : day | tuesday : day | wednesday : day | thursday : day | friday : day | saturday : day | sunday : day.   上面的例子定义了一个 day 的类型,包括 monday, tuesday, etc. 第二行以及下面可以读作"monday is a day, tuesday is a dat, etc...

0
0
2020/01/10 10:48

屌爆了,一句话描述各种编程语言

点击上方蓝字“开源优测”一起玩耍 Python: What if everything was a dict? Java: What if everything was an object? JavaScript: What if everything was a dict *and* an object? C: What if everything was ......

0
0
2019/05/13 21:42

收藏贴 :2019年必备43种区块链开发工具

本文列出2019年最新整理的用于区块链开发的43种流行的开发库、开发工具与开发框架。 原文:43个区块链开发工具 - 汇智网 1、MetaMask 人人都知道MetaMask。MetaMask是一个浏览器扩展,可以让你用普通的浏览器访问...

0
0
发表了博客
2020/07/25 00:01

Hacker News 简讯 2020-07-25

最后更新时间: 2020-07-25 23:01 Homeland Security Was Destined to Become a Secret Police Force - (newyorker.com) 国土安全局注定要成为一支秘密警察部队 得分:64 | 评论:5 Show HN: A simple CLI tool to ......

0
0
发表于服务端专区
2020/09/04 22:37

【Rust日报】2020-09-04 Rust 2021 Roadmap 计划

Rust 2021 Roadmap 计划 Rust的2021 Edition提上日程了,官方发布了一篇博客提到未来几周会同步进行两项重要的任务: 1)进行2020年Rust开发者问卷调查 2)希望每一位Rust开发者可以写一篇关于对Rust未来展望的博...

0
0
发表了博客
2018/12/19 18:06

数独高阶技巧之八——SDC

在本系列的第四篇“简单异数链”中,向大家介绍了XY-Wing等一系列Wing类技巧,并提到可以用(拐弯的)数组的观念来理解这些结构,经过第六篇ALS的学习之后,大家回过头再去看Wing,应该可以发现相关的实例都可以用ALS去解释。本篇则要介绍一种与上述结构类似的删除技巧——SDC(Sue de Coq)。 一、基本形态 Sue de Coq...

0
0
发表了博客
2011/11/01 23:42

[转]Scala是个有趣的语言

经常读我的博客的人应该知道,我最喜欢的编程语言是Haskell。我喜欢函数式编程,Haskell是一个能把函数式编程推向极致的语言。虽然如此,我仍然时刻关注着其它新兴的和即将产生的编程语言,特别是函数式的编程语言,所以,当Scala诞生之初我就知道了这种语言。当时,我粗略的对它了解了一下,并不是很喜欢;我感觉它的那...

0
0
发表了博客
2016/10/25 19:29

一个很“水”的Python爬虫入门代码文件

``` # _*_ coding: utf-8 _*_ """ python_spider.py by xianhu """ import urllib.error import urllib.parse import urllib.request import http.cookiejar # 首先定义下边可能需要的变量 url = "https://www.baidu.com" headers = {"User-Agent": "Mozilla/4.0 (compatible; MSIE 5.5; Windows NT)"} # 最简单的网页抓...

0
1
没有更多内容
加载失败,请刷新页面
点击加载更多
加载中
下一页
暂无内容
0 评论
3 收藏
分享
OSCHINA
登录后可查看更多优质内容
返回顶部
顶部