[Haskell-cafe] In what language...?
Alexander Solla
ajs at 2piix.com
Fri Oct 15 17:16:10 EDT 2010
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".
More information about the Haskell-Cafe
mailing list