Coq(ProofCafe)

Coq是twitter上活動「言語擬人化学園もの」的角色，由ちょまど創作，現在為日本名古屋工作小組ProofCafe的看板娘。

簡介

Coq的創作原型為同名的一種用於驗證定理的證明是否正確的計算機工具。

髮飾「∀」「∃」代表一階邏輯的邏輯符號中的量化符號，「∀」為全稱量詞（universal quantifier），「∃」為存在量詞（existential quantifier）

「β」形狀的髪帶λ演算（lambda calculus）的函數概念β-归约