Truth and falsehood, questions and answers, construction and deconstruction; most things come in dual pairs. Duality is a mirror that reveals the new from the old via opposition. This idea appears pervasively in logic, where duality inverts "true" with "false" and "and" with "or." However, even though programming languages are closely connected to logics, this kind of strong duality is not so apparent in practice. Sum types (disjoint tagged unions) and product types (structures) are dual concepts, but in the realm of programming, natural biases obscure their duality. To better understand the role of duality in programming, we shift our perspective. Our approach is based on the Curry-Howard isomorphism which says that programs following a specification are the same as proofs for mathematical theorems. This thesis explores Gentzen's sequent calculus, a logic steeped in duality, as a model for computational duality. By applying the Curry-Howard isomorphism to the sequent calculus, we get a language that combines dual programming concepts as equal opposites: data types found in functional languages are dual to co-data types (interface-based objects) found in object-oriented languages, control flow is dual to information flow, induction is dual to co-induction. This gives a duality-based semantics for reasoning about programs via orthogonality: checking safety and correctness based on a comprehensive test suite. We use the language of the sequent calculus to apply ideas from logic to issues relevant to program compilation. The idea of logical polarity reveals a symmetric basis of primitive programming constructs that can faithfully represent all user-defined data and co-data types. We reflect the lessons learned back into a core language for functional languages, at the cost of symmetry, with the relationship between the sequent calculus and natural deduction. This relationship lets us derive a pure lambda calculus with user-defined data and co-data which we further extend by bringing out the implicit control-flow in functional programs. Explicit control-flow lets us share and name control the same way we share and name data, enabling a direct representation of join points, which are essential for tractable optimization and compilation.

[pt] Linguagens de programação tem tradicionalmente sido classificadas como estaticamente tipadas ou dinamicamente tipadas, estas últimas também sendo conhecidas como linguagens de scripting. Linguagens com tipagem dinâmica são bastante populares para a escrita de programas menores, um cenário onde a facilidade de uso e flexibilidade da linguagem são altamente valorizados. No entanto, com o passar do tempo, pequenos scripts podem se tornar grandes sistemas e a flexibilidade da linguagem pode passar a ser uma fonte de defeitos no programa. Para estes sistemas maiores, a tipagem estática, que oferece detecção de erros em tempo de compilação, melhor documentação e oportunidades de otimização, passa a ser mais atrativa. Como reescrever todo o sistema em uma linguagem estática não é ideal do ponto de um vista da engenharia de software, encontrar formas de adicionar tipos estáticos em programas dinamicamente tipados já existentes tem sido uma área de pesquisa bem rica. Nesse trabalho, nós apresentamos uma perspectiva histórica dessa pesquisa. Nos focamos em abordagens que não são específicas para uma única linguagem de programação, como as Type Hints de Common LISP, o Soft Typing de Fagan et al e o Gradual Typing de Siek et al, contrastando essas diferentes soluções a partir de uma perspectiva moderna. / [en] Programming languages have traditionally been classified as either statically typed or dynamically typed, the latter often being known as scripting languages. Dynamically typed languages are very popular for writing smaller programs, a setting where ease of use and flexibility of the language are highly valued. However, with time, small scripts tend to evolve into large systems and the flexibility of the dynamic language may become a source of program defects. For these larger systems, static typing, which offers compile-time error detection, improved documentation and optimization opportunities, becomes more attractive. Since rewriting the whole system in a statically typed language is not ideal from a software engineering point of view, investigating ways of adding static types to existing dynamically typed programs has been a thriving research area. In this work, we present a historical overview of this research. We focus on general approaches that apply to multiple programming languages, such as the Type Hints of Common LISP, the Soft Typing of Fagan et al and the Gradual Typing of Siek et al, contrasting these different solutions from a modern perspective.

No description available.

