Relation to long term objectives denoted by
[SR] Software reliability
[SEC] Security
[RI] Reliable Information
[DDD] Distributed, decentralized, dynamic problems
Being a basic research group the subjects studied here are relevant
to most problems in Computer Science.
Unification [SR,SEC,RI]:
Recently several interesting relations between three forms of
unification (higher-order, context and sequence) have been intensively
studied in order to reach general algorithms for decidable fragments.
Our main goals in this area:
- Sequence unification: Definition of a complete and terminating algorithm for a
restricted form of sequence unification. Application of these results to
context and higher-order unification, and to more expressive classes of
the problem are now relevant problems in unification theory.
- Higher-order unification: exploit applications of the Formula-Tree
proof method in finding more expressive sets of solutions for
decidable fragments of higher-order unification, with finite (and
computable) descriptions.
Linear calculi [SR,SEC,RI]:
Linear languages are easier to implement and verify and are
intrinsically reversible, thus good candidates for the basis of reliable
information processing.
Concerning this area, the main goals are:
- Study the possibility of obtaining an efficient implementation of
linear systems defined before based on existing efficient algorithms for
implementing linear calculi.
- Definition of computational complete models based on linearity. More
concretly, can one define a linear version of PCF (Programming
language for Computable Functions)?
- Definition of new polymorphic type systems for linear calculi with
iteration.
- Study the growth of linearised terms. This promises to show an
interesting interplay between time and space in computation.
Program Verification [SR,SEC,RI,DDD]:
Study and implement new verification methods for embedded systems.
Two main frameworks to tackle
the formalisation of the corresponding security and safety properties
will be considered:
- the use of types (such as type-and-effect analysis) as safety evidence;
- a more traditional approach to Proof-Carrying-Code (PCC), to resort to
source-level PCC, to apply Type Inhabitance and techniques based on
temporal logic/automata to improve the proof infrastructure of a PCC platform.
The final stage consists in setting up a working backend platform for
the static security enforcement mechanisms applied to embedded systems.
Mário Florido e Luís Damas, Linearization of the Lambda-Calculus and
its Relation with Intersection Type Systems. In Journal of Functional
Programming, CUP, 14, 2004. IF=0.930, nC=0
Sandra Alves and Mário Florido, Weak Linearization of the
Lambda-Calculus. Theoretical Computer Science, 342 (1), 79-103,
Elsevier Science, 2005. IF=0.843, nC=0
Sabine Broda, Luís Damas, On Long Normal Inhabitants of a
Type. Journal of Logic and Computation, 15, 353-390, 2005. IF=0.840,
nC=0
Gilles Barthe, Pierre Courtieu, Guillaume Dufay and Simão Melo De
Sousa, Tool-Assisted Specification and Verification of Typed Low-Level
Languages. Journal of Automated Reasoning, 35 (4), 295-354, 2005,
IF=0.875, nC=2.
Hugo Simoes, Kevin Hammond, Mário Florido and Pedro Vasconcelos. Using
Intersection Types for Cost-analysis of Higher-Order Polymorphic
Functional Programs. Proceedings of TYPES 2006, LNCS, 4502, 221-236,
2006.
Scholarships for PhD (3) and MSc (3) students.