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é.