[pt] Linguagens dinamicamente tipadas, tais como Lua, não usam tipos estáticos em favor de simplicidade e exibilidade, porque a ausência de tipos estáticos significa que programadores não precisam se preocupar em abstrair tipos que devem ser validados por um verificador de tipos. Por outro lado, linguagens estaticamente tipadas ajudam na detecção prévia de diversos bugs e também ajudam na estruturação de programas grandes. Tais pontos geralmente são vistos como duas vantagens que levam programadores a migrar de uma linguagem dinamicamente tipada para uma linguagem estaticamente tipada, quando os pequenos scripts deles evoluem para programas complexos. Sistemas de tipos opcionais nos permitem combinar tipagem dinâmica e estática na mesma linguagem, sem afetar a semântica original da linguagem, tornando mais fácil a evolução de código tipado dinamicamente para código tipado estaticamente. Desenvolver um sistema de tipos opcional para uma linguagem dinamicamente tipada é uma tarefa desafiadora, pois ele deve ser o mais natural possível para os programadores que já estão familiarizados com essa linguagem. Neste trabalho nós apresentamos e formalizamos Typed Lua, um sistema de tipos opcional para Lua, o qual introduz novas características para tipar estaticamente alguns idiomas e características de Lua. Embora Lua compartilhe várias características com outras linguagens dinamicamente tipadas, em particular JavaScript, Lua também possui várias características não usuais, as quais não estão presentes nos sistemas de tipos dessas linguagens. Essas características incluem funções com aridade flexível, atribuições múltiplas, funções que são sobrecarregadas no número de valores de retorno e a evolução incremental de registros e objetos. Nós discutimos como Typed Lua tipa estaticamente essas características e também discutimos nossas decisões de projeto. Finalmente, apresentamos uma avaliação de resultados, a qual obtivemos ao usar Typed Lua para tipar código Lua existente. / [en] Dynamically typed languages such as Lua avoid static types in favor of simplicity and exibility, because the absence of static types means that programmers do not need to bother with abstracting types that should be validated by a type checker. In contrast, statically typed languages provide the early detection of many bugs, and a better framework for structuring large programs. These are two advantages of static typing that may lead programmers to migrate from a dynamically typed to a statically typed language, when their simple scripts evolve into complex programs. Optional type systems allow combining dynamic and static typing in the same language, without affecting its original semantics, making easier this code evolution from dynamic to static typing. Designing an optional type system for a dynamically typed language is challenging, as it should feel natural to programmers that are already familiar with this language. In this work we present and formalize the design of Typed Lua, an optional type system for Lua that introduces novel features to statically type check some Lua idioms and features. Even though Lua shares several characteristics with other dynamically typed languages such as JavaScript, Lua also has several unusual features that are not present in the type system of these languages. These features include functions with exible arity, multiple assignment, functions that are overloaded on the number of return values, and the incremental evolution of record and object types. We discuss how Typed Lua handles these features and our design decisions. Finally, we present the evaluation results that we achieved while using Typed Lua to type existing Lua code.

One way to build large-scale autonomous systems is to develop an open multi-agent system using peer-to-peer architectures in which agents are not pre-engineered to work together and in which agents themselves determine the social norms that govern collective behaviour. The social norms and the agent interaction models can be described by Electronic Institutions such as those expressed in the Lightweight Coordination Calculus (LCC), a compact executable specification language based on logic programming and pi-calculus. Open multi-agent systems have experienced growing popularity in the multi-agent community and are expected to have many applications in the near future as large scale distributed systems become more widespread, e.g. in emergency response, electronic commerce and cloud computing. A major practical limitation to such systems is security, because the very openness of such systems opens the doors to adversaries for exploit existing vulnerabilities. This thesis addresses the security of open multi-agent systems governed by electronic institutions. First, the main forms of attack on open multi-agent systems are introduced and classified in the proposed attack taxonomy. Then, various security techniques from the literature are surveyed and analysed. These techniques are categorised as either prevention or detection approaches. Appropriate countermeasures to each class of attack are also suggested. A fundamental limitation of conventional security mechanisms (e.g. access control and encryption) is the inability to prevent information from being propagated. Focusing on information leakage in choreography systems using LCC, we then suggest two frameworks to detect insecure information flows: conceptual modeling of interaction models and language-based information flow analysis. A novel security-typed LCC language is proposed to address the latter approach. Both static (design-time) and dynamic (run-time) security type checking are employed to guarantee no information leakage can occur in annotated LCC interaction models. The proposed security type system is then formally evaluated by proving its properties. A limitation of both conceptual modeling and language-based frameworks is difficulty of formalising realistic policies using annotations. Finally, the proposed security-typed LCC is applied to a cloud computing configuration case study, in which virtual machine migration is managed. The secrecy of LCC interaction models for virtual machine management is analysed and information leaks are discussed.

This work considers formulation of new classes of adaptive controllers for double-integrator type systems where the underlying system parameters are uncertain and the complete state-vector is not available for feedback. Given the parameter uncertainty within the system model, a "separation principle" cannot generally be invoked towards an observer geared towards reconstruction of the full state vector using only measured variables. In this report, controllers are designed for some important sub-classes of Euler-Lagrange type mechanical systems, where states are physically interpreted as position and velocity variables, and only the position part of the state vector is available as measured output. The typical approach to obtain velocity estimates using position interpolation (also known as dirty differentiation), is known to be strongly susceptible to measurement noise and therefore does not usually represent a robust option for feedback control implementation. The proposed control scheme achieves global asymptotic stability for system dynamics subject to the condition that velocity states appear within the governing dynamics in a linear fashion. This arguably restrictive condition is loosened for the special case of scalar system with friction non-linearity as is typical within hardware implementations. The objective is to study prototypical mechanical systems with non-linearity appearing in the velocity rate equations with the eventual applications envisioned towards the attitude control problem accounting for the gyroscopic non-linearity in the Euler rotational dynamics. Based on classical certainty equivalence approaches for adaptive control, one cannot readily deal with cross terms associated with parameter estimates and unmeasured states in the Lyapunov function derivative in order to make the Lyapunov function negative definite or negative semi-definite. However, employing a new approach, this obstacle is shown in this report to be circumvented for scalar systems. In order to generalize the methodology for higher-order dynamics, a filtered state approach is used. Specifically, an auxiliary variable is introduced which plays an important role in determining restrictions on the control parameters and analyzing the stability. The proposed approach helps to overcome the uniform detectability obstacle. Additionally, this work can be applied to uncertain linear systems where independent control inputs are applied on each of the velocity state dynamics. Lastly, the solution for the scalar is applied to the rotor speed control system and is extended to the case where Coulomb friction is considered in addition to viscous friction. Since a sign function can be approximated as a hyperbolic tangent, the tanh model is used for the Coulomb friction. A controller is developed with the assumption that the coefficients of these frictions are unknown. The proposed control is then verified with Educational Control Product Model 750 Control Moment Gyroscope, and the simulation and actual test results are compared. / text

