Suguivy@ekaitz_zarraga Coq is a proof assistant, it implements a type theory called the Calculus of Inductive Constructions (I don't know how is it). But in Coq it's not that easy to see that when using it because it uses "tactics" that are like an abstraction to prove things more easily. In another languages like Agda you can see that correspondence better.
Chirp! is a GNU Social instance for the Cooley and Sekula families and their friends.
Chirp! is a social network. It runs on GNU social, version 2.0.1-beta0, available under the GNU Affero General Public License.
All Chirp! content and data are available under the Creative Commons Attribution 3.0 license.