3 ms·
As this paper is about a Curry-Howard correspondence, the statement has two (equivalent) readings. Reading 1. It's a typing judgement. You can read ∆⊢e:A as "t
by mafribe 10y ago
As this paper is about a Curry-Howard correspondence, the statement has two (equivalent) readings.
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 ∆".
- jraedisch 10y agoThanks! I took a look at the Wiki page https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... but didn't see any Deltas there.
- mafribe 10y agoLogical and typing judgements can be presented in many different ways, triples like ∆⊢e:A being one of them.
- s_ngularity 10y agoA great overview of this stuff is http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
- jraedisch 10y agoAnd this one actually has Deltas in it. Thanks!
- greydius 10y agoIt's common to use Γ (gamma) as well.