The role of animacy and definiteness in the clitic-DP nexus

We extend Cuervo's (2003) analysis of the Lower Applicative Dative DP in Spanish to account for the animate definite DP preceded by a and the fact that it is not possible to have both an animate dative definite direct object and a dative indirect object in the same clause. We argue that the presence of such a dative DP 'blocks' the upward movement of the direct object DP to the specifier of the Lower Applicative phrase. We analyse the case ‘mismatch’ between the third person accusative clitic and the co-referring dative DP with animate definite reference in River Plate Spanish as resulting from the raising of the accusative clitic to the head of the Applicative phrase and the movement of the DP to its specifier, where dative case is always assigned in Spanish. We propose that similar phenomena observed in some Australian languages are amenable to a similar analysis.

Introducing reference semantics via refinement

Two types of semantics have been given to object-oriented formal specification languages. Value semantics denote a class by a set of values representing its objects. Reference semantics denote a class by a set of references, or pointers, to values representing its objects. While adopting the former facilitates formal reasoning, adopting the latter facilitates transformation to object-oriented code. In this paper, we propose a combined approach using value semantics for abstract specification and reasoning, and then refining to a reference semantics before transforming specification to code.

A partial-correctness semantics for modelling assembler programs

Previous work on formally modelling and analysing program compilation has shown the need for a simple and expressive semantics for assembler level programs. Assembler programs contain unstructured jumps and previous formalisms have modelled these by using continuations, or by embedding the program in an explicit emulator. We propose a simpler approach, which uses techniques from compiler theory in a formal setting. This approach is based on an interpretation of programs as collections of program paths, each of which has a weakest liberal precondition semantics. We then demonstrate, by example, how we can use this formalism to justify the compilation of block-structured high-level language programs into assembler.