Constructive Foundations for Featherweight Java

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 prooftheoretically 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.

• Type: Conference
• Year: 2001
• Where: DAGSTUHL
• Authors: Thomas Studer
• Keywords: DAGSTUHL 2001, DAGSTUHL 2007, Featherweight Java, Object Model, Recursion-theoretic Denotational Semantics