You are here:
(02 Sep 2010,
Date: 2009-04-09 Time: 11:45 Room: BBL room 471 ----+++ Speaker: Arie Middelkoop ----+++ Title: Algorithmic Type Inferencer Specifications for Declarative Type Systems ----+++ Abstract A _type system_ defines which types are valid for an expression. A _type inferencer_ tries to construct a most general valid type for an expression. Therefore, a type system serves as a specification for a type inferencer. For non-trivial type systems, there is an enormous gap between specification and implementation. We are working on closing this gap by coming up with executable specifications. Type rules are not used as the language for our specification. Instead, we use _inferencer rules_. These inferencer rules are similar to type rules, except that they contain annotations that describe how to actually perform computations. When we straightforwardly transform the type rules into type inferencer rules, we encounter problems with declarative aspects of type rules. One particular problem is that a type rule may refer to a value that during inference is not available yet when the corresponding inference rule is executed. We solve this problem by providing annotations that deal with this problem in a specific way, but general enough to work for many type systems. During this talk, I'll demonstrate this inferencer language and its semantics by means of an example: obtaining an inferencer from a relatively simple impredicative type system.
ore topic actions
Topic revision: r2 - 02 Sep 2010,
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS?