Inferring Intersection Typings that are Equivalent to Call-by-Name and Call-by-Value Evaluations

We present a procedure to infer a typing for an arbitrary λ-term M in an intersection-type system that translates into exactly the call-by-name (resp., call-by-value) evaluation of M. Our framework is the recently developed System E which augments intersection types with expansion variables. The inferred typing for M is obtained by setting up a unification problem involving both type variables and expansion variables, which we solve with a confluent rewrite system. The inference procedure is compositional in the sense that typings for different program components can be inferred in any order, and without knowledge of the definition of other program components. Using expansion variables lets us achieve a compositional inference procedure easily. Termination of the procedure is generally undecidable. The procedure terminates and returns a typing if the input M is normalizing according to call-by-name (resp., call-by-value). The inferred typing is exact in the sense that the exact call-by-name (resp., call-by-value) behaviour of M can be obtained by a (polynomial) transformation of the typing. The inferred typing is also principal in the sense that any other typing that translates the call-by-name (resp., call-by-value) evaluation of M can be obtained from the inferred typing for M using a substitution-based transformation.

Computational Properties of SNAFU

Sensor applications in Sensoria [1] are expressed using STEP (Sensorium Task Execution Plan). SNAFU (Sensor-Net Applications as Functional Units) serves as a high-level sensor-programming language, which is compiled into STEP. In SNAFU’s current form, its differences with STEP are relatively minor, as they are limited to shorthands and macros not available in STEP. We show that, however restrictive it may seem, SNAFU has in fact universal power; technically, it is a Turing-complete language, i.e., any Turing program can be written in SNAFU (though not always conveniently). Although STEP may be allowed to have universal power, as a low-level language not directly available to Sensorium users, SNAFU programmers may use this power for malicious purposes or inadvertently introduce errors with destructive consequences. In future developments of SNAFU, we plan to introduce restrictions and highlevel features with safety guards, such as those provided by a type system, which will make SNAFU programming safer.

Safe Compositional Specification of Network Systems With Polymorphic, Constrained Types

In the framework of iBench research project, our previous work created a domain specific language TRAFFIC [6] that facilitates specification, programming, and maintenance of distributed applications over a network. It allows safety property to be formalized in terms of types and subtyping relations. Extending upon our previous work, we add Hindley-Milner style polymorphism [8] with constraints [9] to the type system of TRAFFIC. This allows a programmer to use for-all quantifier to describe types of network components, escalating power and expressiveness of types to a new level that was not possible before with propositional subtyping relations. Furthermore, we design our type system with a pluggable constraint system, so it can adapt to different application needs while maintaining soundness. In this paper, we show the soundness of the type system, which is not syntax-directed but is easier to do typing derivation. We show that there is an equivalent syntax-directed type system, which is what a type checker program would implement to verify the safety of a network flow. This is followed by discussion on several constraint systems: polymorphism with subtyping constraints, Linear Programming, and Constraint Handling Rules (CHR) [3]. Finally, we provide some examples to illustrate workings of these constraint systems.

Programming multicores safely : handling barrier deadlocks

Tese de doutoramento, Informática (Ciências da Computação), Universidade de Lisboa, Faculdade de Ciências, 2015

Memory Usage Inference for Object-Oriented Programs

We present a type-based approach to statically derive symbolic closed-form formulae that characterize the bounds of heap memory usages of programs written in object-oriented languages. Given a program with size and alias annotations, our inference system will compute the amount of memory required by the methods to execute successfully as well as the amount of memory released when methods return. The obtained analysis results are useful for networked devices with limited computational resources as well as embedded software.

Semantic data modelling and visualization using Noetica

