Re: Typechecking union types

Hi again,


Thanks for your answers, sorry for the delay.


The language to be typechecked is VDM++, an object-oriented formal
specification language.
See http://www.vdmbook.com/langmanpp_a4.pdf for details.


The language is used for modelling and as such is not required to
be executable. It supports a range of "broad" datatypes such as
unions, sets and set comprehensions, injective maps and map
comprehension as well as type invariants.


The union types and the static invariants add additional undecidability.


For example we may define a variable to be of a union type:


        x : nat | bool


Which is the union of booleans and the natural numbers.
This leads to problems when typechecking the expression


        x + 1


The expression will be type correct if x is a natural number, and
type incorrect if x is a boolean.


Type invariants can be added:


        Nat5 = nat
        inv n == n > 4


The type Nat5 then represents the natural numbers greater than 4.


The current approach in the available tools is to generate proof
obligations which the user must manually discharge.


What I am looking for is pointers to articles, books and research on
typechecking various "difficult" constructs, such as union types and
invariants.


Regards
Thomas Christensen












"Thomas Christensen" <tc@elvis.dk> wrote in message
news:06-06-072@comp.compilers...
> Hi,
>
> For my master thesis, I need to get up to speed
> on the current state of the art within the somewhat
> narrow field of typechecking union types.
>
> Can anyone point me to some good starting points, books,
> papers, articles. I have Benjamin Pierce's book, "Types and Programming
> Languages" and am currently ploughing my way through that.
>
> What I need is some background on the various problems/issues related
> specifically to union types.
>
> Regards
> Thomas Christensen
>

Return to the comp.compilers page.
Search the comp.compilers archives again.