[isabelle] Paper available (1)
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,
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 !
Burkhart (& Achim)
This archive was generated by a fusion of
Pipermail (Mailman edition) and