Na última década muitos esforços têm sido feitos em verificação formal de propriedades de agentes do cálculo-π. Uma dessas propriedades é a equivalência observacional, que serve para determinar se um processo é equivalente a sua especificação. Contudo, a verificação de equivalência observacional não é um problema trivial. A maioria dos algoritmos destinados a verificação de equivalência são baseados na construção de sistemas de transições rotuladas (π-autômatos). O principal problema com essa abordagem é o grande número de estados envolvidos podendo chegar a um número infinito. Montanari e Pistore mostram que é possível gerar π-autômatos finitos para agentes-π e é possível reduzir a quantidade de estados desses π-autômatos, através da identificação dos nomes ativos. Um nome é semanticamente ativo em um agente se ele pode ser executado de forma observável por ele. Este é um trabalho de análise estática, que tem por objetivo coletar os possíveis nomes ativos contidos em expressões-π, utilizando para isso um sistema de tipos. A vantagem da utilização de sistemas de tipos em relação a outras formas de análise estática é que sistemas de tipos são sistemas lógicos, logo as técnicas de prova da lógica podem ser aproveitadas no estudo de propriedades de sistemas de tipos. Além disso sistemas de tipos são definidos através da estrutura sintática de expressões, facilitando assim as provas por indução estrutural. Assim a principal contribuição deste trabalho é a elaboração do Active-Base-π, um sistema de tipos para a coleta de nomes ativos de expressões-π.

