blob: 387ac8a855f0c5d199880d5e7b42f1c3f07964bf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
+++
title = "Stack Machine"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b1"]
forwardlinks = ["3b3"]
zettelid = "3b2"
+++
The theoretical foundation of Coq is called Calculus of Inductive
Constructions (CIC), an extension to the older Calculus of Construction
(CoC). Gallina is actually an extension of CIC which is all the code
that comes after the `:=` and before the period. Next there is LTac,
which is a domain-specific language for writing proofs and decision
procedures. Finally, commands like `Inductive` and `Definition` are the
Vernacular, which supports many queries to the Coq system.
|
