Margrave is a specification language and analysis tool for access control policies with semantics based in order-sorted logic. The clear logical roots of Margrave's semantics makes policies specified in the Margrave language both machine analyzable and relatively easy for users to reason about. However, the decision conflict resolution declaration and policy set features of Margrave do not have semantics that are as cleanly rooted in order-sorted logic as Margrave policies and queries are. Additionally, the current semantics of decision conflict resolution declarations and of policy sets do not permit users to take full advantage of the multi-decision capabilities of Margrave policies. The purposes of this thesis are (i) to provide a unified extension to the semantics for policies and policy combination, (ii) to cleanly support decision conflict resolution mechanisms in a general way within those semantics and (iii) to provide insight into the properties of policy combination and decision conflict resolution for multi-decision policies in general. These goals are achieved via the realization that policy combinators may be treated as policies operating within environments extended with the results of the policies to be combined, allowing policy combinators to be defined as if they were policies. The ability to treat policy combinators as policies means that users' current understanding of policies can be easily extended to policy combinators. Additionally, the tools that Margrave has for supporting policies can be leveraged as the Margrave language and analysis tool grow to provide fuller support for policy combination and rule conflict resolution declarations.

[pt] Este trabalho descreve uma nova linguagem de programação funcional e sua implementação. Sloth é uma linguagem funcional pura interpretada, não estrita, que suporta funções de ordem elevada como valores de primeira classe, tipos de dados estruturados e definições múltiplas de funções selecionadas por casamento de padrões. Sloth foi criada para o uso no meio acadêmico, em atividades relacionadas ao uso e à  implementação de linguagens funcionais. Sendo assim, durante o desenvolvimento de Sloth, uma grande preocupação com a simplicidade direcionou tanto a especificação da linguagem quanto sua implementação. Como resultado, a sintaxe da linguagem é modesta, mas expressiva o bastante para permitir seu uso em aplicações práticas. Da mesma forma, a grande simplicidade e portabilidade de sua implementação não prejudicam severamente sua eficiência. As principais contribuições do trabalho são o projeto e desenvolvimento de Sloth, uma otimização à  redução de grafos combinatórios como alternativa ao uso dos combinadores de Turner, uma arquitetura inovadora para a implementação de linguagens funcionais interpretadas, baseada no uso cooperativo de duas linguagens de programação, e uma análise comparativa entre a eficiência de Sloth e outras linguagens semelhantes. / [en] This work describes a new functional programming language and its implementation. Sloth is a non-strict purely functional interpreted programming language, which supports high order functions as first class values, structured data types, and pattern-matching based function definitions. Sloth was created for academical use in activities related to the use and to the implementation of functional programming languages. Therefore, there has been a great concern with the simplicity of both the language specification and its implementation. As a result, Sloth's syntax is modest, but expressive enough for practical applications. Furthermore, the great simplicity and portability of its implementation has no serious impact on its performance. The main contributions of this work are the design and implementation of Sloth, an optimization to combinator graph reduction as an alternative to the use of Turner combinators, a new architecture for the implementation of interpreted functional programming languages, based on the cooperation between two programming languages, and the performance comparison between Sloth and similar languages.

A domain-specific embedded language (DSEL) is a domain-specific programming language with no concrete syntax of its own. Defined as a set of combinators encapsulated in a module, it borrows the syntax and tools (such as type-checkers and compilers) of its host language; hence it is economical to design, introduce, and maintain. Unfortunately, this economy is counterbalanced by a lack of room for growth. DSELs cannot match sophisticated domain-specific languages that offer tools for domainspecific error-checking and optimisation. These tools are usually based on syntactic analyses, so they do not work on DSELs. Abstract interpretation is a technique ideally suited to the analysis of DSELs, due to its semantic, rather than syntactic, approach. It is based upon the observation that analysing a program is equivalent to evaluating it over an abstract semantic domain. The mathematical properties of the abstract domain are such that evaluation reduces to solving a mutually recursive set of equations. This dissertation shows how abstract interpretation can be applied to a DSEL by replacing it with an abstract implementation of the same interface; evaluating a program with the abstract implementation yields an analysis result, rather than an executable. The abstract interpretation of DSELs provides a foundation upon which to build sophisticated error-checking and optimisation tools. This is illustrated with three examples: an alphabet analyser for CSP, an ambiguity test for parser combinators, and a definedness test for attribute grammars. Of these, the ambiguity test for parser combinators is probably the most important example, due to the prominence of parser combinators and their rather conspicuous lack of support for the well-known LL(k) test. In this dissertation, DSELs and their signatures are encoded using the polymorphic lambda calculus. This allows the correctness of the abstract interpretation of DSELs to be proved using the parametricity theorem: safety is derived for free from the polymorphic type of a program. Crucially, parametricity also solves a problem commonly encountered by other analysis methods: it ensures the correctness of the approach in the presence of higher-order functions.