[isabelle] Paper available (1)

Dear all,

we proudly announce our paper:

Achim D. Brucker and Burkhart Wolff. Extensible Universes for Object- Oriented Data Models. In Proceedings of the European Conference of Object-Oriented Programming (ECOOP 2008). LNCS 5142 Springer-Verlag, 2008.

A pdf is available under:

Key features are:

- We provide a data-type package for object-oriented class systems;
  it generates a theory with the usual oo infra-structure,
  i.e. a typed state with typed constructors and accessors,
  dynamic type-tests and (loss-less) casts
- all properties are proven from conservative definitions,
  the approach is based on a generalization of extensible records
- accessors can have types over arbitrary nestings of type-constructors
  such as list, pairs, but also (general) sets, total functions, ...
  Types are neither bound to be countable nor to represent domains ...
  (For those who get curious here: The underlying type-discipline
  allows Universe-constructions U_(n+1) = A + U_(n) => U_(n),
  but rules out circularities like U_(n) = A + U_(n) => U_(n) for
  =>  the total function space).
- the package supports incremental definitions of class systems,
  by default, it supports the "open world" assumption

Comments and discussions are welcome !

Best regards,

Burkhart (& Achim)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.