Group DescriptionPlease confirm here the name of the group, the Host Institution in which the Principal Investigator is located, four Key words that best describe your work and finally in concise form indicate mains sources of funding for the research of your group. Include all types of funding, like FCT projects, FCT Base, as well as funding from other institutions. You should indicate an approximate amount in EUROS, and the source to which the funds apply. |
| 1. Group Name/Designation |
Formal Models of Computation (RG-COMP-Norte-Porto-27-1036) |
| 2. Principal Investigator |
| Sabine Babette Broda |
| 3. Location of Group (Host Institution) |
| Universidade do Porto |
| 4. Keywords |
| | | | |
| 5. Funding, source, dates (1000 ca.) |
FCT: 31373 Plurianual 2007
+ salaries of team members, University of Porto 2007 + grants, FCT, Gulbenkian, others 2007 |
PI & ResearchersIn this section indicate first the PhD researchers that make up the group by selecting them from the list of researchers integrated in the Unit. In the second section you can indicate whether other PhD researchers not integrated in the Unit collaborate with group by typing their public key. Finally in the last part you should include all the non-PhDs members of the group. |
||||
| 1. Researchers in the Group (PhD. Only) (1) | ||||
|
||||
| 2. Other Researchers in the Group (PhD.) (2) | ||||
|
||||
| 3. Other Researchers in the Group (non PhD.) (2) | ||||
|
||||
Objectives & AchievementsIn this section please describe the main objectives and achievements of the group during the 2007 period . If the number of characters is more than the permitted maximum you will not be able to complete the form. |
| 1. Objectives (2000 ca.) |
- Linear Calculi: in 2006 we defined a new linear type system for a functional language based on iteration (System L). Our main goals for 2007 were to study in detail System L type system (particularly the role of a new kind of polymorphism, which we called iterator types), to apply linearisation techniques to other computational models (besides the lambda-calculus) and to define efficient reduction strategies for system L.
- Type-inhabitation: application of the Formula-Tree proof method in the area of type-inhabitation.
- Resource analysis for lazy functional languages: cost analysis has been undertaken in the context of a strict functional language, producing cost information in the form of data structure sizes. Our goal was to extending it to languages that use lazy evaluation (such as Haskell).
- Logics for multi-agents systems: provide a logical framework for reasoning about the role of Artificial Emotions in the Belief-Desire-Intention agent architecture following the Emotional BDI architecture, developed by the team in a previous work.
- Formal Verification and Specification: we were particularly interested in the use of formal methodologies, tools and applications for the reliability and security of computer systems.
|
| 2. Main Achievements (2000 ca.) |
Linear Calculi: - We defined a monomorphic version of system L and studied in detail the polymorphic version, where an iterated function is used with different types each time. We studied these new types, gave a Curry-style type system for System L, and related it to intersection type assignment systems. Finally we showed that this type system is decidable. - We showed that any primitive recursive function can be defined using a syntactically linear system and that any computable function can be defined using a single minimisation operator and linear functions. This yields an alternative formulation of the theory of recursive functions, where each function is linear, which we called linear recursive functions. - A proof of minimality of the call-by-need strategy for System L. Note that there exists no computable minimal strategy for the lambda-calculus.
Type-inhabitation: - We obtained a neat characterization of the principal types of BCK-lambda-terms, or equivalently the theorems of condensed BCK-logic.
Resource analysis for lazy functional languages: - We defined a semantics for lazy evaluation with appropriate cost information and a preliminary version of a type system for deriving cost information for lazy programs, which is sound with respect to the semantics. This work will be submitted for publication in 2008.
Logics for multi-agents systems: - Development of the logic EBDI for modelling and reasoning about the Emotional BDI architecture. This framework is an extension of BDI_CTL, with modal operators for capabilities, Resources, Actions and Emotional States.
Formal Verification and Specification: - COCO/R for F#. A compiler for the F# programming language (in col. with A. Pereira). – Formal analysis and development of the Condorcert Voting Method system using the B method (in col. with R. Romano). – PCSC for Ocaml, a middleware for programming smart cards in the OCaml programming language (in col. with M. Preliteiro).
|
ProductivityThis section refers to the research output of the group during the 2007. From the list provided choose the items that you want to complete and a field will appear. Follow the instructions provided in each item. You are not required to fill in all the items only those for which your group has output. Please note that for peer reviewed publication you must include impact factor and number of citations. If these indicators are not available you must include that publication as Other Publications. |
| Other publications International (3000 ca.) (Include only Books, chapters or full papers published in conference proceedings up to max of 10. Give title and full citation in original language) |
S. Alves, M. Fernandez, M. Florido and I. Mackie. Linear Recursive Functions. In Rewriting, Computation and Proof, Essays dedicated to Jean-Pierre Jouannaud on the occasion of his 60th birthday. LNCS 4600 Festschrift, Springer, 2007.
S. Alves, M. Fernandez, M. Florido and I. Mackie. Iterator Types. Foundations of Software Science and Computation Structures (FOSSACS 2007), Springer LNCS 4423, 2007.
S. Alves, M. Florido, I. Mackie and F.-R. Sinot. Minimality in a Linear Calculus with Iteration. Proc. of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Electronic Notes on Theoretical Computer Science (ENTCS) 2007.
S. Alves, M. Fernández, M. Florido and I. Mackie. Very Primitive Recursive Functions. Computability in Europe (CiE 2007), Sienna, Italy, 2007.
S. Alves, M. Fernandez, M. Florido and I. Mackie. System T Revisited (Abstract). Workshop on Linear Logic, Ludics, Implicit Complexity and Operator Algebras: Dedicated to Jean-Yves Girard on his 60th birthday. Siena, Italy, 2007.
S. Broda, L. Damas. On Principal Types of BCK-lambda-terms, Wollic'2007, LNCS 4576, pp.120-130, 2007.
D. Pereira, E. Oliveira, and N. Moreira. Formal modelling of emotions in bdi agents. In 8th Workshop on Computational Logic in Multi-Agent Systems (CLIMA-VIII), Porto, Portugal, 10-11/09 2007
V. Santos, M. Freire, J. Hyuk Park, S. Melo de Sousa et al. (Eds.). Proceeedings of the "International Symposium on Information Security - IS 2007". Integrado nas actas de "On the Move to Meaningful Internet Systems 2007" Springer Verlag, LNCS 4803 e LNCS 4804, ISBN 978-3-540-76846-3 e ISBN 978-3-540-76835-7.
V. Santos, P. Rangel Henriques, S. Melo de Sousa et al. (Eds.). Proceedings of the conference Corta’07 "COmpilers, Related Technologies and Applications". Universidade da Beira Interior. ISBN 978-972-8790-70-7.
H. Simoes, K. Hammond, M. Florido and P. Vasconcelos. Using Intersection Types for Cost-analysis of Higher-Order Polymorphic Functional Programs. Types for Proofs and Programs, TYPES 2006 (Revised Selected Papers), LNCS 4502, Springer Verlag 2007.
|
| Master and Ph.D. thesis completed (3000 ca.) |
PhD Thesis: Sandra Alves, Linearisation of the Lambda-calculus. PhD in Computer Science, DCC-FCUP, April 2007.
Msc Thesis: David Pereira, Modelação Lógica de Agentes BDI Dotados de Emoções Artificiais. Master in Informatics - Systems and Networks, DCC-FCUP, May 2007.
|
| Organization of conferences (2000 ca.) |
- Organization of Corta’07 "COmpilers, Related Technologies and Applications". Universidade da Beira Interior, Portugal, July 2007.
- Organization of IS2007, International Symposium on Information Security, November 26-27th, 2007, Vilamoura, Algarve - Portugal.
|
| Internationalization (2000 ca.) (Collaborative publication, Research, Graduate Training Networks or other forms of participation of the Research Group at the international level) |
Collaboration with: - Maribel Fernández, King's College, Ian Mackie, École Polytécnhique, in the area of linear languages, that resulted in the following publications: [1,2,3,4,5].
- Kevin Hammond, St. Andrews University in the area of resourse analysis of functional programs, that resulted in publication [10].
- Temur Kutsia, RISC Institute in the area of unification, resulting in the following publication:
Jorge Coelho, Mário Florido and Temur Kutsia. Sequence Disunification and its Application in Collaborative Schema Construction. WISE 2007 Workshops. LNCS 4832, 2007.
Graduate training: - Hugo Simões. PhD co-advised by Mário Florido (FCUP) and Kevin Hammond (University of St. Andrews).
- Co-supervision of Stephane Cauchie (with Thierry Brouard) from the Laboratoire d'Informatique de l'Université de Tours. Design and validation of a cryptographically secure and distributed biometric system.
- François Régis-Sinot. Post-doc advised by Mário Florido (FCUP). This Post-doc originated a research collaboration with École Normale Supérieure de Cachan. |