Simple Dependent Types: Concord
By Paul Jolly,
Sophia Drossopoulou,
Christopher Anderson and Klaus
Ostermann.
Last revised 2004/05/31
Download: [ps] [ps.gz] [pdf] (FTfJP workshop (final) version1 - May 2004)
Download: [ps] [ps.gz] [pdf] (FTfJP accepted version2 - April 2004)
Abstract
We suggest a simple model for a restricted form of dependent types in
object oriented languages, whereby classes belong to groups and dependency
is introduced via intra-group references using the MyGrp
keyword. We introduce motivating and exploratory examples, present the
formal model and outline soundness of the type system.
BibTeX
@inproceedings{jolly04concord,
author = {Paul Jolly and Sophia Drossopoulou and Christopher Anderson and Klaus Ostermann},
title = {{Simple Dependent Types: Concord (FTfJP workshop version)}},
crossref = {FTfJP04},
month = {June},
url = {http://myitcv.org.uk/papers/concord04.html},
}
@techreport{FTfJP04,
editor = {Susan Eisenbach and Gary T. Leavens and Peter M{\"u}ller and Arnd Poetzsch-Heffter and Erik Poll},
author = {Erik Poll},
title = {{Formal Techniques for Java-like Programs 2004 (Proceedings)}},
institution = {Oslo, Norway},
year = {2004},
type = {Technical Report},
}
1 The workshop version will appear in the FTfJP workshop
proceedings, May 2004.
2 The accepted version is a slightly
longer paper, containing complete formal definitions and more
examples.
|