The Need for Type Theory in Semantic Web Services

INTRODUCTION My name is Rod Moten. I am a senior computer scientist at Bloomberg L.P., a financial market data company. Currently I'm involved in ontology and taxonomy development. Prior to coming to Bloomberg, I was an assistant professor at Colgate University. While on a sabbatical, I visited RPI. At RPI, I conducted research on using type theory to resolve semantic heterogeneity in multi--agent systems [6, 7]. In this work, I showed how type theory could be used to implement a technique for automatically resolving semantic heterogeneity between software agents. The technique is an o#shoot of the proofs--as--programs technique created in the 1970's [2, 1]. The proofs--as--programs paradigm was developed by researchers in the formal methods community to develop software that was guaranteed to correctly implement its specification. The specifications were stated as logical assertions. If a proof could be constructed from the specification, then a program could be extracted from the