No description available.

Connotational subtyping is an approach to typing that allows an object's type to change dynamically, following changes to the object's internal state. This allows for a more precise representation of a problem domain with logical objects that have variable behavior. Two approaches to supporting connotational subtyping in the Ruby programming language were implemented: a language-level implementation using pure Ruby and a modification to the Ruby 1.8.7 interpreter. While neither implementation was wholly successful the language level implementation created complications with reflective language features like self and super and, while Ruby 1.8.7 has been obsoleted by Ruby 1.9 (YARV), the results suggest that Chambers-style, predicate-based runtime type inference could be incorporated into Ruby with only some reduced interpreter performance.

Parallelization is an important part of modern data systems. However, the non-determinism of thread scheduling introduces the difficult problem of considering all different execution orders when constructing an algorithm. Therefore deterministic-by-design concurrent systems are attractive. A new approach called LVars consists of using data which is part of a lattice, with a predefined join operation. Updates to shared data are carried out using the join operation and thus the updates commute. Together with limiting the reads of shared data, this guarantees a deterministic result. The Reactive Async framework follows a similar approach but has several aspects which can cause a non-deterministic result. The goal with this thesis is to explore how we can ammend Reactive Async in order to guarantee a deterministic result. First an exploration into the subtleties of lattice based data combined with concurrency is made. Then a formal model based on a simple object-oriented language is constructed. The constructed small-step operational semantics and type system are shown to guarantee a form of determinism. This shows that LVars-similar system can be implemented in an object-oriented setting. Furthermore the work can act as a basis for future revisions of Reactive Async and similar frameworks. / Parallellisering är en viktig del i moderna datasystem. Flertrådade applikationer innebär dock en svårighet i och med att programmerare måste ta alla exekveringsordningar i beaktning. Därför är beräkningsmodeller vars resultat är garanterat deterministiskt en attraktiv utväg. En ny modell, kallad LVars, använder gitterstrukturer tillsammans med en supremum-operation för att garantera att uppdateringar av delad data kommuterar. Detta tillsammans med begränsningar av läsning av datan garanterar ett deterministiskt resultat. Reactive Async är ett programmeringsramverk som följer en liknande strategi. Det finns dock flera delar i dess konstruktion som i en oförsiktig programmerares händer kan orsaka att ett programs resultat blir icke-deterministiskt. Målet med detta examensarbete är att utforska vilka modifikationer som skulle kunna göras av Reactive Async för att garantera determinism. Först görs en undersökning av de mer svårförståeliga delarna i kombinationen av gitterbaserad data med flertrådad exekvering. Sedan konstrueras en formell beräkningsmodell baserad på ett enkelt objektorienterat språk. Konstruktionens småstegade operationella semantik tillsammans med dess typsystem visas kunna garantera en form av determinism. Detta visar att ett system liknande LVars kan implementeras i ett objektorienterat språk. Därmed skulle detta arbete kunna ligga till grund för framtida versioner av Reactive Async.

<p dir="ltr">This thesis explores two approaches to bridge the gap between expressiveness and performance in programming languages. It presents two complementary directions that reconcile performance and expressiveness: retrofitting static performance guarantees into an expressive general-purpose language like Scala, and transparently extending a restricted language like Datalog with features like polymorphism and user-defined functions while generating specialized and efficient code.</p><p dir="ltr">We first introduce storage modes, lightweight type qualifiers that enable statically tracking the lifetime of values in Scala programs. This enables stack allocating them and reduce memory pressure on the garbage collector. A key novelty is delaying the popping of the stack frames when returning dynamically-sized stack-allocated values, overcoming limitations of previous approaches.</p><p dir="ltr">Second, we present Flan, a Datalog compiler and embedding in Scala implemented as a multi-stage interpreter. Through staging, Flan can generate highly specialized code for different execution strategies and indexing structures, achieving performance on par with state-of-the-art domain-specific compilers like Soufflé. Moreover, by leveraging the host language, Flan enables seamless extension of Datalog with powerful features like user-defined functions, lattices and polymorphism, retaining the expressiveness of languages like Flix.</p><p dir="ltr">Overall, this work advances the design space for expressive and efficient programming languages, through lightweight annotations in an expressive host language, and transparent compiler specialization of an embedded domain-specific language. The techniques intoduced bridghe the gap between low-level performance and high-level programming abstractions.</p>