|Typechecking union types firstname.lastname@example.org (Thomas Christensen) (2006-06-27)|
|Re: Typechecking union types email@example.com (Curtis W) (2006-07-05)|
|Re: Typechecking union types DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-07-05)|
|Re: Typechecking union types firstname.lastname@example.org (2006-07-05)|
|Re: Typechecking union types email@example.com (Thomas Christensen) (2006-07-28)|
|From:||"Thomas Christensen" <firstname.lastname@example.org>|
|Date:||28 Jul 2006 18:55:09 -0400|
|Posted-Date:||28 Jul 2006 18:55:09 EDT|
Thanks for your answers, sorry for the delay.
The language to be typechecked is VDM++, an object-oriented formal
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
"Thomas Christensen" <email@example.com> wrote in message
> 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.
> Thomas Christensen
Return to the
Search the comp.compilers archives again.