LÓGICA E COMPUTAÇÃO – UM

A investigação desenvolvida pelo grupo de investigação em Lógica e Computação centra-se na teoria estrutural da demonstração e na teoria de tipos, com ênfase (i) na relação entre sistemas formais de demonstração e extensões do lambda-calculus e (ii) no uso de tipos para controlar a terminação de definições recursivas. No panorama internacional existem vários investigadores que desenvolvem investigação próxima deste tópicos, a maioria deles membros do projecto europeu TYPES, no qual este grupo de investigação participa como sub-site. Na Universidade de Helsínquia, Sara Negri e Jan von Plato desenvolvem a teoria estrutural da demonstração com vista ao estudo de teorias matemáticas. A investigação da teoria estrutural da demonstração com ênfase nos aspectos computacionais desenvolve-se em St Andrews (R. Dyckhoff, S. Lengrand), Munich (H. Schwichtenberg, R. Matthes), Paris (P.-L. Curien, H. Herbelin) e CMU (F. Pfenning). No domínio da aplicação de tipos para assegurar a terminação de funções recursivas deve destacar-se a investigação em Sophia Antipolis (G. Barthe), em Munich (A. Abel) e em Tallinn (T. Uustalu). A nível nacional não existem outros centros que desenvolvam investigação nestes tópicos específicos, além de uma investigadora do Dep. de Informática da UM (M.J.Frade) co-autora de trabalhos com os membros deste grupo. No entanto, existem investigadores na U. do Porto (Dep. de Ciência de Computadores) e no IST (Dep. de Matemática) cuja investigação cobre áreas (tais como lambda-calculus, sistemas dedutivos e lógicas não clássicas) com afinidades com a investigação desenvolvida no DMAT da UM.

O grupo é um sub-site da rede europeia TYPES, que reúne a generalidade dos investigadores europeus com interesse em Teoria de Tipos. Este projecto financia a participação em eventos organizados no âmbito da rede e financia visitas entre membros da rede. Num passado recente, o grupo esteve ainda envolvido em dois projectos na área da Teoria de Tipos, focando, respectivamente, em tipos dependentes e em subtipificação com tipos indutivos. Ambos os projectos contaram com o envolvimento do Dep. de Informática da UM. No primeiro caso o projecto resultou de uma colaboração com G. Barthe (Sophia-Antipolis). Já o segundo projecto foi inteiramente desenvolvido na UM, tendo contado com o bolseiro de pós-doutoramento T. Uustalu.

Projectos:

1. TYPES, projecto europeu (Coordination Action FP6 510996), 2004-2007
2. Sistemas de Tipos Dependentes para Provas e Programas, projecto ICCTI/GRICES-INRIA, 2001-2003.
3. TYPES, projecto europeu (IST Workingroup 29001), 2000-2003
4. Foundations and Applications of Constructor Subtyping, projecto FCT (PRAXIS/EEI/14172/98), Julho de 1999 a Abril de 2002.

LÓGICA E COMPUTAÇÃO – UA

O DMAT-UA possui o único grupo que trabalha em Geometria Computacional em Portugal, estando integrado nesse grupo, na qualidade de colaborador, um professor da Universidade de Porto. Dentro desta área, a investigação desse grupo está centrada fundamentalmente no estudo dos problemas da galeria de arte: visibilidade, iluminação e vigilância, assunto este que tem sido extensamente estudado por investigadores da área e onde permanece um conjunto de importantes problemas por resolver.

A Computação Quântica é uma área emergente, sendo ainda poucos e recentes os grupos nacionais que a ela se dedicam. Os tópicos desta área que caracterizam a investigação desenvolvida no DMAT-UA são os circuitos de aritmética quântica e a simulação de algoritmos quânticos.

A investigação desenvolvida na área de Álgebra, Lógica e Computação centra-se na aplicação de métodos e resultados da Lógica Algébrica à teoria da especificação de tipos de dados abstractos. Temos estado essencialmente interessados no estudo das lógicas escondidas (Hidden logics). Estas lógicas são utilizadas na especificação de sistemas orientados a objectos; neste caso, temos de considerar estas lógicas de especificação como sistemas dedutivos e a equivalência comportamental como uma noção generalizada da congruência de Leibniz. Parte desta investigação tem sido realizada em colaboração com o Professor Don Pigozzi, reconhecido investigador na área da Lógica Algébrica. Actualmente, em colaboração com o grupo de Lógica e Computação do DM-IST, estamos a investigar a teoria algébrica de certos tipos de lógicas, nomeadamente a algebrização de lógicas multi-género, lógicas não-vero-funcionais e lógicas combinadas.

No panorama internacional são muitos os grupos de investigação dedicados ao estudo da classe referida de problemas de Geometria Computacional, como por exemplo: Grupo de Geometria Computacional da Universidad Politécnica de Madrid, Grupo de Geometria Computacional da Universidad Politécnica de Cataluña, Department of Applied Mathematics and Statistics of the State University of New York at Stony Brook, Los Álamos National Laboratory, School of Computer Science at Carleton University, the Algorithms Group at the Department of Computer Science of the Technical University of Eindhoven, etc.

A Computação Quântica é uma área em fase de enorme crescimento a nível internacional. Apesar de recentes, são inúmeros os centros onde é desenvolvida investigação multidisciplinar, tanto no sentido da construção de dispositivos quânticos, como na elaboração de algoritmos quânticos e no estudo da sua complexidade computacional.

Projectos industriais:

1. “Programação inserida no sector de extrusão de alumínio”; empresa Extrusão de Alumínio S.A., início Oct/03, duração 6 meses, PRODEP III - Programa Operacional Educação.
2. “Desenvolvimento de uma aplicação Informática para o Controlo da Qualidade”; empresa Heliflex Petzetakis Tubos, Lda., início Oct/00, duração 6 meses, PRODEP III - Programa Operacional Educação;
3. “Desenho e Implementação de um Sistema de Apoio à Decisão na Organização de um Processo Tecnológico em Artigos de Vidro Decorados”, empresa Alberto Martins & Filhos Lda., início Oct/99, duração 6 meses, PRODEP III – Programa Operacional Educação;

Outros projectos:

1. “Problems of Illumination and Visibility in Computational Geometry”, em colaboração com investigadores da Universidade de Porto, da Universidad Politécnica de Madrid, da Universidade de Acalá, da Universidad de Valladolid e da Universidad Pontifícia de Comillas (Madrid), 2006-2007, Acções Integradas Luso-Espanholas.