∆⊢e:A
Can someone explain this (from p. 3) to me, or point me to an explanation? I am especially unsure about the usage of ∆ and : in this context.
Can someone explain this (from p. 3) to me, or point me to an explanation? I am especially unsure about the usage of ∆ and : in this context.
Reading 1. It's a typing judgement. You can read ∆⊢e:A as "the program e has type A, assuming the free variables in e are typed as described by ∆".
Reading 2. It's a logical judgement. You can read ∆⊢e:A as "the proof e is a proof of the logical formula A, assuming the free variables in the proof e stand in for proofs as described by ∆".