Deciding Kleene Algebra Terms Equivalence in Coq

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

Que alternativa ao currículo regular no ensino básico?

Encaramos o currículo como um projeto em constante transformação, que tendo por referência o currículo nacional, é adequado ao seu públicoalvo, os alunos. No contexto de cada comunidade onde a escola está inserida, a definição das ofertas educativas/curriculares assume maior pertinência, podendo contemplar componentes locais e regionais do currículo, valorizando as caraterísticas de cada região e, sobretudo, engrandecer os talentos dos alunos, de acordo com as suas especificidades individuais. A reflexão, realizada em torno das dificuldades que muitos alunos têm em realizar as aprendizagens previstas no currículo oficial, deu origem a uma questão central: Que alternativa ao currículo regular no ensino básico? Na procura de respostas à questão, abordamos o nascimento da escola e conceitualização de currículo, a evolução da formação para o mundo do trabalho, a diversificação curricular e a autonomia da escola. O estudo empírico seguiu uma metodologia quantitativa e qualitativa, através de um estudo de caso e centrou-se: na análise documental do Projeto Educativo do Agrupamento; inquérito por questionário aos alunos do terceiro ciclo do ensino básico, regular e cursos vocacionais; inquérito por entrevistas semiestruturadas ao Presidente do Conselho Geral do Agrupamento, Diretora do Agrupamento, Coordenadoras de Departamento, Coordenador dos Cursos Vocacionais e representante no Conselho Pedagógico dos Serviços de Psicologia e Orientação. Expomos as conclusões da investigação através da triangulação dos dados obtidos com os instrumentos de recolha. Como resposta à questão inicial, apresentamos uma proposta alternativa ao currículo regular do ensino básico, que procura diversificar a oferta.