Coq(ProofCafe)

Coq是twitter上活动「言语拟人化学园もの」的角色，由ちょまど创作，现在为日本名古屋工作小组ProofCafe的看板娘。

简介

Coq的创作原型为同名的一种用于验证定理的证明是否正确的计算机工具。

发饰「∀」「∃」代表一阶逻辑的逻辑符号中的量化符号，「∀」为全称量词（universal quantifier），「∃」为存在量词（existential quantifier）

「β」形状的发带λ演算（lambda calculus）的函数概念β-归约