[Haskell-cafe] In what language...?

[Alexander Solla]

On Oct 15, 2010, at 1:36 PM, Andrew Coppin wrote:

> Does anybody have any idea which particular dialect of pure math  
> this paper is speaking? (And where I can go read about it...)

It's some kind of typed logic with lambda abstraction and some notion  
of witnessing, using Gertzen (I think!) style derivation notation.   
Those A |- B things mean A "derives" B.  The "|-" is also called a  
Tee.  If your mail client can see underlining, formulas like

A, B
    |
    A

mean:

A, B |- A

That's where the Tee gets its name.  It's a T under A, B.  The former  
notation is better for some uses, since it "meshes" with the method of  
"truth trees".