BASTOS, Antonio Josefran de Oliveira. Sequências convergentes de estruturas discretas e testabilidade. 2012. 62 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-08T18:57:48Z No. of bitstreams: 1 2007_dis_adbnogueira.pdf: 13756193 bytes, checksum: bb4a338bd2622ad6f90479ce37824ccd (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-13T13:31:42Z (GMT) No. of bitstreams: 1 2007_dis_adbnogueira.pdf: 13756193 bytes, checksum: bb4a338bd2622ad6f90479ce37824ccd (MD5) / Made available in DSpace on 2016-07-13T13:31:42Z (GMT). No. of bitstreams: 1 2007_dis_adbnogueira.pdf: 13756193 bytes, checksum: bb4a338bd2622ad6f90479ce37824ccd (MD5) Previous issue date: 2012 / In this work, we studied the recent theory of convergent graph sequences and its extensions to permutation and partially ordered sets with fix dimension. We’ve conjectured a lemma of weak regularity on intervals that, if this conjecture is true, we can extend this theory to ordered graphs, which are graphs such that there is a total order on its vertices. We show some interesting relations on permutation and partially ordered sets with ordered graphs. Then, we obtain another proof to the existence of limit objects for all convergent permutation sequences. We also proved that all hereditary property of either permutation or ordered graph is testable. / Neste trabalho, estudamos a teoria recente de convergência de sequências de grafos e suas extensões para permutações e ordens parciais de dimensão fixa. Conjecturamos um lema de regularidade fraca de grafos em intervalos que, se for verdadeira, nos possibilita estender essa teoria para grafos ordenados, que são grafos tais que existe uma ordem total entre os vértices. Mostramos algumas relações interessantes de permutações e ordens parciais com grafos ordenados. Com isso, conseguimos uma prova alternativa para a existência de objetos limites de qualquer sequência convergente de permutações. Provamos também que toda propriedade hereditária de permutações ou grafos ordenados é testável.

DANTAS, Allberson Bruno de Oliveira. Certificação de componentes em uma plataforma de nuvens computacionais para serviços de computação de alto desempenho. 2017. 214 f. Tese (Doutorado em Ciência da Computação)-Universidade Federal do Ceará, Fortaleza, 2017. / Submitted by Gláucia Helena da Silveira Mota (glaucia@lia.ufc.br) on 2017-10-23T17:57:00Z No. of bitstreams: 1 2017_tese_abodantas.pdf: 3345763 bytes, checksum: 7d9c19651fdf5919fcc10ab432a72eeb (MD5) / Approved for entry into archive by Jairo Viana (jairo@ufc.br) on 2017-11-03T16:48:46Z (GMT) No. of bitstreams: 1 2017_tese_abodantas.pdf: 3345763 bytes, checksum: 7d9c19651fdf5919fcc10ab432a72eeb (MD5) / Made available in DSpace on 2017-11-03T16:48:46Z (GMT). No. of bitstreams: 1 2017_tese_abodantas.pdf: 3345763 bytes, checksum: 7d9c19651fdf5919fcc10ab432a72eeb (MD5) Previous issue date: 2017 / The development of correct and safe High Performance Computing (HPC) applications is a challenge for developers, since such applications generally use parallelism and run on heterogeneous parallel computing platforms. The Doctoral Thesis proposed in this document is aimed at presenting an architecture of a component certification mechanism for cloud computing platforms of high performance computing services. In particular, this mechanism is proposed within the context of the HPC Shelf platform, allowing the construction of certified components for functional and non-functional properties, which can be used to compose applications for expert users. Two particular certifier components are proposed using the certification mechanism introduced in this Thesis: SWC2 (Scientific Workflow Certifier Component) e C4 (Computation Component Certifier Component). SWC2 components are used to verify formal properties of workflows in HPC Shelf. In turn, C4 components are employed to verify formal properties on computation components. There are still tactical components, which expose the services of software formal verification infrastructures and can be orchestrated, by certifiers, by means of the TCOL (Tactical Component Orchestration Language) language, also proposed in this work. It is expected to contribute to the state-of-the-art in the following points: in cloud computing, by providing the first cloud infrastructure focused on software formal verification using exclusively high performance computing techniques; in component-oriented platforms, by providing nondisruptive components that can certify others in a reflexive way; enabling the creation of the so-called parallel certification systems, which are formed by the orchestration of provers to verify formal properties; in scientific workflows, by extracting the main verifiable patterns in these workflows; and in high performance computing applications, by providing a study on which software formal verification tools are able to verify their properties. / O desenvolvimento de aplicações de Computação de Alto Desempenho (CAD) corretas e seguras é um desafio para desenvolvedores, uma vez que tais aplicações geralmente utilizam paralelismo e executam em plataformas heterogêneas de computação paralela. A Tese de Doutorado proposta neste documento dispõe-se a apresentar a arquitetura de um mecanismo de certificação de componentes para plataformas de nuvens computacionais de serviços de computação de alto desempenho. Em particular, esse mecanismo é proposto no contexto da plataforma HPC Shelf, permitindo a construção de componentes certificados quanto a propriedades funcionais e não funcionais, os quais podem ser utilizados para compor aplicações para usuários especialistas. Dois componentes certificadores particulares são propostos utilizando o mecanismo de certificação introduzido na Tese: SWC2 (Scientific Workflow Certifier Component) e C4 (Computation Component Certifier Component). Componentes SWC2 são utilizados para verificar propriedades formais em workflows na HPC Shelf. Já os componentes C4 são empregados para verificar propriedades formais em componentes de computação. Existem ainda componentes táticos, que expõem serviços de infraestruturas de verificação formal de software e podem ser orquestrados, por certificadores, através da linguagem TCOL (Tactical Component Orchestration Language), também proposta nesse trabalho. Espera-se contribuir com o estado da arte nos seguintes pontos: em nuvens computacionais, fornecendo a primeira infraestrutura em nuvem voltada à verificação formal de software utilizando exclusivamente técnicas de CAD; em plataformas orientadas a componentes, provendo componentes não disruptivos que podem certificar outros de forma reflexiva; possibilitando a criação dos chamados sistemas de certificação paralela, os quais são formados por orquestrações de provadores para verificar propriedades formais; em workflows científicos, extraindo os principais padrões verificáveis desses workflows; e em aplicações de CAD, fornecendo um estudo sobre quais ferramentas de verificação formal de software se aplicam na verificação de suas propriedades.

BASTOS, Antonio Josefran de Oliveira. Sequências Convergentes de Estruturas Discretas e Testabilidade. 2012. 47 f. : Dissertação (mestrado) - Universidade Federal do Ceará, Centro de Ciências, Departamento de Computação, Fortaleza-CE, 2012. / Submitted by guaracy araujo (guaraa3355@gmail.com) on 2016-05-31T19:31:54Z No. of bitstreams: 1 2012_dis_ajobastos.pdf: 836578 bytes, checksum: 7267190dcdfd4c22a13a8a661fa593b4 (MD5) / Approved for entry into archive by guaracy araujo (guaraa3355@gmail.com) on 2016-05-31T19:32:46Z (GMT) No. of bitstreams: 1 2012_dis_ajobastos.pdf: 836578 bytes, checksum: 7267190dcdfd4c22a13a8a661fa593b4 (MD5) / Made available in DSpace on 2016-05-31T19:32:46Z (GMT). No. of bitstreams: 1 2012_dis_ajobastos.pdf: 836578 bytes, checksum: 7267190dcdfd4c22a13a8a661fa593b4 (MD5) Previous issue date: 2012 / In this work, we studied the recent theory of convergent graph sequences and its extensions to permutation and partially ordered sets with fix dimension. We’ve conjectured a lemma of weak regularity on intervals that, if this conjecture is true, we can extend this theory to ordered graphs, which are graphs such that there is a total order on its vertices. We show some interesting relations on permutation and partially ordered sets with ordered graphs. Then, we obtain another proof to the existence of limit objects for all convergent permutation sequences. We also proved that all hereditary property of either permutation or ordered graph is testable. / Neste trabalho, estudamos a teoria recente de convergência de sequências de grafos e suas extensões para permutações e ordens parciais de dimensão fixa. Conjecturamos um lema de regularidade fraca de grafos em intervalos que, se for verdadeira, nos possibilita estender essa teoria para grafos ordenados, que são grafos tais que existe uma ordem total entre os vértices. Mostramos algumas relações interessantes de permutações e ordens parciais com grafos ordenados. Com isso, conseguimos uma prova alternativa para a existência de objetos limites de qualquer sequência convergente de permutações. Provamos também que toda propriedade hereditária de permutações ou grafos ordenados é testável.

Made available in DSpace on 2016-08-29T15:32:27Z (GMT). No. of bitstreams: 1 tese_2723_DissertacaoMestradoWesleyLucasBreda.pdf: 2352402 bytes, checksum: ea4443a2c6595a096d1b34f4d81fb874 (MD5) Previous issue date: 2008-02-22 / Esta dissertação apresenta uma proposta de tradução automática baseada em conhecimento, o projeto e a implementação de um sistema de autoria e uso de tradutores automatizados para apoio à tradução, tendo como estudo de caso a tradução de Português para Libras. Esse sistema possui um ambiente para manipulação dos elementos utilizados no processo de tradução automática e um para tradução automática de textos de uma língua-fonte, em forma de texto, para uma língua-alvo, em forma de texto, vídeo e/ou áudio. Os elementos utilizados no processo de tradução são exemplos de tradução da língua-fonte para a língua-alvo e regras de tradução inferidas considerando esses mesmos exemplos. Para isso, o conteúdo deste trabalho apresenta um estudo sobre tradução automática, apontando seus métodos e, brevemente, seus principais paradigmas, além de uma breve exposição sobre memória de tradução. Apresenta também um estudo sobre a definição de linguagens formais e inferência gramatical, apontando seus métodos e, brevemente, a especificação de problemas de inferência gramatical. Apresenta ainda os algoritmos de tradução e de inferência utilizados pelo sistema, bem como as estruturas de dados necessárias e resultados gerados por eles. Ao longo de todo o conteúdo, é possível observar alguns aspectos de usabilidade, navegabilidade, funcionalidade e complexidade do sistema gerado como produto final deste trabalho, um ambiente de apoio à tradução, baseado em exemplos e sintaxe.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Letras, Departamento de Linguística, Português e Línguas Clássicas, Programa de Pós-Graduação em Linguística, 2013. / Submitted by Luiza Silva Almeida (luizaalmeida@bce.unb.br) on 2013-07-29T18:14:36Z No. of bitstreams: 1 2013_JulianaBatistadoPrado.pdf: 789851 bytes, checksum: b43b7d7b2b8693629ffa0baaf334ddae (MD5) / Approved for entry into archive by Leandro Silva Borges(leandroborges@bce.unb.br) on 2013-07-29T20:21:02Z (GMT) No. of bitstreams: 1 2013_JulianaBatistadoPrado.pdf: 789851 bytes, checksum: b43b7d7b2b8693629ffa0baaf334ddae (MD5) / Made available in DSpace on 2013-07-29T20:21:02Z (GMT). No. of bitstreams: 1 2013_JulianaBatistadoPrado.pdf: 789851 bytes, checksum: b43b7d7b2b8693629ffa0baaf334ddae (MD5) / Este estudo trata da variação das formas de tratamento da segunda pessoa do discurso no contexto do Tribunal do Júri. O Tribunal do Júri caracteriza-se como instituição em que predomina a adoção do estilo formal de linguagem por parte das pessoas que nele atuam. Por essa razão, procurou-se investigar o uso das formas de tratamento com a segunda pessoa do discurso nesse contexto. A pesquisa situa-se no quadro da Sociolinguística Interacional, com contribuições da Pragmática. Metodologicamente, utiliza-se das técnicas de transcrição da Análise da Conversação e de orientações etnográficas para condução da abordagem qualitativa dos dados. O corpus da dissertação constitui-se de aproximadamente oito horas de gravação em vídeo de uma sessão do Tribunal do Júri e de uma hora em áudio, correspondente à entrevista concedida pelo juiz que presidiu a sessão sob análise. Como resultados de pesquisa, identificaram-se as formas de tratamento utilizadas durante a sessão analisada: senhor/senhora, senhores, você/cê, vocês, seu, doutor, Excelência e Vossas Excelências. Constatou-se também a ocorrência de alternância no uso dessas formas na interlocução com a segunda pessoa do discurso e revelou-se que a variação senhor/senhora; doutor e você e cê no contexto pesquisado manifesta-se em um contínuo estilístico mais ou menos alinhado a um quadro de formalidade. O significado social do uso das formas você e cê, utilizadas pelos profissionais do Direito durante a inquirição das testemunhas, representa estratégia de intimidação dessas com fins de obter confissões ou consentimentos. As análises demonstraram que a formalidade é contextualmente situada, pois a seleção das formas você e cê não sinalizou enquadre de intimidade entre os interagentes, o que na perspectiva de Irvine (1984) caracterizaria uma situação de informalidade. Diferentemente, nesse contexto, os interagentes mantiveram distanciamento social e relacionamento assimétrico mesmo quando adotavam tratamento menos cerimonioso. Espera-se que os resultados dessa análise interacional possam contribuir para o desenvolvimento teórico de estudos da interação em contextos institucionais, assim também como para melhor compreensão quanto ao uso das formas de tratamento utilizadas no Brasil. _______________________________________________________________________________________ ABSTRACT / This study concerns a research about treatment forms of second person speech in the context of the jury’s trial. The jury’s trial is characterized as an institution that predominates the formal style of language. In this way, this study tried to investigate the use of treatment forms with the second person speech in this context. The research is situated within the Interactional Sociolinguistics, with contributions of Pragmatics. As a methodological source, it was used the techniques of transcription Conversational Analysis and guidelines for conducting ethnographic qualitative approach. The corpus of the research consists in approximately eight hours of video recording of a session of the jury’s trial and one hour audio, corresponding to an interview by the judge who presided the session. As search results, were identified the types of treatment used during the session focused: senhor/senhora, senhores, você/cê, vocês, seu, doutor, Excelência and Vossas Excelências. It Was found also the occurrence of alternation in the use of these forms in communication with the second-person speech and revealed that the variation senhor/senhora and você/cê in the context manifests itself in a more continuous stylistic or less aligned to a frame of formality. The social meaning of the forms você and cê, used by legal professionals during the investigation of witnesses, was interpreted as a strategy of intimidation these purpose of extracting confessions or consents. The analyzes showed that the formality is contextually situated, for the selection of forms você and cê not signaled frame of intimacy among interactings, which in Irvine’s view (1984) characterize a situation of informality. In contrast, in this context, interactings kept social distancing and asymmetrical relationship even when they adopted less ceremonious treatment. It is expected that the results of this analysis interaction may contribute to the development of theoretical studies of the interaction in institutional contexts, so to better understand how the use of treatment modalities is in Brazil.

Na última década muitos esforços têm sido feitos em verificação formal de propriedades de agentes do cálculo-π. Uma dessas propriedades é a equivalência observacional, que serve para determinar se um processo é equivalente a sua especificação. Contudo, a verificação de equivalência observacional não é um problema trivial. A maioria dos algoritmos destinados a verificação de equivalência são baseados na construção de sistemas de transições rotuladas (π-autômatos). O principal problema com essa abordagem é o grande número de estados envolvidos podendo chegar a um número infinito. Montanari e Pistore mostram que é possível gerar π-autômatos finitos para agentes-π e é possível reduzir a quantidade de estados desses π-autômatos, através da identificação dos nomes ativos. Um nome é semanticamente ativo em um agente se ele pode ser executado de forma observável por ele. Este é um trabalho de análise estática, que tem por objetivo coletar os possíveis nomes ativos contidos em expressões-π, utilizando para isso um sistema de tipos. A vantagem da utilização de sistemas de tipos em relação a outras formas de análise estática é que sistemas de tipos são sistemas lógicos, logo as técnicas de prova da lógica podem ser aproveitadas no estudo de propriedades de sistemas de tipos. Além disso sistemas de tipos são definidos através da estrutura sintática de expressões, facilitando assim as provas por indução estrutural. Assim a principal contribuição deste trabalho é a elaboração do Active-Base-π, um sistema de tipos para a coleta de nomes ativos de expressões-π.

Tese (doutorado)—Universidade de Brasília, Faculdade de Ciência da Informação, Programa de Pós-Graduação em Ciência da Informação, 2015. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2016-01-25T15:17:04Z No. of bitstreams: 1 2015_LauroCesarAraujo.pdf: 14597557 bytes, checksum: d2a60d9b4cea4d03cede2f2768669396 (MD5) / Approved for entry into archive by Patrícia Nunes da Silva(patricia@bce.unb.br) on 2016-01-25T16:01:48Z (GMT) No. of bitstreams: 1 2015_LauroCesarAraujo.pdf: 14597557 bytes, checksum: d2a60d9b4cea4d03cede2f2768669396 (MD5) / Made available in DSpace on 2016-01-25T16:01:48Z (GMT). No. of bitstreams: 1 2015_LauroCesarAraujo.pdf: 14597557 bytes, checksum: d2a60d9b4cea4d03cede2f2768669396 (MD5) / Esta pesquisa propõe a arquitetura da informação de uma linguagem formal textual para representar discursos sobre entidades ontológicas e obter deduções a respeito de ontologias de domínio. Por meio do paradigma de metamodelagem, a linguagem permite tratamento de ontologias heterogêneas que podem ser descritas como instâncias de uma ou mais ontologias de fundamentação. A linguagem suporta comportamentos clássicos e modais sustentados por noções de prova baseadas no paradigma de Programação em Lógica (Modal). O arcabouço modal desenvolvido possibilita que diferentes interpretações modais sejam introduzidas às especificações das ontologias, e contempla especialmente sistemas baseados em lógicas de múltiplos agentes. Uma sistematização do fragmento endurante da Unified Foundational Ontology (UFO) é realizada com objetivo de compor parte do marco teórico que fundamenta a proposta e de servir de exemplo de instanciação do arcabouço desenvolvido. Como resultados complementares, destacam-se: uma sistematização de um conjunto ampliado de regras para produção de modelos conceituais e um glossário detalhado de termos e conceitos da UFO-A; protótipos funcionais que implementam os sistemas elaborados; traduções das teorias descritas no arcabouço proposto para linguagens visuais, como extensões da representação gráfica da OntoUML; e discussões a respeito da integração de Arquitetura da Informação, Modelagem Conceitual e Programação em Lógica (Modal) no contexto social aplicado. / This research proposes the information architecture of a textual formal language to represent and reason about ontological entities based on foundational ontologies. Through metamodeling, the language is able to deal with heterogeneous ontologies that can be described as instances of one or more foundational ontology. The language provides classic and modal inference mechanisms supported by proof notions based on the (Modal) Logic Programming paradigm. The modalities introduced by the modal framework allow a wide range of interpretations, including multi-agent systems. A systematization of the endurant fragment of the Unified Foundational Ontology (UFO) is produced in order to compose part of the theoretical framework underlying the proposal, and to serve as an example instantiating the developed framework. As complementary results we highlight: a systematization of an extended set of rules for conceptual modeling and a detailed glossary of terms and concepts of UFO-A; functional prototypes implementing the developed systems; translations of the theories described as instances of the framework to diagramatic representations, as extensions of the OntoUML visual language; and discussions regarding the integration of Information Architecture, Conceptual Modeling and Logic Programming within Applied Social Science.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Letras, Departamento de Linguística, Português e Línguas Clássicas, Programa de Pós-Graduação em Linguística, 2018. / Submitted by Fabiana Santos (fabianacamargo@bce.unb.br) on 2018-08-22T19:17:25Z No. of bitstreams: 1 2018_RosaniKristineParaísoGarcia.pdf: 2789550 bytes, checksum: a0492b8e4403e5caca30e09c36a2fa26 (MD5) / Approved for entry into archive by Raquel Viana (raquelviana@bce.unb.br) on 2018-08-27T20:04:59Z (GMT) No. of bitstreams: 1 2018_RosaniKristineParaísoGarcia.pdf: 2789550 bytes, checksum: a0492b8e4403e5caca30e09c36a2fa26 (MD5) / Made available in DSpace on 2018-08-27T20:04:59Z (GMT). No. of bitstreams: 1 2018_RosaniKristineParaísoGarcia.pdf: 2789550 bytes, checksum: a0492b8e4403e5caca30e09c36a2fa26 (MD5) Previous issue date: 2018-08-22 / Este estudo versa sobre a expressão da polidez na Língua de Sinais Brasileira (Libras ou LSB) e desenvolve-se pela análise de dados coletados em comunidade surda usuária de Libras. Assim como em qualquer língua, nas línguas de sinais há o uso de diferentes registros e “graus” de polidez. O objetivo geral do estudo é analisar os elementos linguísticos utilizados como recursos na expressão gramatical da polidez em Libras, tomando como ponto de partida o trabalho pioneiro de Brown e Levinson (1987 [1978]) e um capítulo que Ferreira Brito (1995) desenvolve sobre esse assunto. Como se trata de um tema que está na interface entre a gramática e o discurso, a abordagem teórica leva em conta categorias de análise de base funcionalista, mas trabalha, também, com pressupostos da gramática gerativa, quanto à existência de uma faculdade da linguagem e de mecanismos gramaticais universais para a expressão do pensamento. O caminho metodológico adotado para esta pesquisa baseia-se em coleta de dados, por meio de filmagens em vídeo e de entrevistas, a fim de comparar os diferentes mecanismos gramaticais utilizados pelos surdos sinalizantes de Libras e analisar esses mecanismos com base no referencial teórico adotado. A análise dos dados permitiu identificar que os surdos participantes da pesquisa relacionam os registros formais e informais com o comportamento mais (ou menos) polido dos interlocutores, sendo a estrutura diretiva a preferida tanto em situações formais quanto em situações informais. Essa característica se revelou ser própria da Libras – confirmando-se a proposta de Ferreira Brito (1995) de que a familiaridade é um aspecto fundamental para a descrição da polidez nessa língua, e desafiando-se a teoria de Brown e Levinson (1987 [1978]) de que os atos de fala indiretos agregam elementos de polidez nas línguas em geral. / This research deals with the expression of politeness in Brazilian Sign Language (Libras or LSB) and is developed by the analysis of data produced by deaf people who are Libras’ speakers. Just as in any language, in sign languages different registers and degrees of politeness are used. The general objective of this study is to analyze the linguistic elements used as resources in the grammatical expression of politeness in Libras, taking as a start point Brown e Levinson’s (1987 [1978]) research and the chapter that Ferreira Brito (1995) developed on this subject. As this work deals with a theme that is at the interface between grammar and discourse, the theoretical approach takes into account categories of functionalist framework, but also the assumptions of generative grammar, about the existence of a language faculty and of universal grammatical mechanisms for the expression of thought. The methodological approach adopted for this research is based on data collected in order to compare the different grammatical mechanisms used by the deaf people and to analyze these mechanisms based on the adopted theoretical framework. The analysis allowed us to identify that the deaf participants relate formal and informal registers to the more (or less) polite behavior of the interlocutors, the directive structure being preferred in both formal and informal situations. This characteristic was considered to be proper of Libras – confirming the proposal of Ferreira Brito (1995) that familiarity is a fundamental aspect for the description of politeness in this language, and challenging the theory of Brown and Levinson (1987 [1978]) that the indirect speech acts generally show elements of politeness in the languages.

Na última década muitos esforços têm sido feitos em verificação formal de propriedades de agentes do cálculo-π. Uma dessas propriedades é a equivalência observacional, que serve para determinar se um processo é equivalente a sua especificação. Contudo, a verificação de equivalência observacional não é um problema trivial. A maioria dos algoritmos destinados a verificação de equivalência são baseados na construção de sistemas de transições rotuladas (π-autômatos). O principal problema com essa abordagem é o grande número de estados envolvidos podendo chegar a um número infinito. Montanari e Pistore mostram que é possível gerar π-autômatos finitos para agentes-π e é possível reduzir a quantidade de estados desses π-autômatos, através da identificação dos nomes ativos. Um nome é semanticamente ativo em um agente se ele pode ser executado de forma observável por ele. Este é um trabalho de análise estática, que tem por objetivo coletar os possíveis nomes ativos contidos em expressões-π, utilizando para isso um sistema de tipos. A vantagem da utilização de sistemas de tipos em relação a outras formas de análise estática é que sistemas de tipos são sistemas lógicos, logo as técnicas de prova da lógica podem ser aproveitadas no estudo de propriedades de sistemas de tipos. Além disso sistemas de tipos são definidos através da estrutura sintática de expressões, facilitando assim as provas por indução estrutural. Assim a principal contribuição deste trabalho é a elaboração do Active-Base-π, um sistema de tipos para a coleta de nomes ativos de expressões-π.