This thesis presents Topological Domain Theory as a powerful and flexible framework for denotational semantics. Topological Domain Theory models a wide range of type constructions and can interpret many computational features. Furthermore, it has close connections to established frameworks for denotational semantics, as well as to well-studied mathematical theories, such as topology and computable analysis. We begin by describing the categories of Topological Domain Theory, and their categorical structure. In particular, we recover the basic constructions of domain theory, such as products, function spaces, fixed points and recursive types, in the context of Topological Domain Theory. As a central contribution, we give a detailed account of how computational effects can be modelled in Topological Domain Theory. Following recent work of Plotkin and Power, who proposed to construct effect monads via free algebra functors, this is done by showing that free algebras for a large class of parametrised equational theories exist in Topological Domain Theory. These parametrised equational theories are expressive enough to generate most of the standard examples of effect monads. Moreover, the free algebras in Topological Domain Theory are obtained by an explicit inductive construction, using only basic topological and set-theoretical principles. We also give a comparison of Topological and Classical Domain Theory. The category of omega-continuous dcpos embeds into Topological Domain Theory, and we prove that this embedding preserves the basic domain-theoretic constructions in most cases. We show that the classical powerdomain constructions on omega-continuous dcpos, including the probabilistic powerdomain, can be recovered in Topological Domain Theory. Finally, we give a synthetic account of Topological Domain Theory. We show that Topological Domain Theory is a specific model of Synthetic Domain Theory in the realizability topos over Scott's graph model. We give internal characterisations of the categories of Topological Domain Theory in this realizability topos, and prove the corresponding categories to be internally complete and weakly small. This enables us to show that Topological Domain Theory can model the polymorphic lambda-calculus, and to obtain a richer collection of free algebras than those constructed earlier. In summary, this thesis shows that Topological Domain Theory supports a wide range of semantic constructions, including the standard domain-theoretic constructions, computational effects and polymorphism, all within a single setting.

Network-on-chip (NoC) based multi-processor systems-on-chip (MPSoCs) are promising candidates for future multi-processor embedded platforms, which are expected to be composed of hundreds of heterogeneous processing elements (PEs) to potentially provide high performances. However, together with the performances, the systems complexity will increase, and new high level design techniques will be needed to efficiently model, simulate, debug and synthesize them. System-level design (SLD) is considered to be the next frontier in electronic design automation (EDA). It enables the description of embedded systems in terms of abstract functions and interconnected blocks. A promising complementary approach to SLD is the use of models of computation (MoCs) to formally describe the execution semantics of functions and blocks through a set of rules. However, also when this formalization is used, there is no clear way to synthesize system-level models into software (SW) and hardware (HW) towards a NoC-based MPSoC implementation, i.e., there is a lack of system design automation (SDA) techniques to rapidly synthesize and prototype system-level models onto heterogeneous NoC-based MPSoCs. In addition, many of the proposed solutions require large overhead in terms of SW components and memory requirements, resulting in complex and customized multi-processor platforms. In order to tackle the problem, a novel model-based SDA flow has been developed as part of the thesis. It starts from a system-level specification, where functions execute according to the synchronous MoC, and then it can rapidly prototype the system onto an FPGA configured as an heterogeneous NoC-based MPSoC. In the first part of the thesis the HeartBeat model is proposed as a model-based technique which fills the abstraction gap between the abstract system-level representation and its implementation on the multiprocessor prototype. Then details are provided to describe how this technique is automated to rapidly prototype the modeled system on a flexible platform, permitting to adjust the system specification until the designer is satisfied with the results. Finally, the proposed SDA technique is improved defining a methodology to automatically explore possible design alternatives for the modeled system to be implemented on a heterogeneous NoC-based MPSoC. The goal of the exploration is to find an implementation satisfying the designer's requirements, which can be integrated in the proposed SDA flow. Through the proposed SDA flow, the designer is relieved from implementation details and the design time of systems targeting heterogeneous NoC-based MPSoCs on FPGA is significantly reduced. In addition, it reduces possible design errors proposing a completely automated technique for fast prototyping. Compared to other SDA flows, the proposed technique targets a bare-metal solution, avoiding the use of an operating system (OS). This reduces the memory requirements on the FPGA platform comparing to related work targeting MPSoC on FPGA. At the same time, the performance (throughput) of the modeled applications can be increased when the number of processors of the target platform is increased. This is shown through a wide set of case studies implemented on FPGA. / <p>QC 20140609</p>