Gallina

Gallina

Coqの内部で使われている言語。 イタリア語、スペイン語などで雌鶏(メスのにわとり)を意味する。

Specification Languageであり、かつFunctional Programming Languageであるこの言語の正体は実はラムダ項である。

Coqではterm, type, proof, programを記述するために使われる。