Identificação de nomes ativos em agentes-π baseada em tipos

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-π.

O que norteia a escolha de professores de língua estrangeira por diferentes tipos de feedback corretivo

O presente estudo foi desenvolvido com o objetivo de investigar, através de uma perspectiva sociocultural, o que norteia a escolha de diferentes tipos de feedback corretivo por professores de língua estrangeira (LE) ao corrigir a fala de seus alunos. A pesquisa foi realizada em um curso particular de idiomas no sul do Brasil que segue os princípios da abordagem comunicativa, tendo cinco professores como participantes. Este trabalho foi realizado através da observação do comportamento corretivo dos professores atuando com seus próprios alunos durante atividades com foco na forma. Tais atividades foram gravadas em vídeo e, logo após a gravação, foram comentadas pelos professores durante entrevistas com a pesquisadora, as quais também foram gravadas em vídeo. Houve uma terceira gravação que consistiu em uma entrevista entre a pesquisadora e cada professor participante para conversarem sobre as percepções dos professores a respeito de tratamento corretivo e diferentes tipos de feedback. A análise das transcrições das gravações resultou em um levantamento e uma descrição das escolhas corretivas de cada professor individualmente e uma descrição do padrão de comportamento quanto à opção por feedback reformulador e/ou feedback elicitativo. Verifiquei que os cinco professores estudados - mesmo tendo experiências, tempo de prática e formação diferentes - consideram principalmente os seguintes fatores quando decidem optar por tipos de feedback: como julgam que o aluno está se sentindo no momento, como vêem a personalidade do aluno e como julgam ser a capacidade lingüística e a capacidade emocional do aluno.