Navegando por Autor "Ribeiro, Rodrigo Geraldo"
Agora exibindo 1 - 20 de 22
Resultados por página
Opções de Ordenação
Item Ambiguity and constrained polymorphism.(2016) Figueiredo, Carlos Camarão de; Figueiredo, Lucília Camarão de; Ribeiro, Rodrigo GeraldoThis paper considers the problem of ambiguity in Haskell-like languages. Overloading resolution is characterized in the context of constrained polymorphism by the presence of unreachable variables in constraints on the type of the expression. A new definition of ambiguity is presented, where existence of more than one instance for the constraints on an expression type is considered only after overloading resolution. This introduces a clear distinction between ambiguity and overloading resolution, makes ambiguity more intuitive and independent from extra concepts, such as functional dependencies, and enables more programs to type-check as fewer ambiguities arise. The paper presents a type system and a type inference algorithm that includes: a constraint-set satisfiability function, that determines whether a given set of constraints is entailed or not in a given context, focusing on issues related to decidability, a constraint-set improvement function, for filtering out constraints for which overloading has been resolved, and a context-reduction function, for reducing constraint sets according to matching instances. A standard dictionary-style semantics for core Haskell is also presented.Item Ambiguity and context-dependent overloading.(2013) Ribeiro, Rodrigo Geraldo; Figueiredo, Carlos Camarão deThis paper discusses ambiguity in the context of languages that support context-dependent overloading, such as Haskell. A type system for a Haskell-like programming language that supports context-dependent overloading and follow the Hindley-Milner approach of providing contextfree type instantiation, allows distinct derivations of the same type for ambiguous expressions. Such expressions are usually rejected by the type inference algorithm, which is thus not complete with respect to the type system. Also, Haskell’s open world approach considers a definition of ambiguity that does not conform to the existence of two or more distinct type system derivations for the same type. The article presents an alternative approach, where the standard definition of ambiguity is followed. A type system is presented that allows only context-dependent type instantiation, enabling only one type to be derivable for each expression in a given typing context: the type of an expression can be instantiated only if required by the program context where the expression occurs. We define a notion of greatest instance type for each occurrence of an expression, which is used in the definition of a standard dictionary-passing semantics for core Haskell based on type system derivations, for which coherence is trivial. Type soundness is obtained as a result of disallowing all ambiguous expressions and all expressions involving unsatisfiability in the use of overloaded names. Following the standard definition of ambiguity, satisfiability is tested—i.e., “the world is closed” —if only if overloading is (or should have been) resolved, that is, if and only if there exist unreachable variables in the constraints on types of expressions. Nowadays, satisfiability is tested in Haskell, in the presence of multiparameter type classes, only upon the presence of functional dependencies or an alternative mechanism that specifies conditions for closing the world, and that may happen when there exist or not unreachable type variables in constraints. The satisfiability trigger condition is then given automatically, by the existence of unreachable variables in constraints, and does not need to be specified by programmers, using an extra mechanism.Item An intrinsically-typed solution for the list-machine benchmark.(2022) Feitosa, Samuel da Silva; Ribeiro, Rodrigo GeraldoFormal models are important tools in the programming language research community. However, such models are full of intricacies and, due to that, they are subject to subtle errors. Such failures motivated the usage of tools to ensure the correctness of these formalisms. One way to eliminate such errors is to encode models in a dependently-typed language in order to ensure its ‘‘correctness-by-construction’’. In this paper, we use this idea to build a verified interpreter for the list-machine benchmark in the Agda programming language, comparing the results with formalizations developed by Appel et al.. We formalize the 14 tasks of the benchmark using roughly 14% of LOC compared to a Twelf solution, and 47% of LOC compared to a Coq solution, even without the use of proof automation. We also describe a solution to the second version of the benchmark and compare it with Appel’s et. al. Coq-based solution.Item Avaliação do uso de realidade mista na prática de atividades colaborativas no contexto industrial.(2020) Keller, Breno Nunes de Sena; Silva, Saul Emanuel Delabrida; Silva, Saul Emanuel Delabrida; Freire, André Pimenta; Ribeiro, Rodrigo GeraldoO processo de transição da Indústria 3.0 para 4.0 necessita que a linha de produção tenha conhecimento sobre o processo em execução e isso demanda o desenvolvimento de sistemas interconectados capazes de coletar essas informações bem como novas interfaces para interação humano-computador que permitam aos interessados interagir com estes sistemas, já que em certos contextos não é possível ou permitido uma automação completa desses processos. Portanto é necessário que pessoas sejam incluídas e sejam capazes de interagir com esses sistemas automatizados, além de terem a capacidade de tomar decisões relacionadas ao processo. Nesse contexto, os recursos de Realidade Mista se mostram como uma alternativa para inclusão de pessoas no processo, dado que permite ao usuário ter sua percepção aumentada por meio de informações provenientes do ambiente industrial. Assim sendo, o uso de recursos de Realidade Mista como ferramenta de auxílio na realização de atividades colaborativas em contexto industrial se mostra promissor. Logo, este trabalho busca avaliar como a utilização de recursos de Realidade Mista impactam na realização de atividades colaborativas no contexto da Indústria 4.0. Sendo assim, foram levantados trabalhos e ferramentas da literatura e identificadas suas limitações, além disso também foi estabelecido um contexto de teste o qual permitisse realizar uma avaliação com usuários sobre a execução de uma tarefa de inspeção de equipamento de forma colaborativa, tendo como meios de interação diferentes dispositivos \textit{handheld} e \textit{handsfree}, além do uso ou não de recursos de Realidade Mista. Como resultados, temos o desenvolvimento de uma ferramenta para interação de pessoas utilizando recursos de Realidade Mista em equipamento vestíveis, além de análises sobre a aplicação dessa ferramenta no cenário proposto em relação a outras combinações tecnológicas. Os resultados demonstram que a diferença entre os dispositivos \textit{handheld} e \textit{handsfree} e o uso ou não de recursos de Realidade Mista não é estatisticamente significativa. Demonstrando assim que todas condições avaliadas podem ser utilizadas no contexto proposto, uma vez que a diferença de performance entre as combinações não impacta na realização da tarefa. Além disso, os resultados também indicam que a aplicação desenvolvida neste trabalho tem potencial como uma ferramenta de treinamento para o contexto avaliado, uma vez que o modelo de colaboração permite o compartilhamento do conhecimento entre os usuários em um modelo mestre/aprendiz.Item Certified derivative-based parsing of regular expressions.(2018) Lopes, Raul Felipe Pimenta; Ribeiro, Rodrigo Geraldo; Figueiredo, Carlos Camarão de; Malaquias, José Romildo; Reis, Leonardo Vieira dos Santos; Ribeiro, Rodrigo GeraldoParsing is pervasive in computing and fundamental in several software artifacts. This dissertation reports the rst step in our ultimate goal: a formally veri ed toolset for parsing regular and context free languages based on derivatives. Speci cally, we describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU Grep has been developed using the certi ed algorithms. Practical experiments conducted using this tool are reported.Item Certified virtual machine-based regular expression parsing.(2019) Delfino, Thales Antônio; Ribeiro, Rodrigo Geraldo; Ribeiro, Rodrigo Geraldo; Malaquias, José Romildo; Reis, Leonardo Vieira dos SantosRegular expressions (REs) are pervasive in computing. We use REs in text editors, string search tools (like GNU-Grep) and lexical analyzers generators. Most of these tools rely on converting REs to its corresponding finite state machine or use REs derivatives for directly parse an input string. In this work, we investigated the suitability of another approach: instead of using derivatives or generating a finite state machine for a given RE, we developed a certified virtual machine-based algorithm (VM) for parsing REs, in such a way that a RE is merely a program executed by the VM over the input string. First, we developed a small-step operational semantics for the algorithm, implemented it in Haskell, tested it using QuickCheck and provided proof sketches of its correctness with respect to RE standard inductive semantics. After that, we developed a big-step operational semantics, an evolution of the small-step one. Unlike the small-step, the bigstep semantics can deal with problematic REs. We showed that the big-step semantics for our VM is also sound and complete with regard to a standard inductive semantics for REs and that the evidence produced by it denotes a valid parsing result. All of our results regarding the big-step semantics are formalized in Coq proof assistant and, from it, we extracted a certified algorithm, which we used to build a RE parsing tool using Haskell programming language. Experiments comparing the efficiency of our algorithm with another Haskell tool are reported.Item Compiling general recursive functions into finite depth pattern matching.(2023) Amaro, Maycon José Jorge; Ribeiro, Rodrigo Geraldo; Ribeiro, Rodrigo Geraldo; Vieira, Bruno Lopes; Reis, Leonardo Vieira dos SantosProgramming languages are popular and diverse, and the convenience of extending or changing the behavior of complex systems is attractive even for the systems with stringent security requirements, which often impose restrictions on the programs. A very common restriction is that the program must terminate, which is very hard to check in general because the Halting Problem is undecidable. In this work, we proposed a technique to unroll recursive programs in functional languages to create terminating versions of them. We prove that our strategy is total and we also formalize term generation and run property- based tests to build confidence that the semantics is preserved through the transformation. This strategy can be used to compile general purpose functional languages to targets such as the eBPF and smart contracts for blockchain networks.Item Formal semantics for java-like languages and research opportunities.(2018) Feitosa, Samuel da Silva; Ribeiro, Rodrigo Geraldo; Bois, André Rauber DuCurrently, Java is one of the most used programming languages, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software development. Because of that, there is a growing research field that concerns the formalization of small subsets of Java-like languages aimed to conduct studies that were impossible to achieve through informal approaches. In this context, the objective of this paper is twofold: the discussion of the state-of-the-art on Java-like semantics and the presentation of research opportunities in this area. For the first goal, we present a research about Java-like formal semantics, filtering those that provide some insights in type-safety proofs, choosing the four most cited projects to be presented in details. We also briefly present some related studies that extended the originals aggregating useful features. Additionally, we provide a comparison between the most cited projects in order to show which functionalities are covered by each one of them. As for the second goal, we discuss possible future studies that can be performed by using the presented formal semantics.Item Uma formalização da lógica modal usando o assistente de provas Coq.(2023) Silveira, Ariel Agne da; Ribeiro, Rodrigo Geraldo; Roggia, Karina Girardi; Ribeiro, Rodrigo Geraldo; Roggia, Karina Girardi; Vasconcellos, Cristiano Damiani; Reis, Leonardo Vieira dos SantosA modelagem de determinados tipos de sistemas computacionais com a lógica clássica possui fatores limitantes. Neste contexto, a apresentação de outros sistemas lógicos, como a lógica modal, e a construção de uma biblioteca para o assistente de provas Coq tem o intuito de auxiliar nesta tarefa e facilitar o uso para a verificação de propriedades de sistemas. A semântica da lógica modal é representada pela semântica dos mundos possíveis, onde existe uma relação de acessibilidade que conecta os mundos de um mo- delo. Diferentes restrições impostas na relação de acessibilidade constroem sistemas da lógica modal que auxiliam na representação de propriedades nas mais diversas áreas de estudo. O desenvolvimento da biblioteca tem como objetivo sustentar a formalização de propriedades de softwares e prová-los em Coq.Item Generating random well-typed Featherweight Java Programs using quickcheck.(2019) Feitosa, Samuel da Silva; Ribeiro, Rodrigo Geraldo; Bois, André Rauber DuCurrently, Java is one of the most used programming language, being adopted in many large projects, where applications reach a level of complexity for which manual testing and human inspection are not enough to guarantee quality in software development. Even when using automated unit tests, such tests rarely cover all interesting cases of code, which means that a bug could never be discovered, once the code is tested against the same set of rules over and over again. This paper addresses the problem of generating random well-typed programs in the context of Featherweight Java, a well-known object-oriented calculus, using QuickCheck, a Haskell library for property-based testing.Item Inference of static semantics for incomplete C programs.(2018) Melo, Leandro T. C.; Ribeiro, Rodrigo Geraldo; Araújo, Marcos Roberto de; Pereira, Fernando Magno QuintaoIncomplete source code naturally emerges in software development: during the design phase, while evolving, testing and analyzing programs. Therefore, the ability to understand partial programs is a valuable asset. However, this problem is still unsolved in the C programming language. Difficulties stem from the fact that parsing C requires, not only syntax, but also semantic information. Furthermore, inferring types so that they respect C’s type system is a challenging task. In this paper we present a technique that lets us solve these problems. We provide a unification-based type inference capable of dealing with C intricacies. The ideas we present let us reconstruct partial C programs into complete well-typed ones. Such program reconstruction has several applications: enabling static analysis tools in scenarios where software components may be absent; improving static analysis tools that do not rely on build-specifications; allowing stub-generation and testing tools to work on snippets; and assisting programmers on the extraction of reusable data-structures out of the program parts that use them. Our evaluation is performed on source code from a variety of C libraries such as GNU’s Coreutils, GNULib, GNOME’s GLib, and GDSL; on implementations from Sedgewick’s books; and on snippets from popular open-source projects like CPython, FreeBSD, and Git.Item MASLAB : um software interativo de simulação para apoio no ensino de modelagem e análise de sistemas lineares.(2022) Aguiar, Italo Almeida; Ribeiro, Rodrigo Geraldo; Ricco, Rodrigo Augusto; Ribeiro, Rodrigo Geraldo; Ricco, Rodrigo Augusto; Silva, Saul Emanuel Delabrida; Reis, Leonardo Vieira dos SantosSimulações aplicadas no contexto educacional são capazes de prover um considerável apoio no processo de aprendizado de determinada área de conhecimento. Este traba- lho propõe o desenvolvimento de um software de simulação interativo, gratuito e de código aberto para uso educacional no contexto da disciplina de Modelagem e Análise de Sistemas Lineares, nomeado MASLAB. Dentro do escopo da disciplina, MASLAB é capaz de compor e simular graficamente, dentro do escopo da disciplina, variações de cenários definidos pelos usuários, seja por visualização em tempo real ou por visuali- zação de um instante específico. Como forma se de testar as saídas do simulador, a metodologia de validação se propôs a replicar um experimento real por meio de dados previamente amostrados, de modo a se buscar uma proximidade relativa aos dados do experimento original. Por fim, são apresentados os resultados obtidos na replicação vir- tual do experimento real e a análise da proximidade esperada dos resultados obtidos no simulador.Item Mechanized metatheory for a λ-calculus with trust types.(2013) Ribeiro, Rodrigo Geraldo; Figueiredo, Lucília Camarão de; Figueiredo, Carlos Camarão deAs computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a λ-calculus with trust types, originally formulated by Ørbæk and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.Item A mechanized proof of a textbook type unification algorithm.(2020) Amaro, Maycon José Jorge; Ribeiro, Rodrigo Geraldo; Bois, André Rauber DuUnification is the core of type inference algorithms for modern functional programming languages, like Haskell and SML. As a first step towards a formalization of a type inference algorithm for such programming languages, we present a formalization in Coq of a type unification algorithm that follows classic algorithms presented in programming language textbooks. We also report on the use of such formalization to build a correct type inference algorithm for the simply typed λ-calculus.Item Modelos evolutivos para composição algorítmica afetiva.(2022) Santos, Carla Sanches Nere dos; Freitas, Alan Robert Resende de; Freitas, Alan Robert Resende de; Ribeiro, Rodrigo Geraldo; Barbosa, Rogério VasconcelosSistemas de Composição Algorítmica Afetiva buscam gerar músicas que expressam ou provocam emoções. Ainda se encontra em aberto a composição de melodias que passam todos os sentimentos presentes nos modelos emocionais. Esses sistemas podem ser utilizados em diferentes contextos, como saúde e entretenimento. Assim, pessoas podem se expressar através da música ou ter experiências de maior imersão em jogos ou filmes. Este trabalho visa identificar estratégias para realizar múltiplas transformações afetivas em melodias, de modo a passar emoções para o ouvinte. São propostos dois algoritmos transformativos: um modelo evolutivo mono-objetivo e outro multiob- jetivo, baseado no algoritmo Non-dominated Sorting Genetic Algorithm II (NSGA-II). Os resultados mostram que os dois modelos geraram melodias que passam emoções positivas e negativas. O modelo multiobjetivo alcançou melhores resultados do que o mono-objetivo. No entanto, é preciso analisar estratégias para melhorar a qualidade das melodias e alcançar mais emoções.Item Realidade aumentada aplicada à redução de riscos na segurança do trabalho em subestações elétricas.(2021) Rocha, Victor Menezes; Silva, Saul Emanuel Delabrida; Silva, Saul Emanuel Delabrida; Oliveira, Ricardo Augusto Rabelo; Ribeiro, Rodrigo Geraldo; Silva, Rone Ilidio daAs atividades que envolvem energia elétrica estão inseridas entre as mais perigosas e mais danosas ao trabalhador que as desempenham. Assim, o objetivo geral desse trabalho consiste em desenvolver uma aplicação da tecnologia de realidade aumentada móvel como meio de orientação de acesso e instruções de segurança junto a operadores/mantenedores de subestações elétricas. Para tanto, inicialmente, foi modelada uma subestação elétrica simplificada em 3D para experimentação em realidade virtual e, assim, avaliar a experiência do usuário quanto ao uso do protótipo e definir quais são os principais requisitos que podem ser utilizados para construção da aplicação final. A partir dos resultados obtidos, foi projetado em realidade virtual o arranjo físico e os equipamentos de uma subestação elétrica industrial do Terminal Marítimo de Ponta da Madeira (São Luís-MA). Em seguida, foi desenvolvido um protótipo de realidade aumentada usando o Unity 3D e o Vulforia para a plataforma Android. Este aplicativo permite ler tags instaladas nos equipamentos da subestação e faz a identificação dos EPIs recomendados, da distância segura para trabalho e exibe os principais parâmetros dos painéis elétricos (diagramas unifilares detalhados, corrente de curto circuito, tensão elétrica, entre outros).Item Terminating constraint set satisfiability and simplification algorithms for context-dependent overloading.(2013) Ribeiro, Rodrigo Geraldo; Figueiredo, Carlos Camarão de; Figueiredo, Lucília Camarão deAlgorithms for constraint set satisfiability and simplification of Haskell type class constraints are used during type inference in order to allow the inference of more accurate types and to detect ambiguity. Unfortunately, both constraint set satisfiability and simplification are in general undecidable, and the use of these algorithms may cause nontermination of type inference. This paper presents algorithms for these problems that terminate on any given input, based on the use of a criterion that is tested on each recursive step. The use of this criterion eliminates the need of imposing syntactic conditions on Haskell type class and instance declarations in order to guarantee termination of type inference in the presence of multi-parameter type classes, and allows program compilation without the need of compiler flags for lifting such restrictions. Undecidability of the problems implies the existence of instances for which the algorithm incorrectly reports unsatisfiability, but we are not aware of any practical example where this occurs.Item The design of a verified derivative-based parsing tool for regular expressions.(2021) Cardoso, Elton Máximo; Amaro, Maycon José Jorge; Feitosa, Samuel da Silva; Reis, Leonardo Vieira dos Santos; Bois, André Rauber Du; Ribeiro, Rodrigo GeraldoWe describe the formalization of Brzozowski and Antimirov derivative based algorithms for regular expression parsing, in the dependently typed language Agda. The formalization produces a proof that either an input string matches a given regular expression or that no matching exists. A tool for regular expression based search in the style of the well known GNU grep has been developed with the certified algorithms. Practical experiments conducted with this tool are reported.Item Towards an extrinsic formalization of featherweight Java in Agda.(2020) Feitosa, Samuel da Silva; Ribeiro, Rodrigo Geraldo; Bois, André Rauber DuFeatherweight Java is one of the most popular calculi which specify object-oriented programming features. It has been used as the basis for investigating novel language functionalities, as well as to specify and understand the formal properties of existing features for languages in this paradigm. However, when considering mechanized formalization, it is hard to find an implementation for languages with complex structures and binding mechanisms as Featherweight Java. In this paper we formalize Featherweight Java, implementing the static and dynamic semantics in Agda, and proving the main safety properties for this calculus.Item Type inference for C : applications to the static analysis of incomplete programs.(2020) Melo, Leandro T. C.; Ribeiro, Rodrigo Geraldo; Guimarães, Breno Campos Ferreira; Pereira, Fernando Magno QuintaoType inference is a feature that is common to a variety of programming languages. While, in the past, it has been prominently present in functional ones (e.g., ML and Haskell), today, many object-oriented/ multi-paradigm languages such as C# and C++ offer, to a certain extent, such a feature. Nevertheless, type inference still is an unexplored subject in the realm of C. In particular, it remains open whether it is possible to devise a technique that encompasses the idiosyncrasies of this language. The first difficulty encountered when tackling this problem is that parsing C requires, not only syntactic, but also semantic information. Yet, greater challenges emerge due to C’s intricate type system. In this work, we present a unification-based framework that lets us infer the missing struct, union, enum, and typedef declarations in a program. As an application of our technique, we investigate the reconstruction of partial programs. Incomplete source code naturally appears in software development: during design and while evolving, testing, and analyzing programs; therefore, understanding it is a valuable asset. With a reconstructed well-typed program, one can: (i) enable static analysis tools in scenarios where components are absent; (ii) improve precision of “zero setup” static analysis tools; (iii) apply stub generators, symbolic executors, and testing tools on code snippets; and (iv) provide engineers with an assortment of compilable benchmarks for performance and correctness validation. We evaluate our technique on code from a variety of C libraries, including GNU’s Coreutils and on snippets from popular projects such as CPython, FreeBSD, and Git.