History-Dependent automata (HD-automata in brief) are an extension of ordinary automata that overcomes their limitations in dealing with history-dependent formalisms, like pi-calculus, CCS with causal dependencies or localities, and place/transition Petri nets. Ordinary automata are an unsatisfactory operational model for these formalisms: infinite automata are usually obtained for systems with infinite computations, even for very simple ones; moreover, the ordinary definition of bisimilarity does not apply in these cases, thus preventing the reuse of standard theories and algorithms.

Successive work has proposed to model the transition system of the pi-calculus as a bialgebra, more precisely as a coalgebra on a category of name permutation algebras, and to define its abstract semantics as the final coalgebra on such a category. It is possible to link the coalgebraic semantics with a version of HD-automata where states are equipped with groups of name permutations called symmetries. Here bisimilarity in the bialgebraic context corresponds to the minimal HD-automaton. In recent work presented at CONCUR 2002 the bialgebraic approach has been extended with the pi-calculus operations of parallel composition and restriction.

(work in collaboration with Marco Pistore and Marzia Buscemi).

The term 'categorical logic' denotes those tools and techniques from category theory that are used for recasting the languages provided by mathematical logic by means of objects, arrows and universal properties.

Its use has been advocated, since the seminal mid-Sixties work of Lawvere, as a way of exploring the relationships among different logical formalisms, by mapping them into categorical structures whose properties are characterized by relatively few underlying concepts (such as binary products, exponents, etc.). In addition, the investigations on categorical semantics often provided hints for developing new formalisms, see e.g all those languages arising from lambda-calculus as a variant of the internal language of cartesian closed categories.

The aim of these introductory talks is to show the main applications of categorical logic to the semantics of algebraic specifications, as well as for presenting an extension dealing with recent advances in the field of rewriting formalisms.

1) Basics of equational deduction
2) Categorical semantics for equational specifications (classifying and functor categories)
3) Algebraic and weaker theories (terms vs let-terms)
4) Basics of rewriting logic (incl. let-rewriting)
5) Categorical semantics for rewriting specifications
6) Algebraic and weaker 2-theories
7) Basics of tile logic
8) Categorical semantics of tile specifications
9) Algebraic double theories

A noção de refinamento captura a essência da atividade diária de engenheiros de software, ao projetar sistemas tendo em vista suas especificações, e de programadores, ao implementar estes projetos. Em ambos os casos, um objetivo central e a construção de sistemas e programas de acordo com as suas especificações. O produto final, primordialmente, tem que ser correto.

Refinamento é exatamente a relação que existe entre uma especificação e uma implementação correta desta especificação. Métodos de desenvolvimento formal de software, como todos os outros, são baseados nesta noção, mas vão além no sentido de que a tornam central para o processo de programação.

Neste tutorial, nós vamos apresentar as noções clássicas de refinamento, incluindo refinamento de algoritmos e refinamento de dados, que é vital para o tratamento de módulos. Nós vamos também apresentar preocupações mais recentes associadas ao desenvolvimento formal de programas orientados a objetos e concorrentes. Nestes casos, as noções de refinamento precisam ser adaptadas devido as características adicionais das linguagens de programação: objetos, heranca, ligação dinâmica, e paralelismo.

No mundo real, grande parte dos processos são não-seqüenciais. Ou seja, muitas vezes, nos deparamos com processos concorrentes. Computacionalmente, em diversos níveis, de um simples chip a uma rede de computadores, o comportamento é dado de forma distribuída e concorrente.

Assim, a modelagem formal de sistemas concorrentes é claramente de grande importância. Diversos modelos para este propósito foram formalizados, originando as seguintes perguntas: Quais as diferenças entre eles? Quais modelos são mais expressivos que outros? Qual a aplicabilidade de cada modelo? Qual abstração está por trás de cada modelo?

Alguns modelos são mais abstratos que outros, e isto é freqüentemente utilizado em classificações informais com respeito a expressibilidade destes. Através da representação categorial e do uso de adjunções, é possível estabelecer uma hierarquia entre os diferentes modelos, do menos expressivo ao mais expressivo, além da possibilidade de se mostrar formalmente uma medida da diferença entre eles. Este é um dos principais objetivos a ser explorado por este tutorial.

Tópicos a serem abordados:

- modelos de sistemas de transição etiquetados, estruturas de eventos, traços, redes de Petri e autômatos não-seqüenciais;
- introdução às vantagens de modelos para concorrência vistos como categorias;
- relações entre diferentes modelos expressos através de adjunções;
- contribuição de Teoria das Categorias para modelos de concorrência.

Este tutorial não pressupõe conhecimentos acerca da Teoria das Categorias, estando ao alcance de todos alunos de graduação em computação com conhecimentos prévios em matemática discreta e semântica formal.