[seek-kr-sms] Sth like this might be interesting for SEEK/KR-SMS

[Sergey Krivov]

This looks like a typical Type Theory thing.   Last spring I have read a
classical book on this subject:
http://books.google.com/books?id=BGBt4oNGP1cC&printsec=toc&dq=Type+theory+an
d+programming+languages
 And as I know there are decidable type checking algorithms for complex type
systems with records, subclasses, and even Boolean operations (though I have
not seen not/complement). Some complex cases :
http://www.cs.jhu.edu/~scott/pll/papers/mfps95.pdf
http://www.cs.jhu.edu/~scott/pll/papers/sas96.pdf

If you guys decide to construct a Type Theory to track Kepler's semantic
types I would like to get involved in that.

sergey

 
 
> -----Original Message-----
> From: seek-kr-sms-bounces at ecoinformatics.org [mailto:seek-kr-sms-
> bounces at ecoinformatics.org] On Behalf Of Bertram Ludaescher
> Sent: Thursday, August 10, 2006 3:15 PM
> To: seek-kr-sms
> Subject: [seek-kr-sms] Sth like this might be interesting for SEEK/KR-SMS
> 
> 
> Shawn (and others):
> 
> We should look at that and see whether/how this might be useful for us:
> 
> http://www.cs.ucdavis.edu/~su/publications/icse06-unit.pdf
> 
> (from a colleague down the hall).
> 
> Bertram
> 
> _______________________________________________
> Seek-kr-sms mailing list
> Seek-kr-sms at ecoinformatics.org
> http://mercury.nceas.ucsb.edu/ecoinformatics/mailman/listinfo/seek-kr-sms