proofs/typesystems

[Tril]

hi I saw your question on the irc log.
Where did you hear about doing proofs with typesystems? I do not have any
experience with this, but my abstract framework that I am writing specs
on, is moving straight in this direction.  Here's how it will work:
If there is a type A, with subtypes B and C, but B and C do not overlap,
and (B union C) is equal to A,
you can conclude all of the following:
B->A
C->A
A->B or C
B->not C
C->not B

also, if there is a type D which is a subtype of C, then you know
D->C, and everything that C implies (A and not B), is true of D also.

If everything in the system is integrated in this typesystem, you can make
a large number of conclusions automatically.  The relationship between all
data and programs is very clear.  Also, types can be represented visually.  

I am very interested to find other systems which use typesystems as the
object of logical reasoning.  Unfortunately I will not be looking for
these systems actively, so I can work on my specs.  If others would like
to research this, please do!

David Manifold <dem@tunes.org>
This message is placed in the public domain.