Mon, 22 Feb 1999 15:12:08 -0800 (PST)
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:
A->B or C
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 <firstname.lastname@example.org>
This message is placed in the public domain.