Type Class Polymorphism in an Institutional Framework

Higher-order logic with shallow type class polymorphism is widely used as a specification formalism. Its polymorphic entities (types, operators, axioms) can easily be equipped with a ‘naive’ semantics defined in terms of collections of instances. However, this semantics has the unpleasant property that while model reduction preserves satisfaction of sentences, model expansion generally does not. In other words, unless further measures are taken, type class polymorphism fails to constitute a proper institution, being only a so-called rps preinstitution; this is unfortunate, as it means that one cannot use institution-independent or heterogeneous structuring languages, proof calculi, and tools with it. Here, we suggest to remedy this problem by modifying the notion of model to include information also about its potential future extensions. Our construction works at a high level of generality in the sense that it provides, for any preinstitution, an institution in which the original...

• Type: Conference
• Year: 2004
• Where: WADT
• Authors: Lutz Schröder, Till Mossakowski, Christoph Lüth
• Keywords: HasCasl’s Polymorphism, Semantic, Software Engineering, Type Class Polymorphism, WADT 2004