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".
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
