Links

Notes about Coq

Prop is impredicative. A definition is said to be impredicative if it generalises over the totality to which the the entity being defined belongs.

Otherwise said, a statement of the form ∀ A : Prop, P A can be instantiated by itself: if ∀ A : Prop, P A is provable, then P (∀ A : Prop, P A) is.
Set is predicative. It lays at the bottom of the type hierarchy.
Type is stratified, but its universe level is hidden from the user.
All proofs are provided via tactics. Tactics are applied in an imperative style. Some tactics map to pattern matching, but pattern matching on dependent types requires overhead.
Invariants are not carried through datatypes. Instead proofs and data are split.
Many of the tactics are extremely powerful.
Coq has a minimal kernel to which everything compiles to.
Coq does not support induction-recursion.

With continuation passing, channels are required to be linear.
We do HOAS, and Coq does not support linearity.
We must be able to traverse a process and check the creation and usage of channels.
To do so we can use the parametricity of HOAS.
Channels can be sent over channels. To properly check the linearity of these channels sent over channels, we would need to actually evaluate the process. A way of avoiding that is to mark a channel as used when it's sent as a message. When it is received as a message, we make a new created mark. This way we avoid evaluation, at the cost of treating the same channel as two different channels.
All messages cannot be treated equally: we need to know whether they are channels or plain messages.