Theory and Formal Methods Seminar Series

Wednesdays at 9:00 in the DI meeting room

The Theory and Formal Methods Seminar series (TfmSeminar) is a bi-weekly scientific colloquium organized by the Theory and Formal Methods group. The seminar continues the tradition of PURé Café in a wider scope.

Moderator: Jorge Sousa Pinto.

Attendance is open to all.

If you would like to contribute a talk, please contact the moderator.

Upcoming talks

As of September 2007, the TFM seminar series will been continued with a wider scope as the FAST Group Seminar.

Past talks

Wed, 14 Feb, 2007 at 12:00
Extended Static Checking by Strategic Rewriting of Pointfree Relational Expressions
Claudia Necco
We describe how a pointfree treatment of relations, their properties, their operators, and the laws that govern them can be captured in a type-directed strategic rewriting system for transformation of relational expressions. This rewriting tool can be used to simplify relational proof obligations and ultimately reduce them to tautologies. We demonstrate how such reductions provide extended static checking (ESC) for design contraints commonly found in software modeling and development.

Wed, 13 December, 2006 at 11:00
XCentric: processamento de XML em programação em lógica
Jorge Coelho, LIACC
Nesta palestra vamos apresentar a linguagem de programação especializada no processamento de XML, XCentric. O XCentric é uma linguagem de programação em lógica baseada numa extensão ao algoritmo de unificação de Robinson para lidar com termos com functores de aridade arbitrária e num sistema de tipos que extende a noção de tipo regular para para permitir tipificar sequências de argumentos: os "regular sequence types". Vai ser apresentada a linguagem, vários exemplos de utilização, o uso de termos com functores de aridade flexivel para representar XML e de regular sequence types para representar linguages de tipos para XML (DTDs e XMLSchema). Em seguida vamos mostrar o uso da nova forma de unificação no processamento (muito compacto e declarativo) de XML e o uso dos tipos para validação desse processamento.

Wed, 6 December, 2006 at 9:00
Compreensão de Algoritmos de Routing / Understanding Routing Algorithms
Mario Berón
Nesta palestra conceptualizamos Compreensão de Programas e Ferramentas de Compreensão de Programas. Depois descrevemos um esquema de anotação de código que permite a extracção de informação dinâmica de programas escritos em linguagem C. Como passo seguinte apresentamos um sistema de avaliação de algoritmos de routing denominado EAR (un Evaluador de Algoritmos de Ruteo) que utilizamos para analisar a aplicabilidade do nosso esquema de anotação de código. Também, apresentamos as diferentes visões de EAR que foram extraídas a partir do nosso esquema de anotação. Finalmente apresentamos BORS (Behavioral-Operational Relation Strategy), uma estratégia para relacionar as visões comportamental e operacional de sistemas.

Wed, 15 November, 2006 at 9:00
Transformation of Structure-Shy Programs
Alcino Cunha
We present an algebraic approach to transformation of structure-shy programs, in particular strategic functions (eg. Strafunski or SyB) and XML queries (eg. XPath). We formulate a rich set of algebraic laws and show how subsets of these laws can be used to construct rewrite systems for specialization, generalization, and optimization of structure-shy programs. Our approach demonstrates that the analogy between the Laplace/Fourier transforms and the point-wise/point-free transform can be extended with a structure-shy/point-free transform.

Wed, 25 October, 2006 at 9:00
Utilização das ferramentas Caduceus, COQ e SIMPLIFY na Verificação de programas em C
José Pedro Correia and José Pedro Magalhães

Wed, 18 October, 2006 at 9:00
Secure Cryptographic Workflow in the Standard Model
Manuel Bernardo Barbosa
Following the work of Al-Riyami et al. we define the notion of key encapsulation mechanism supporting cryptographic workflow (WF-KEM) and prove a KEM-DEM composition theorem which extends the notion of hybrid encryption to cryptographic workflow. We then generically construct a WF-KEM from an identity-based encryption (IBE) scheme and a secret sharing scheme. Chosen ciphertext security is achieved using one-time signatures. Adding a public-key encryption scheme we are able to modify the construction to obtain escrow-freeness. We prove all our constructions secure in the standard model.

Wed, 4 October, 2006 at 9:00
Short introduction to the 2LT project
Alcino Cunha
A two-level data transformation (2LT) consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. A typical example of a 2LT consists in transforming XML schemas into relational database schemas, coupled with the migration of the XML documents to relational tables. Recently, we have developed a type-safe Haskell library for 2LT, based on the theory of data refinement.
9:15
Generation and preservation of referential constraints during two-level tranformation
Pablo Berdaguer
Abstract not available yet
9:45
Luís Pedro Machado
On the correspondance between generic lenses and data refinement
Abstract not available yet

See the past talks of PURé Café.