九款编程语言以及缔造它们的伟大女性

Coq

缔造者: Christine Paulin-Mohring协同Thierry Coquand、Gérard Huet、Bruno Barras、Jean-Christophe Filliâtre、Hugo Herbelin、Chet Murthy、Yves Bertot以及Pierre Castéran

年份: 1991年

背景故事: 1984年，法国计算机科学家Gérard Huet以及Thierry Coquand开始着手开发一套交互型系统，专门针对数学定理进行相关证明过程。其初始版本为Coquand打造的Calculus of Constructions（即构造演算），简称为CoC。1991年，Christine Paulin-Mohrin以Calculus of Inductive Constructions为基础创建出了一套新的实现方案，并将该语言重新命名为Coq——这正是为了向Coquand致敬。除了数学定理之外，颇具知名度的Coq Proof Assistant System（即Coq证明辅助系统）也被用于进行软件验证。Paulin-Mohring已经被编程业界广泛视为这款重要语言及工具的主要开发者之一。

（编辑：PHP编程网 - 湛江站长网）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!