Paper announcement: Constructive Foundations for Featherweight Java

Dear Friends and Colleagues,

I am pleased to announce the paper "Constructive Foundations
for Featherweight Java", available at:


Comments are welcome.

Best regards,
-- Thomas Studer


       Constructive Foundations for Featherweight Java

                         Thomas Studer

In this paper we present a recursion-theoretic denotational semantics
for Featherweight Java. Our interpretation is based on a formalization 
of the object model of Castagna, Ghelli and Longo in a predicative 
theory of types and names. Although this theory is proof-theoretically 
weak, it allows to prove many properties of programs written in
Featherweight Java. This underpins Feferman's thesis that impredicative
assumptions are not needed for computational practice. Moreover, the 
present work is also a contribution to the ongoing research on unifying
functional and object-oriented programming. It shows that these two
paradigms fit well together and that their combination has a sound
mathematical model.

Thomas Studer                                             office: 110
Universitaet Bern, IAM                      phone: +41 (0)31 631 4976
Neubrueckstrasse 10                      e-mail: tstuder@iam.unibe.ch    
CH-3012 Bern                        http://www.iam.unibe.ch/~tstuder/