Capitalizing on its comparative political and social stability in the region, in recent years the Moroccan regime has been attracting global and regional investors with the promise of new ... Show moreCapitalizing on its comparative political and social stability in the region, in recent years the Moroccan regime has been attracting global and regional investors with the promise of new ‘megaprojects’ that aim to radically transform local natural, economic and social landscapes. Inaugurated in 2018, Morocco’s (and Africa’s) first high-speed rail line (LGV) is considered a flagship project within this landscape. Part of a wider ‘development corridor’, this 2-billion-euro infrastructure has become invested with political, ideological, and strongly affective meanings related to ideas of mobility and future prosperity, even as it violently displaced informal housing communities and created disruptions along the existing rail network. Drawing on the recent theoretical apparatus of anthropologies of infrastructure, this paper traces the ways in which the introduction of high-speed railway has thrown into stark relief the scaling of geographical and temporal relationships of belonging in Morocco. From this exploration scale emerges as a political process of spatiotemporal re-arrangement that contributes to the consolidation of particular power relations while also providing a conduit for their critique. Show less
In this thesis we investigate different techniques and formalisms to address complexity introduced by unbounded structures in object-oriented programs. We give a representation of a weakest... Show moreIn this thesis we investigate different techniques and formalisms to address complexity introduced by unbounded structures in object-oriented programs. We give a representation of a weakest precondition calculus for abstract object creation in dynamic logic. Based on this calculus we define symbolic execution including abstract object creation. We investigate the complex behaviour introduced by multi-threading and give a formalism based on the transformation of multi-threaded reentrant call-graphs to thread automata and the application of context free language reachability to decide deadlock freedom of such programs. We give a formalisation of the observable interface behaviour of a concurrent, object-oriented language with futures and promises. The calculus captures the core of the Creol language and allows for a comparison with the concurrency model of thread-based, object-oriented languages like Java or C#. We give a technique to detect deadlock freedom for an Actor-like subset of the Creol language. Show less
