Shallow encoding

http://www4.di.uminho.pt/~mjf/pub/SFV-CurryHoward-2up.pdf にいいことが書いてある。

Shallow encoding (Logical Frameworks).

The type theory is used as a logical framework, a meta system for encoding a specific logic one wants to work with.
The encoding of a logic L is done by choosing an appropriate context Γ_L, in which the language of L and the proof rules are declared.
Usually, the proof-assistants based on this kind of encoding do not produce standard proof-objects, just proof-scripts.

Isabelleはシャローエンコーディングだ。CoqはDirect encoding。