Estudar

LEMA promove seminário sobre linearização quantitativa fraca
20-05-2026

Realiza-se, no próximo dia 27 de maio, às 12h00, um seminário em Engenharia Matemática, intitulado “Quantitative Weak Linearisation”, promovido pelo Laboratório de Engenharia Matemática (LEMA) do Instituto Superior de Engenharia do Porto (ISEP).  

O evento, que irá decorrer na sala H211 do ISEP, terá como oradora Sandra Alves, docente do Departamento de Ciência de Computadores da Faculdade de Ciências da Universidade do Porto. 

 

Resumo 

A linearização de funções é o processo de tornar funções lineares, no sentido em que os seus argumentos ocorrem na definição da função exatamente uma vez. A linearização fraca foi definida há anos por meio de uma caracterização estática da noção intuitiva de redex virtual, baseada em caminhos válidos, calculados a partir da árvore sintática dos termos. Termos fracamente lineares impõem uma condição de linearidade apenas às funções que são aplicadas, consumidas pela redução; e funções que não são aplicadas, portanto, persistem no termo ao longo de qualquer redução, podem ser não lineares. Demonstrou-se que essa classe de termos é fortemente normalizável, com tipagem decidível em tempo polinomial. Revisitamos essa noção por meio de tipos com interseções não idempotentes, também chamados de tipos quantitativos. Ao usar uma caracterização eficaz de tipos mínimos, baseada na noção de coesão, somos capazes de distinguir entre construtores de termos "consumidos" e "persistentes", o que nos permite definir uma relação de expansão entre termos-lambda gerais e lambda-termos fracamente lineares, preservando as formas normais. 

 

 

Biografia 

Sandra Alves é Professora Auxiliar do Departamento de Ciência de Computadores da Faculdade de Ciências da Universidade do Porto. O seu trabalho de investigação centra-se no estudo e desenvolvimento de modelos e ferramentas para análise e verificação de sistemas computacionais usando teoria de tipos, reescrita e cálculos fundamentais. Tem particular interesse em modelos que lidam, implícita ou explicitamente, com recursos.  

Na sua tese de doutoramento, concluída em 2007, abordou sistemas de tipos para linguagens lineares, pela qual recebeu uma distinção para jovens pesquisadores da Fundação Calouste Gulbenkian. Publicou diversos artigos em importantes conferências e revistas internacionais. É editora associada da revista CUP Journal on Mathematical Structures in Computer Science, membro da direção das comunidades ACM Special Interest Group on Logic and Computation e International Federation of Computational Logic, e ainda membro do grupo de trabalho de reescrita da International Federation for Information Processing. Participou nas comissões organizadoras de diversas conferências e workshops (TLCA, FSCD, TYPES, Linearity, LSFA, WiL). Tem um forte envolvimento na comunidade de investigação, tendo participado na organização e comités científicos de dezenas de eventos.