Noetica is a tool for structuring knowledge about concepts and the reIationships between them. It differs from typical information systems in that the knowledge it represents is abstract, highly connected, and includes meta-knowledge (knowledge about knowledge). Noetica represents knowledge using a strongly typed graph data model. By providing a rich type system it is possible to represent conceptual information using formalized structures. A class hierarchy provides a basic classification for all objects. This allows for a consistency of representation that is not often found in `free' semantic networks, and gives the ability to easily extend a knowledge model while retaining its semantics. Visualization and query tools are provided for this data model. Visualization can be used to explore complete sets of link-classes, show paths while navigating through the database, or visualize the results of queries. Noetica supports goal-directed queries (a series of user-supplied goals that the system attempts to satisfy in sequence) and pathfinding queries (where the system finds relationships between objects in the database by following links).

Rehabilitation with ear prosthesis linked to osseointegrated implants

Background: The absence of an ear, which can be the result of a congenital malformation, surgical tumour resection or traumatic injury, is a significant aesthetic problem. Attachment of ear prostheses with adhesives can cause local irritation for the wearer and affect the colour of the prostheses. Use of implants in craniofacial reconstruction can improve the retention and stability of prostheses giving to patient greater comfort and security relative to adhesive attachment.Objective: The aim of this report was to present a clinical case of a mutilated patient who was rehabilitated by means of installing an ear prosthesis fixed through osseointegrated implants.Materials and methods: The patient had two implants installed in the mastoid region that were linked by a bar, and a clip-type system was used. The ear prosthesis was constructed from medical-use silicone, pigmented to match the patient's skin colour and linked to the retention system.Conclusion: The patient's rehabilitation was satisfactory from both a functional and an aesthetic point of view, making it possible for the patient to return to a normal social life and regain lost self-esteem.

Comunicação científica: agregação, compartilhamento e reuso de elementos informacionais

Pós-graduação em Ciência da Informação - FFC

Visão contemporânea do uso de implantes de conexão interna tipo cone morse

The Morse Taper implant system, developed from its introduction in engineering, has become increasingly effective for use in dentistry. However, other systems, main external hexagon type, have been used more frequently today. Current studies have been reported the positive features of the Morse taper system and even emphasized as ideal within the systems used in implantology. Unfortunately, some professional duty by not knowing this system, or even prefer hexagon type system by decreased cost of components, have refused to use it. Thus, this study was aimed to perform a brief review of the Morse taper system, emphasizing its main points of interest in dentistry, in an attempt to familiarize the professionals to at least learn more about this system that has the prospect to become the leading system implants used in dentistry in the coming years. It is concluded that this system of dental implants is favorable showing predictability and success.

Novos materiais multifuncionais para aplicação em fotocatálise

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Costrutti ed Applicazioni di Programmazione Generica in Linguaggi Object-Oriented

Generic programming is likely to become a new challenge for a critical mass of developers. Therefore, it is crucial to refine the support for generic programming in mainstream Object-Oriented languages — both at the design and at the implementation level — as well as to suggest novel ways to exploit the additional degree of expressiveness made available by genericity. This study is meant to provide a contribution towards bringing Java genericity to a more mature stage with respect to mainstream programming practice, by increasing the effectiveness of its implementation, and by revealing its full expressive power in real world scenario. With respect to the current research setting, the main contribution of the thesis is twofold. First, we propose a revised implementation for Java generics that greatly increases the expressiveness of the Java platform by adding reification support for generic types. Secondly, we show how Java genericity can be leveraged in a real world case-study in the context of the multi-paradigm language integration. Several approaches have been proposed in order to overcome the lack of reification of generic types in the Java programming language. Existing approaches tackle the problem of reification of generic types by defining new translation techniques which would allow for a runtime representation of generics and wildcards. Unfortunately most approaches suffer from several problems: heterogeneous translations are known to be problematic when considering reification of generic methods and wildcards. On the other hand, more sophisticated techniques requiring changes in the Java runtime, supports reified generics through a true language extension (where clauses) so that backward compatibility is compromised. In this thesis we develop a sophisticated type-passing technique for addressing the problem of reification of generic types in the Java programming language; this approach — first pioneered by the so called EGO translator — is here turned into a full-blown solution which reifies generic types inside the Java Virtual Machine (JVM) itself, thus overcoming both performance penalties and compatibility issues of the original EGO translator. Java-Prolog integration Integrating Object-Oriented and declarative programming has been the subject of several researches and corresponding technologies. Such proposals come in two flavours, either attempting at joining the two paradigms, or simply providing an interface library for accessing Prolog declarative features from a mainstream Object-Oriented languages such as Java. Both solutions have however drawbacks: in the case of hybrid languages featuring both Object-Oriented and logic traits, such resulting language is typically too complex, thus making mainstream application development an harder task; in the case of library-based integration approaches there is no true language integration, and some “boilerplate code” has to be implemented to fix the paradigm mismatch. In this thesis we develop a framework called PatJ which promotes seamless exploitation of Prolog programming in Java. A sophisticated usage of generics/wildcards allows to define a precise mapping between Object-Oriented and declarative features. PatJ defines a hierarchy of classes where the bidirectional semantics of Prolog terms is modelled directly at the level of the Java generic type-system.

Expression profiling und rationale Expressionsoptimierung am Beispiel eines prokaryontischen Wirt-,Vektor-Systems

Durch globale Expressionsprofil-Analysen auf Transkriptom-, Proteom- oder Metabolom-Ebene können biotechnologische Produktionsprozesse besser verstanden und die Erkenntnisse für die zielgerichtete, rationale Optimierung von Expressionssystemen genutzt werden. In der vorliegenden Arbeit wurde die Überexpression einer Glukose-Dehydrogenase (EC 1.1.5.2), die von der Roche Diagnostics GmbH für die diagnostische Anwendung optimiert worden war, in Escherichia coli untersucht. Die Enzymvariante unterscheidet sich in sieben ihrer 455 Aminosäuren vom Wildtyp-Enzym und wird im sonst isogenen Wirt-/Vektor-System in signifikant geringeren Mengen (Faktor 5) gebildet. Das prokaryontische Expressionssystem wurde auf Proteom-Ebene charakterisiert. Die 2-dimensionale differenzielle Gelelektrophorese (DIGE) wurde zuvor unter statistischen Aspekten untersucht. Unter Berücksichtigung von technischen und biologischen Variationen, falsch-positiven (α-) und falsch-negativen (β-) Fehlern sowie einem daraus abgeleiteten Versuchsdesign konnten Expressionsunterschiede als signifikant quantifiziert werden, wenn sie um den Faktor ≥ 1,4 differierten. Durch eine Hauptkomponenten-Analyse wurde gezeigt, dass die DIGE-Technologie für die Expressionsprofil-Analyse des Modellsystems geeignet ist. Der Expressionsstamm für die Enzymvariante zeichnete sich durch eine höhere Variabilität an Enzymen für den Zuckerabbau und die Nukleinsäure-Synthese aus. Im Expressionssystem für das Wildtyp-Enzym wurde eine unerwartet erhöhte Plasmidkopienzahl nachgewiesen. Als potenzieller Engpass in der Expression der rekombinanten Glukose-Dehydrogenase wurde die Löslichkeitsvermittlung identifiziert. Im Expressionsstamm für das Wildtyp-Enzym wurden viele Proteine für die Biogenese der äußeren Membran verstärkt exprimiert. Als Folge dessen wurde ein sog. envelope stress ausgelöst und die Zellen gingen in die stationäre Wuchsphase über. Die Ergebnisse der Proteomanalyse wurden weiterführend dazu genutzt, die Produktionsleistung für die Enzymvariante zu verbessern. Durch den Austausch des Replikationsursprungs im Expressionsvektor wurde die Plasmidkopienzahl erhöht und die zelluläre Expressionsleistung für die diagnostisch interessantere Enzymvariante um Faktor 7 - 9 gesteigert. Um die Löslichkeitsvermittlung während der Expression zu verbessern, wurde die Plasmidkopienzahl gesenkt und die Coexpression von Chaperonen initiiert. Die Ausbeuten aktiver Glukose-Dehydrogenase wurden durch die Renaturierung inaktiven Produkts aus dem optimierten Expressionssystem insgesamt um einen Faktor von 4,5 erhöht. Somit führte im Rahmen dieser Arbeit eine proteombasierte Expressionsprofil-Analyse zur zielgerichteten, rationalen Expressionsoptimierung eines prokaryontischen Modellsystems.

A study of two Languages for Active Objects with Futures

In computer systems, specifically in multithread, parallel and distributed systems, a deadlock is both a very subtle problem - because difficult to pre- vent during the system coding - and a very dangerous one: a deadlocked system is easily completely stuck, with consequences ranging from simple annoyances to life-threatening circumstances, being also in between the not negligible scenario of economical losses. Then, how to avoid this problem? A lot of possible solutions has been studied, proposed and implemented. In this thesis we focus on detection of deadlocks with a static program analysis technique, i.e. an analysis per- formed without actually executing the program. To begin, we briefly present the static Deadlock Analysis Model devel- oped for coreABS−− in chapter 1, then we proceed by detailing the Class- based coreABS−− language in chapter 2. Then, in Chapter 3 we lay the foundation for further discussions by ana- lyzing the differences between coreABS−− and ASP, an untyped Object-based calculi, so as to show how it can be possible to extend the Deadlock Analysis to Object-based languages in general. In this regard, we explicit some hypotheses in chapter 4 first by present- ing a possible, unproven type system for ASP, modeled after the Deadlock Analysis Model developed for coreABS−−. Then, we conclude our discussion by presenting a simpler hypothesis, which may allow to circumvent the difficulties that arises from the definition of the ”ad-hoc” type system discussed in the aforegoing chapter.

Deadlock analysis of asynchronous sequential processes

In this thesis we present ad study an object-oriented language, characterized by two different types of objects, passive and active objects, of which we define the operational syntax and semantics. For this language we also define the type system, that will be used for the type checking and for the extraction of behavioral types, which are an abstract description of the behavior of the methods, used in deadlock analysis. Programs can manifest deadlock due to the errors of the programmer. To statically identify possible unintended behaviors we studied and implemented a technique for the analysis of deadlock based on behavioral types.

Practical, Pluggable Types for a Dynamic Language

Most languages fall into one of two camps: either they adopt a unique, static type system, or they abandon static type-checks for run-time checks. Pluggable types blur this division by (i) making static type systems optional, and (ii) supporting a choice of type systems for reasoning about different kinds of static properties. Dynamic languages can then benefit from static-checking without sacrificing dynamic features or committing to a unique, static type system. But the overhead of adopting pluggable types can be very high, especially if all existing code must be decorated with type annotations before any type-checking can be performed. We propose a practical and pragmatic approach to introduce pluggable type systems to dynamic languages. First of all, only annotated code is type-checked. Second, limited type inference is performed on unannotated code to reduce the number of reported errors. Finally, external annotations can be used to type third-party code. We present Typeplug, a Smalltalk implementation of our framework, and report on experience applying the framework to three different pluggable type systems.