Center for Logic and Computation 

Activities Report 2005

April 12, 2006

The Center for Logic and Computation (CLC) is a research unit of the Department of Mathematics of IST established on February 14, 2001 (formerly the Logic and Computation Group of Centro de Matemática Aplicada). The Center is a member of CIM (Centro Internacional de Matemática).

The Center develops its research and scientific training activity in mathematics supported by FCT and FEDER under POCTI, with special emphasis on logic and theory of computation, including related aspects of algebra, topology and dynamical systems, as well as applications to engineering, biology, physics and other sciences.

Executive Committee (2005-2006): 

• Cristina Sernadas (President).
• Paulo Mateus.
• João Rasga.

Advisory Committee: 

• Giuseppe Longo (CNRS & Ecole Normale Supérieure, France), since February 5, 2004.
• Andre Scedrov (U Pennsylvania, USA), since January 11, 2002.
• Umesh Vazirani (U California at Berkeley, USA), since July 22, 2005.

1- Overview

The Center develops research and advanced scientific training activities in Mathematics, currently organized as follows:

• Task 1 - Abstract deductive systems
  [Project Fiblog and some representative publications]
  Analysis and synthesis of logic systems, including modal logic, hybrid logic, paraconsistent logic, observational logic, probabilistic logic, algebraic logic, higher-order logic and categorical logic, with applications in knowledge representation, software engineering and security.

• Task 2 - Probabilistic and quantum computation and information
  [Projects Quantlog, Problog and some representative publications]
  Probabilistic models of computation, quantum computation and quantum cryptography, with applications in security.  

• Task 3 - Dynamical systems and computational complexity
  [Project ConTComp and some representative publications]
  Digital and analog computation, physical realizability of analog computational classes, recursive functions over the reals, analog characterization of low time complexity classes, links between computational complexity and dynamical systems, neural networks, and brain modeling with dynamical systems.

• Task 4 - Type theory, constructive mathematics and mobile computation
  [Projects Space-Time-Types, Sensoria and some representative publications]
  Higher-order logics and type systems applied to constructive mathematics and to provably correct concurrent and distributed mobile systems.

During 2005, the shift towards topics in the quantum front continued in Task 1 and Task 2 (see the survey paper 06-SMO-quantlog09.pdf), with the formal start of the QuantLog project in January.

Within Task 1, the work on exogenous quantum logic resulted in the development of a novel logic (EQPL) for reasoning about pure quantum states, its complete axiomatization, and the identification of a decidable fragment. The exogenous approach to enriching a given logic towards probabilistic or quantum reasoning was further investigated, namely in the context of the theory of institutions. Work was started towards extending EQPL with dynamical constructs for reasoning about probabilistic and quantum imperative programs. Ricardo Gonçalves is working towards his PhD on the topic of algebrization of exogenous probabilistic and quantum logics. Work continued in close cooperation with David Basin and Luca Viganò (ETH, Switzerland) on kleistic logics (logics of security). First steps were given on the problem of setting up a general purpose logic of indistinguishability. João Marcos concluded his PhD with work on paraconsistent logic. Concerning the theory of fibring, the work was focused on producing two survey papers and on the forthcoming book Analysis and Synthesis of Logics (at this stage with 500 pages). Finally, the theory of fibring was extended to the heterogeneous scenario and sequent calculi.

In  Task 2, the work continued on minimization of quantum automata, comparison of random and quantum walks, quantum process algebras, and quantum security. Furthermore, a variation of Grover's quantum search algorithm was proposed for pattern matching in long strings and a quantum attack was devised against classical zero-knowledge proof protocols. Pedro Adão, while working towards his PhD, made several significant contributions to the understanding of the Dolev-Yao abstraction of the probabilistic computational model of security, with extended stays at Penn University and Microsoft, Cambridge. First steps were given towards quantum protocols for contract signing and model checking of probabilistic and quantum protocols. Tiago Reis was awarded a scholarship from FCT to prepare his PhD at ETH on the latter topic. In cooperation with Pedro Freitas (GFM), work started on estimating gaps of Hamiltonians relevant in adiabatic quantum computation. Pedro Ribeiro, who is working towards his PhD at LPTMC, Université Pierre et Marie Curie, France, joined the Center in November 2005. CLC was visited by many distinguished researchers active in quantum computation and information. The proposal of the Lisbon Quantum Computation, Information and Logic (LQCIL'07), IST, Lisboa, July 18-20, 2007 was submitted to CIM - Centro Internacional de Matemática (and has already been approved).

Work in Task 3, under the ConTComp project, was partly directed to the analysis of the computational properties of analytic differential equations and, in particular, of polynomial type. It was shown that analytic flows and maps can simulate Turing machines. The equivalence of computable analysis and polynomial differential equations was proved in an appropriate framework. This is one of the first results on the equivalence of distinct analog computation paradigms. Some decidability results on analytic ordinary differential equations have also been investigated in cooperation with Jorge Buescu (CAMGSD) and Ning Zhong (Cincinnati University, USA). Daniel Graça visited Olivier Bournez (Loria, Nancy) during most of 2005 to work on those topics and toward his PhD thesis. The collaboration with Olivier Bournez' group in Nancy was formalized through the Franco-Portuguese research programme PESSOA for the years 2005-2006. Kerry Ojakian started to work on the complexity of real recursive functions. With respect to computational properties of continuous-time neural nets, the dual possibility of approximate as well as exact computation continued to be investigated in a unified framework. Relations were established with other systems outside the realm of neural nets, while keeping an emphasis on the possibility of using spatio-temporal chaotic regimes as computational modes for the larger class of systems. Still within the scope of Task 3, the International Workshop on Computations on the Continuum was organized and hosted in June 27-28 (including thirteen talks by participants from abroad, and three talks by local participants).

Finally, within the scope of Task 4, work continued, mostly dedicated to applications of type systems, on two fronts: (i) behavioural type systems, session types for the verification of correct protocol
implementations, and action types for ensuring deterministic system behaviour, in close cooperation with Simon Gay (U Glasgow) and within the scope of projects Space-Time-Types: Behavioural and Spatial Type Systems, Sensoria and Communication protocols in session types; (ii) constructive mathematics, namely on the subject of extraction of efficient algorithms from formalizations of constructive proofs and on the issue of representing partial functions in logic. Maxime Gamboni started work towards his PhD within the topic of behavioural type systems. CLC contributed to the organization of  the 32nd International Colloquium on Automata, Languages and Programming and Satellite Workshops, FCG and IST, Lisboa, July 11-15 and July 10, 16-17, 2005.

In December 2005, CLC made a call for applications for visiting scientists and postdocs. Grants were awarded to Mingsheng Ying (visiting scientist from Tsinghua University, Beijing, China) and Nikola Paunkovic (postdoc) for 2006.

2- Members

During 2005, J. Marcos, R. Chadha and K. Ojakian joined CLC as full members. P. Ribeiro, P. Baltazar and M. Gamboni joined the Center as student members. By the end of December 2005 the membership of CLC was as folows:

• Full members:
  1. CALEIRO, Carlos (Assistant Professor, SLC) founding member
  2. CAMPAGNOLO, Manuel (Assistant Professor, ISA) since 2002
  3. CHADHA, Rohit (Postdoc Fellow on a grant from FCT) since 2005
  4. CRUZ-FILIPE, Luís (Postdoc Fellow on a grant from FCT, Invited Assistant Professor, SLC) since 2004
  5. DIONÍSIO, F. Miguel (Assistant Professor, SLC) founding member
  6. GOUVEIA, Paula (Assistant Professor, SLC) founding member
  7. HERMIDA, Claudio (Research Fellow on a grant from CLC) since 2004
  8. LOURENÇO, Carlos (Assistant Professor, FCUL) since 2002
  9. MARCOS, João (Associate Professor, UFRN) since 2005
  10. MATEUS, Paulo (Assistant Professor, SLC) founding member
  11. OJAKIAN, Kerry (Postdoc Fellow on a grant from FCT) since 2005
  12. RAMOS, Jaime (Assistant Professor, SLC) founding member
  13. RASGA, João (Assistant Professor, SLC) since 2003
  14. RAVARA, António (Assistant Professor, SLC) founding member
  15. SERNADAS, Amílcar (Full Professor, SLC) founding member
  16. SERNADAS, Cristina (Full Professor, SLC) founding member
• Student members:
  1. ADÃO, Pedro (on a scholarship from FCT) since 2001
  2. BALTAZAR, Pedro (Monitor, SLC,  on a scholarship from FCT) since 2005
  3. CAMACHO, Luís (Teaching Assistant, University of Madeira) since 2004
  4. GAMBONI, Maxime (on a scholarship of the Space-Time-Types project) since 2005
  5. GONÇALVES, Ricardo (Monitor, SLC, with a research grant in 2005 from Fundação Calouste Gulbenkian and on a scholarship from FCT) since 2004
  6. GRAÇA, Daniel (Teaching Assistant, UALG, with a research grant in 2004 from Fundação Calouste Gulbenkian and on a scholarship from FCT) since 2001
  7. PAIS, Hélio (Monitor, SLC) since 2004
  8. REIS, Tiago (at ETH on a scholarship from FCT) since 2005
  9. RIBEIRO, Pedro (at LPTMC - Université Pierre et Marie Curie on a scholarship from FCT) since 2005
• Collaborators:
  1. ALMEIDA, Jorge (Assistant Professor, SAA)
  2. BUESCU, Jorge (Assistant Professor, SAA and CAMGSD)
  3. CARNIELLI, Walter (Full Professor, Unicamp)
  4. FRANCISCO, Alexandre (Teaching Assistant, DEI)
  5. FREITAS, Pedro (Full Professor, FMH and GFM)
  6. GARCIA, Narciso (Associate Professor, SAA)
  7. MARTINS, Ana Maria (Assistant Professor, DF and CFP)
  8. NUNES, Cláudia (Assistant Professor, SEA and CEMAT)
  9. OMAR, Yasser (Assistant Professor, ISEG and CEMAPRE)
  10. ORESTES, Jorge (Associate Professor, ISA)
  11. PACHECO, António (Associate Professor, SEA and CEMAT)
  12. ROCHA VIEIRA, Vítor (Research Coordinator, CFIF)
• Honorary members:
  1. CARMO, José (Full Professor, University of Madeira)
  2. RESENDE, Pedro (Associate Professor, SLC and CAMGSD)
  3. VALENÇA, José Manuel (Full Professor, University of Minho)

3- Guest program

The Center has maintained an intensive guest program since the beginning of the financial support by FCT. Some researchers have stayed at CLC for extended periods. Close cooperation continue with most of those long term visitors.

The following researchers visited the Center in 2005:

1. Sougato Bose, University College London, UK, 12-17.12.05. Lecture: Quantum communication through spin chains and related systems, 13.12.05.
2. Luís Russo, INESC, Portugal, 9.12.05. Lecture: Improved indexing of text using the Ziv-Lempel trie.
3. Anton Zeilinger, U Vienna, Austria, 2.12.05. Lecture: From Einstein to Quantum Information.
4. Jonathan Borwein, Dalhouisi University, Canada, 22-29.11.05. Lecture: What is High Performance Mathematics, 28.11.05.
5. Markus Arndt, U Vienna, Austria, 16-20.11.05. Lecture: Experimental exploration of the quantum/classical transition, 18.11.05.
6. Sara Madeira, INESC and U Beira Interior, Portugal, 11.11.05. Lecture: CCC-biclustering: a linear time biclustering algorithm for time-series gene expression data.
7. Walter Carnielli, CLE, UniCamp, Brazil, 2-7.10.05. Lecture: Infinite voting, fuzziness and modulated quantifiers, 4.10.05.
8. Dan Ghica, U Birmingham, UK, 16-22.9.05. Lecture: Data-abstraction refinement: a game semantic approach, 20.9.05.
9. Kokichi Futatsugi, JAIST, Japan, 13.9.05. Lecture: Formal Methods with CafeOBJ.
10. Francesco Ciccarello, U Palermo, Italy, 11-16.9.05. Lecture: Hot electron noise in n-type GaAs in crossed electric and magnetic fields, 13.9.05.
11. Luca Viganò, ETH, Switzerland, 28.8-12.9.05. Lecture: The AVISPA Tool for the automated validation of internet security protocols and applications, 9.9.05.
12. Alessandra di Pierro, U Pisa, Italy, 29.8-5.9.05. Lecture: Time-based interference and probabilistic padding, 2.9.05.
13. Elham Kashefi, IQC, U Waterloo, Canada, 1-5.9.05. Lecture: Measurement Calculus, 2.9.05.
14. Lutz Schröder, U Bremen, Germany, 25-30.7.05. Lecture: Expressivity of coalgebraic modal logic, 29.7.05
15. José Carlos Cifuentes, UF Paraná, Brasil, 22.7.05. Lecture: Lógica fuzzy e consistência polivalente.
16. David Basin, ETH, Switzerland, 11-17.7.05. Lecture: Model driven security, 14.7.05.
17. Umesh Vazirani, U California, Berkeley, USA, 12-16.7.05. Lecture: Quantum algorithms: The non-abelian hidden subgroup problem, 14.7.05.
18. Kai Eckert, U Hannover, Germany, 2-7.7.05. Lecture: Quantum information with neutral atoms trapped in optical potentials, 5.7.05.
19. Jean-Yves Béziau, SNSF, U Neuchâtel, Switzerland, 1.7.05. Lecture: Combining conjunction with disjunction.
20. Gilles Brassard, U Montréal, Canada, 28.6-1.7.05. Lecture: The Spooky Power of Quantum Entanglement, 1.7.05.
21. Dick de Jongh, ILLC, U Amsterdam, Netherlands,  13-19.6.05. Lecture: The logic of the Rieger-Nishimura ladder, 17.6.05.
22. Simon Gay, U Glasgow, UK, 7.6.05. Lecture: Probabilistic model-checking of quantum protocols.
23. Claude Crépeau, McGill University, Canada, 26-29.5.05. Lecture: Quantum Zero-Knowledge: state of the art, 27.5.05.
24. João Sobrinho, Instituto de Telecomunicações, Portugal, 6.5.05. Lecture: O M(in)istério da Educação: ou o Problema da Colocação dos Docentes 2004/2005.
25. Andris Ambainis, U Waterloo, Canada, 20-28.4.05. Lecture: Adiabatic theorem and adiabatic quantum algorithms, 22.4.05.
26. Caslav Brukner, U Vienna, Austria, 16-20.4.05. Lecture: How to compute a function without knowing its input? Using quantum entanglement!, 19.4.05.
27. Ana Paula Tomás, LIACC, U Porto, Portugal, 15.4.05. Lecture: Casamentos estáveis e colocação de professores em Portugal.
28. João Marcos, Instituto Superior Técnico, Portugal, 3-10.4.05. Lecture: Paraconsistency, many-valuedness, modality, 8.4.05.
29. Jirí Adámek, TU Braunschweig, Germany, 30-31.3.05. Lecture: A logic of coequations, 31.3.05. 
30. Jörg Flum, U Freiburg, Germany, 18.3.05. Lecture: Parameterized complexity.
31. Beatrix Hiesmayr, U Vienna, Austria, 17-20.2.05. Lecture: Thermodynamical versus optical complementarity, 18.2.05.
32. Karina Roggia, UF Rio Grande do Sul, Brazil, 9-13.2.05. Lecture: Category of partial graphs with total homomorphims: Theory and applications, 11.2.05.
33. Lov Grover, Bell Labs, USA, 2-6.2.05. Lecture: Quantum algorithms, 4.2.05.
34. Ana Bela Cruzeiro, Instituto Superior Técnico e GFM, Portugal, 14.1.05. Lecture: On the equations of motion in quantum mechanics.

4- Seminars

4.1- Logic and Computation Seminar

Organization:  Carlos Caleiro.

1. Luís Russo (INESC)
   Improved indexing of text using the Ziv-Lempel trie, 9/12/05.
2. Luís Cruz-Filipe (Instituto Superior Técnico)
   First-order logic with almost-everywhere quantification, 2/12/05.
3. Rohit Chadha (Instituto Superior Técnico)
   Contract signing, optimism and advantage, 25/11/05.
4. Sara Madeira (INESC and U Beira Interior)
   CCC-biclustering: a linear time biclustering algorithm for time-series gene expression data, 11/11/05.
5. Pedro Lopes (Instituto Superior Técnico)
   Computing minima of colors: beyond the Kauffman-Harary conjecture, 28/10/05.
6. Kerry Ojakian (Instituto Superior Técnico)
   Ramsey lower bounds in bounded arithmetic, 21/10/05.
7. Walter Carnielli (CLE, UniCamp, Brazil)
   Infinite voting, fuzziness and modulated quantifiers, 4/10/05.
8. Dan Ghica (U Birmingham, UK)
   Data-abstraction refinement: a game semantic approach, 20/9/05.
9. Kokichi Futatsugi (JAIST, Japan)
   Formal Methods with CafeOBJ, 13/9/05.
10. Luca Viganò (ETH, Switzerland)
    The AVISPA Tool for the automated validation of internet security protocols and applications, 9/9/05.
11. Daniel Graça (U Algarve)
    On the equivalence of some models of analog computation, 2/9/05.
12. Alessandra di Pierro (U Pisa, Italy)
    Time-based interference and probabilistic padding, 2/9/05.
13. Lutz Schröder (U Bremen, Germany)
    Expressivity of coalgebraic modal logic, 29/7/05.
14. José Carlos Cifuentes (UF Paraná, Brazil)
    Lógica fuzzy e consistência polivalente, 22/7/05.
15. David Basin (ETH, Switzerland)
    Model driven security, 14/7/05.
16. Jean-Yves Béziau (SNSF, U Neuchâtel, Switzerland)
    Combining conjunction with disjunction, 1/7/05.
17. Dick de Jongh (ILLC, U Amsterdam, Netherlands)
    The logic of the Rieger-Nishimura ladder, 17/6/05.
18. Claudio Hermida (Instituto Superior Técnico)
    An accessible approach to behavioural pseudo-metrics, 3/6/05.
19. Luís Cruz-Filipe (Instituto Superior Técnico)
    The essence of proofs when fibring sequent calculi, 13/5/05.
20. João Sobrinho (Instituto de Telecomunicações)
    O M(in)istério da Educação: ou o Problema da Colocação dos Docentes 2004/2005, 6/5/05. Joint session with the Mathematics, Systems and Robotics Seminar. Note the exceptional time and room.
21. Pedro Adão (Instituto Superior Técnico)
    Soundness of formal encryption, 29/4/05.
22. Carlos Caleiro (Instituto Superior Técnico)
    Equipollent logical systems, 22/4/05.
23. Ana Paula Tomás (LIACC, U Porto)
    Casamentos estáveis e colocação de professores em Portugal, 15/4/05.
24. João Marcos (Instituto Superior Técnico)
    Paraconsistency, many-valuedness, modality, 8/4/05.
25. Jirí Adámek (TU Braunschweig)
    A logic of coequations, 31/3/05.
26. Jörg Flum (U Freiburg, Germany)
    Parameterized complexity, 18/3/05.
27. Amílcar Sernadas (Instituto Superior Técnico)
    Proof of the weak completeness of EQPL (conclusion), 11/3/05. Joint session with QCI Seminar. Note the exceptional time and room.
28. Amílcar Sernadas (Instituto Superior Técnico)
    Proof of the weak completeness of EQPL, 4/3/05. Joint session with QCI Seminar.
29. João Rasga (Instituto Superior Técnico)
    Sufficient conditions for cut elimination in first order based calculi, 25/2/05.
30. Karina Roggia (UF Rio Grande do Sul, Brazil)
    Category of partial graphs with total homomorphims: Theory and applications, 11/2/05.
31. Cristina Sernadas (Instituto Superior Técnico)
    Heterogenous fibring of deductive systems via abstract proof (conclusion), 28/1/05.
32. Cristina Sernadas (Instituto Superior Técnico)
    Heterogenous fibring of deductive systems via abstract proof, 21/1/05.

4.2- Working Seminar on Quantum Computation and Information

Organization: Paulo Mateus with José Mourão, Vítor Rocha Vieira and Yasser Omar.
[a joint initiative with CAMGSD, CFIF and CFP, started in September 2003]

1. Sougato Bose (University College London)
   Quantum communication through spin chains and related systems, 13/12/05. Joint seminar with CFIF.
2. Anton Zeilinger (U Vienna)
   From Einstein to Quantum Information, 2/12/05.
3. Markus Arndt (U Vienna)
   Experimental exploration of the quantum/classical transition, 18/11/05.
4. João Rasga (Instituto Superior Técnico)
   Quantum complexity classes - Part II, 4/11/05.
5. João Rasga (Instituto Superior Técnico)
   Quantum complexity classes, 28/10/05.
6. Hélio Pais (Instituto Superior Técnico)
   Quantum string matching, 14/10/05.
7. Paulo Mateus (Instituto Superior Técnico)
   Quantum attacks to zero-knowledge protocols, 23/9/05.
8. Francesco Ciccarello (U Palermo)
   Hot electron noise in n-type GaAs in crossed electric and magnetic fields, 13/9/05. Joint seminar with CFIF, in room P6.
9. Elham Kashefi (IQC, U Waterloo)
   Measurement Calculus, 2/9/05.
10. Umesh Vazirani (U California, Berkeley)
    Quantum algorithms: The non-abelian hidden subgroup problem, 14/7/05.
11. Kai Eckert (U Hannover)
    Quantum information with neutral atoms trapped in optical potentials, 5/7/05.
12. Gilles Brassard (U Montréal)
    The Spooky Power of Quantum Entanglement, 1/7/05.
13. Simon Gay (U Glasgow)
    Probabilistic model-checking of quantum protocols, 7/6/05.
14. Claude Crépeau (McGill University)
    Quantum Zero-Knowledge: state of the art, 27/5/05.
15. Paulo Mateus (Instituto Superior Técnico)
    A process algebra for reasoning about quantum security, 20/5/05.
16. Andris Ambainis (U Waterloo)
    Adiabatic theorem and adiabatic quantum algorithms, 22/4/05.
17. Caslav Brukner (U Vienna)
    How to compute a function without knowing its input? Using quantum entanglement!, 19/4/05.
18. Paulo Mateus (Instituto Superior Técnico)
    Minimization of quantum automata, 1/4/05.
19. Amílcar Sernadas (Instituto Superior Técnico)
    Proof of the weak completeness of EQPL (conclusion), 11/3/05. Joint session with LCSeminar.
20. Amílcar Sernadas (Instituto Superior Técnico)
    Proof of the weak completeness of EQPL, 4/3/05. Joint session with LCSeminar.
21. Beatrix Hiesmayr (U Vienna)
    Thermodynamical versus optical complementarity, 18/2/05.
22. Lov Grover (Bell Labs)
    Quantum algorithms, 4/2/05.
23. Ana Bela Cruzeiro (Instituto Superior Técnico e GFM)
    On the equations of motion in quantum mechanics, 14/1/05.
24. Paulo Mateus (Instituto Superior Técnico)
    Quantum pattern matching using entanglement, 7/1/05.

5- Organization of scientific meetings

The Center maintains a record on the WWW of this type of activity by its members. Two events were organized in 2005:

• The 32nd International Colloquium on Automata, Languages and Programming and Satellite Workshops, FCG and IST, Lisboa, July 11-15 and July 10, 16-17, 2005.
  A. Ravara: Co-organizer.
• International Workshop on Computations on the Continuum, ISA, Lisboa, June 27-28, 2005.
  M. Campagnolo: Co-organizer and host.

Within the scope of the QuantLog project, CLC also contributed to the following CFIF event: 

• Colloquium on the Legacy of Einstein, IST, November 3-30, 2005.

Preparations were initiated towards events to be held after 2005:

• Days in Logic (DiL'08), IST, Lisboa, January 16-18, 2008.
  J. Rasga: Organization chair.
  C. Caleiro: Co-organizer.
• Lisbon Quantum Computation, Information and Logic (LQCIL'07), IST, Lisboa, July 18-20, 2007.
  P. Mateus: Organization chair.
  A. Sernadas: Program chair. 

6- Postdoctoral program

The Center welcomes a few postdoctoral research fellows by promoting applications to the FCT PostDoc Grant Program and also by awarding grants directly.  

During 2005, the following researchers started, continued or concluded their postdocs at the Center:

• Rohit Chadha (PhD in Mathematics, U Penn, USA), since September 2005. Support: CLC September - December 2005 / FCT SFRH/BPD/26137/2005 after January 2006. Supervisors: Amílcar Sernadas and Paulo Mateus.
• Kerry Ojakian (PhD in Mathematics, CMU, USA), since May 2005. Support: FCT SFRH/BPD/16936/2004. Supervisor: Amílcar Sernadas.
• Luís Cruz-Filipe (PhD in Mathematics, University of Nijmegen, The Netherlands), since October 2004. Support: FCT SFRH/BPD/16372/2004. Supervisor: Amílcar Sernadas.
• Claudio Hermida (PhD in Computer Science, University of Edinburgh, UK), since December 1999 (with several interruptions). Support: FCT PRAXIS XXI/BPD/18976/1998 December 1999 - February 2005 / CLC since March 2005. Supervisor: Amílcar Sernadas.

7- Postgraduate program

The Center contributes to the postgraduate program of the Department of Mathematics of IST. It also promotes the work of young members in top research groups abroad. CLC keeps a record of the theses of its student members.

During 2005, the following theses were concluded or in preparation by current CLC student members at the Center or elsewhere:

7.1- PhD theses

Concluded in 2005

• J. Marcos. Logics of Formal Inconsistency. PhD thesis, IFCH, Universidade Estadual de Campinas and IST, Universidade Técnica de Lisboa, 2005. Supervised by W. A. Carnielli and C. Caleiro.
  Get a preprint: 05-M-PhDthesis.pdf 

Ongoing or started in 2005

• P. Adão. Topic: Cleistic Logics of Undistinguishability for Classical and Quantum Protocols. PhD thesis, IST, Universidade Técnica de Lisboa, in preparation. Expected submission: 2006. Supervised by P. Mateus and A. Scedrov.
• D. S. Graça. Topic: Computational Complexity and Dynamical Systems. PhD thesis, IST, Universidade Técnica de Lisboa, in preparation. Expected submission: 2006. Supervised by M. Campagnolo and J. Buescu.
• R. Gonçalves. Topic: Algebraizability of Quantum Logics. PhD thesis, IST, Universidade Técnica de Lisboa, in preparation. Expected submission: 2007. Supervised by C. Caleiro.
• P. Baltazar. Topic: Model Checking of Quantum Systems. PhD thesis, IST, Universidade Técnica de Lisboa, in preparation. Expected submission: 2008. Supervised by P. Mateus.
• L. Camacho. Topic: Colorings of Knots versus Polynomial Invariants. PhD thesis, Universidade da Madeira, in preparation. Expected submission: 2008. Supervised by F. M. Dionísio and P. Lopes.
• T. Reis. Topic: Probabilistic Models in Security. PhD thesis, ETH, Zurich, in preparation. Expected submission: 2009. Supervised by L. Viganò and P. Mateus.
• M. Gamboni. Topic: Models and proof methods for information protection. PhD thesis, IST, Universidade Técnica de Lisboa, in preparation. Expected submission: 2009. Supervised by A. Ravara.

7.2- MSc theses

Concluded in 2005

• P. Baltazar. Variedades M-sólidas de linguagens. Master's thesis, FCUL, Universidade de Lisboa, 2005. Supervised by M. Ramalho.
  Get a preprint: 05-B-MScThesis.pdf 
• P. Ribeiro and F. Nguyen. A new readout method for the quantronium qubit circuit. Technical report, École Polytechnique, 91128 Palaiseau Cedex, France, 2005. DEA Report supervised by D. Esteve.
  Get a preprint: 05-R-DEAReport.pdf 

7.3- Diploma theses

Concluded in 2005

• T. Reis. Quantitative analysis of security protocols. Technical report, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Diploma thesis. Supervised by P. Mateus.
  Get a preprint: 05-R-DiplomaThesis.pdf 

During 2005, CLC members supervised several diploma theses by non-members. It is worthwhile to mention the diploma thesis (Electronic voting) by R. Matias supervised by P. Mateus within the scope of Task 2.

8- Projects

The Center keeps a record of projects with national or international funding. During 2005, members of the Center coordinated or participated in the following research projects:

8.1- QuantLog

FCT Project FEDER POCTI/MAT/55796/2004 (January 1, 2005 - December 31, 2007) 

A joint project of CLC with CFIF, CFP, CEMAT and CAMGSD on quantum computation and information. The main goal of the project is to address and solve some of the many challenging open theoretical problems in the area, as well as to explore some important applications. Significant original results are expected in several aspects of the theory, such as: quantum walks of entangled particles, quantum algorithms in logic, categories of quantum automata and monads, exogenous quantum logic as a combination of logics, compositional analysis of quantum cryptosystems and security protocols. Applications will be investigated mainly for testing the appropriateness of the theoretical techniques, namely concerning zero knowledge proof systems.

Core team (as of December 31, 2005):

• Amílcar Sernadas (General coordinator and Task T3 coordinator) CLC
• Ana Martins CFP
• António Pacheco CEMAT
• Carlos Caleiro (Task T4 coordinator) CLC
• Cláudia Nunes CEMAT
• Claudio Hermida (Research fellow) CLC
• Cristina Sernadas (Task T2 coordinator) CLC
• Jaime Ramos CLC
• João Rasga CLC
• Jorge Almeida CLC
• Luís Cruz-Filipe (Postdoc fellow) CLC
• Paulo Mateus (Task T1 coordinator) CLC
• Pedro Adão (PhD student) CLC
• Pedro Baltazar (PhD student) [+] CLC
• Pedro Ribeiro (PhD student at LPTMC) [+] CLC
• Ricardo Gonçalves (PhD student) CLC
• Rohit Chadha (Postdoc fellow) [+] CLC
• Tiago Reis (PhD student) [+] CLC
• Vítor Rocha Vieira (Task T0 coordinator) CFIF
• Yasser Omar CEMAPRE

[+] since November 2005

Tasks:

• Physics of quantum computation and information (T0)
  pursues specific goals in relevant aspects of quantum physics and provides the foundational support for the whole project. 
• Quantum computation (T1)
  is aimed at developing new quantum algorithms, as well as at establishing abstract results in computational complexity. 
• Quantum automata (T2)
  is directed at developing the categorical theory of quantum automata, ultimately aiming at model checking of quantum algorithms and protocols. 
• Logics for quantum reasoning (T3) 
  is focused on the development of a new quantum logic endowed with a semantics based on superpositions of classical valuations, having in mind the specification and verification of quantum protocols.
• Quantum cryptography and security (T4)
  is mainly devoted to applications in cryptography and security, with emphasis on zero knowledge proof systems

8.2- Space-Time-Types

Project POSC/EIA/55582/2004 (March 1, 2005 - February 29, 2008) funded by FEDER and FCT. 

A joint initiative of CLC and CITI aimed at developing new type systems to statically verify behavioural and structural properties of global, distributed open systems. We shall pursue our previous work on three inter-related subjects: non-uniform types for concurrent objects, investigating decidability issues; session types for component interoperability, investigating their extension to multi-party protocols; spatial types, investigating static analyses methods to prove not only behavioural and but also structural properties of distributed systems. Moreover, we plan to study the relationship between behavioural and session types, looking for a unified notion and system, and to relate spatial to behavioural types, characterising the latter in terms of the former.

Core team:

• Luís Caires 
• António Ravara (Coordinator)
• Vasco T. Vasconcelos 

Tasks:

• Non-uniform Types
  The specific goal of this task is the study of the use of behavioural types in several contexts: (1) In systems of concurrent objects, looking for a decidable notion of simulation which coincides with subtyping, and then defining a type inference algorithm for a non-uniform type system to a mobile calculus of objects. (2) In a framework allowing the definition of a single type system using tailored subtyping relation to check several properties which are now treated separately, each by a particular system with a specific notion of type. These properties are: no arity mismatch in the use of channels; enforcement of input/output or linear use of channels, message immediately or eventually understood, absence of orphan messages.
• Session Types
  The specific goal of this task is the development of type systems which allow complex protocols to be specified in a high-level manner, and support verification by relatively straightforward static type-checking. In previous work we have used session types to specify the dynamic communication between components. We have also studied precise definitions of compatibility and substitutability tests, which form the basis of efficient static checks that components will interact correctly. Our aims are now twofold: (1) To further develop the framework of session types, extending them from dyadic to multiparty interactions. (2) To equip our experimental concurrent functional language with object-oriented constructs.
• Spatial Types
  The specific goal of this task is the definition of a decidable proof system to statically verify spatial and behavioural properties of processes (notice that model-checking is restricted to finite reachability). Following the approach "propositions as types", the types are spatial logic formulae, subtyping is logical entailment, and the type system is a deductive system. We want to capture an expressive sublanguage of spatial logics, which allow us to specify and verify the referred properties, keeping the proof system decidable.

8.3- ConTComp

A project of CLC on the complexity of continuous time computation and, in particular, on real recursive functions and continuous dynamical systems, such as continuous time neural network and analog circuits.

Core team:

• Manuel Lameiras Campagnolo (Coordinator)
• Paula Gouveia
• Daniel Graça
• Carlos Lourenço
• Kerry Ojakian (since July 2005)

Tasks:

• Real recursive functions
  • Algebraic properties of the relations between analog and standard notions of complexity.
  • Analog characterizations of low time complexity classes.
  • Links between problems in computational complexity and in the the theory of differential equations.
  • Real recursive functions and continuous dynamical systems.
• Continuous dynamical systems
  • Neural networks with complex spatiotemporal dynamics.
  • Analog circuits.

8.4- Sensoria

Sensoria: Software Engineering for Service-Oriented Overlay Computers, is an EU Information Society Technologies integrated project funded by the 6th framework programme as part of the Global Computing Initiative (September 1, 2005 - August 31, 2009).

The goal of Sensoria is to generalise the concept of service in such a way that: it is independent from the particular global computer and from any programming language; it can be described in a modular way, so that security issues, quality of service measures and behavioural guarantees are preserved under composition; it supports dynamic, ad-hoc, "just-in-time" composition; it can be made part of an integrated service-oriented approach to business modelling.

Work at CLC by António Ravara will focus on mathematical analysis techniques for specifying and ensuring behavioural properties of services. The main contributions are: (1) notions of types able of providing descriptions of contract definitions and services composition; (2) type systems to statically ensure safety properties of foundational calculi for service-oriented computing.

8.5- Multiparticle quantum walks and their algorithmic applications

Anglo-Portuguese Joint Research Programme, Treaty of Windsor B22/05 and B44/06, 2005-2006, between

• Sougato Bose (University College London), 
  Martin Plenio (Imperial College),
  Vlatko Vedral (University of Leeds),
• Paulo Mateus (CLC and Department of Mathematics, IST) and
  Yasser Omar (CEMAPRE and Department of Mathematics, ISEG).

The main goal of the  project is to study multiparticle quantum walks. Original contributions are expected in the area of quantum walks, namely:  the role of entanglement; effects of particle statistics; and applications to the development of new efficient quantum search algorithms. 

8.6- Communication protocols in session types

Anglo-Portuguese Joint Research Programme, Treaty of Windsor B29/05, 2005-2006, between

• Simon Gay (Department of Computing Science, University of Glasgow), and
• António Ravara (CLC and Department of Mathematics, IST, Technical University of Lisbon) and
  Vasco T. Vasconcelos (Department of Informatics, Faculty of Sciences, University of Lisbon).

The goal of the project is to develop of a framework to specify and statically verify multiparty communication protocols. Software systems consist in collections of components assembled together, although possibly written by different people and in different programming languages. These systems may even be distributed and relying in a communication infrastructure to interoperate. The integration of these components poses difficult problems. The protocol that the components should followed on their interaction must be rigorously specified, and formally verified, not only dynamically, but more important, statically. Specifically, we aim at the development of type systems which support the specification and verification of complex interactions between agents in a concurrent and distributed system. Examples of such interactions are network communication protocols, client-server protocols, and the correct use of high-level data structures implemented by objects.

8.7- Calculabilité et complexité des modèles de calculs à temps continu

• Olivier Bournez (LORIA)
• Manuel Lameiras Campagnolo (CLC and Department of Mathematics, ISA, Technical University of Lisbon)
• Daniel Silva Graça (CLC and Department of Mathematics, Faculty of Science and Technology, University of Algarve)
• Emmanuel Hainry (LORIA)

Goals:

• computational properties of continuous-time models of computation;
• analog machines;
• verification methods for continuous systems.

9- Invited talks and communications

The Center maintains a record on the WWW of the talks given by its members since 1998 in conferences and research centers.

During 2005, in total, 26 communications were given at international conferences and meetings, 1 communication was given at a national meeting, and 17 talks were given in departmental seminars elsewhere:

1. Association for Symbolic Logic 2005-2006 Winter Meeting, New York, USA, December 27-29, 2005.
   J. Marcos: Generalizing truth-functionality.
   (talk given by Arnon Avron due to the absence of J. Marcos)
2. Workshop on Classical and Quantum Information Security, California Institute of Technology, Pasadena, USA, December 15-18, 2005.
   P. Mateus: A process algebra for reasoning about quantum security.
3. Security Lunch Seminar, Stanford University, USA, December 14, 2005.
   P. Mateus: Towards a logic for reasoning about quantum systems.
4. Quantum Reading Group, University of Berkeley, USA, December 9, 2005.
   P. Mateus: Quantum adversaries for zero-knowledge proof systems.
5. Seminário do Departamento de Matemática, Universidade de Aveiro, Portugal, November 24, 2005.
   R. Gonçalves: Sobre a algebrização da semântica das valorações.
6. Microsoft Research Seminar, Cambridge, UK, November 23, 2005.
   P. Adão: Cryptographically sound implementations for communicating processes.
7. Category Theory and Logic Seminar, McGill University, Montreal, Canada, November 1, 2005.
   C. Hermida: Descent on 2-fibrations and strong 2-regularity.
8. Security Group Meeting, University of Cambridge, UK, October 28, 2005.
   P. Adão: How concrete is the Dolev-Yao model?
9. Seminário de Lógica Matemática, IST/FCUL, Lisboa, Portugal, October 25 and November 8, 2005.
   A. Sernadas: Complete axiomatization of EQPL (Exogenous Quantum Propositional Logic).
10. Category Theory Octoberfest '05, University of Ottawa, Canada, October 22-23, 2005.
    C. Hermida: Descent on 2-fibrations and strongly 2-regular 2-categories.
11. Brouwer Seminar, Nijmegen, Netherlands, October 5, 2005.
    L. Cruz-Filipe: The essence of proofs in sequent calculi.
12. VerSePro Kick-off Meeting, Oberdof, Switzerland, October 4-5, 2005.
    P. Mateus: Probabilistic logics for security analysis.
13. Encontro dos Algebristas Portugueses 2005, Braga, Portugal, September 22-24, 2005.
    R. Gonçalves: On the algebraization of valuation semantics.
14. 10th European Symposium on Research in Computer Security (ESORICS 2005), Milan, Italy, September 12-14, 2005.
    P. Adão: Soundness of formal encryption in the presence of key-cycles.
15. Workshop on Categorical Methods in Algebra, Geometry and Physics, Canberra, Australia, July 17-21, 2005.
    C. Hermida: 2-descent and strongly 2-regularity.
16. CALCULEMUS Workshop 2005 (Affiliated Workshop of FM'05), Newcastle-upon-Tyne, UK, July 18-19, 2005.
    L. Cruz-Filipe: Executing extracted programs.
17. Structures and Deduction - The Quest for the Essence of Proofs (Affiliated Workshop of ICALP 2005), Lisbon, Portugal, July 16-17, 2005.
    J. Rasga: Cut elimination in propositional based logics.
18. 4th International Workshop on Proof Theory, Computation, Complexity (Affiliated Workshop of ICALP 2005), Lisbon, Portugal, July 16-17, 2005.
    J. Rasga: Complexity analysis of cut elimination in first order based logics.
19. 2nd Workshop on Automated Reasoning for Security Protocol Analysis (Affiliated Workshop of ICALP 2005), Lisbon, Portugal, July 16, 2005.
    C. Caleiro: Deconstructing Alice and Bob.
20. 3rd International Workshop on Quantum Programming Languages (QPL 2005), Chicago, IL, USA, June 30-July 1, 2005.
    P. Adão: A Process algebra for reasoning about quantum security.
21. International Workshop on Computations on the Continuum, Lisbon, Portugal, June 27-28, 2005.
    D. S. Graça: Computability in the general purpose analog computer.
    C. Lourenço: Natural computing with continuous-time chaotic neural nets.
22. LICS 2005 Short Presentations, Chicago, USA, June 26-29, 2005.
    P. Mateus: Complete exogenous quantum propositional logic.
23. 18th IEEE Computer Security Foundations Workshop (CSFW 2005), Aix-en-Provence, France, June 20-22, 2005.
    P. Adão: Computational and information-theoretic soundness and completeness of formal encryption.
24. Natural Processes and Models of Computation, Bologna, Italy, June 16-18, 2005.
    D. S. Graça: Discrete-time and continuous-time analog computation.
25. Meeting on Algebraic and Topological Methods in Non-Classical Logics II, Barcelona, Spain, June 15-18, 2005.
    R. Gonçalves: On the algebraization of valuation semantics.
26. CiE 2005 New Computational Paradigms, Amsterdam, Netherlands, June 8-12, 2005.
    D. S. Graça: Robust simulations of Turing machines with analytic maps and flows.
27. Complexité, Modèles Finis et Bases de Données & Journées d'Arithmétique Faible (JAF 24), Fontainebleau, France, May 26-28, 2005.
    D. S. Graça: Computing with continuous-time analog circuits.
28. Seminario Dipartimento di Informatica, Università di Pisa, Italy, May 18, 2005.
    C. Hermida: A categorical outlook on simulation and relational modalities.
29. 81st Peripatetic Seminar on Sheaves and Logic, Coimbra, Portugal, April 9-10, 2005.
    C. Hermida: Descent on 2-fibrations and strongly 2-regular 2-categories.
    P. Mateus: Minimization of quantum automata.
30. 1st World Congress on Universal Logic, Montreux, Switzerland, March 31 - April 3, 2005.
    C. Caleiro: Equipollent logical systems.
    R. Gonçalves: On the algebraization of valuation semantics.
31. 1st World School on Universal Logic, Montreux, Switzerland, March 26-30, 2005.
    C. Caleiro: Combining logics.
32. Seminário de Álgebra, CMUC, Coimbra, Portugal, March 15, 2005.
    A. Sernadas: Proof of the weak completeness of EQPL.
33. Séminaire Groupe de Travail MC2, École Normale Supérieure de Lyon, France, March 2, 2005.
    D. S. Graça: Robust simulations of Turing machines with analytic maps and flows.
34. Seminário de Ciência da Computação, IME, Universidade de São Paulo, Brazil, February 18, 2005.
    C. Caleiro: Metareasoning about security protocols using distributed temporal logic.
    J. Rasga: The complexity of cut elimination in a modal sequent calculus labelled with truth values.
35. Colloquia Logicae, CLE, Universidade Estadual de Campinas, Brazil, February 17, 2005.
    C. Caleiro: Dyadic semantics for many-valued logics.
    J. Rasga: The complexity of cut elimination in a modal sequent calculus labelled with truth values.
36. Second Theory of Cryptography Conference (Rump Session) (TCC 2005), MIT, Cambridge, MA, USA, February 10-12, 2005.
    P. Adão: Soundness of formal encryption in the presence of key cycles.
37. Séminaire PROTHEO, LORIA/INRIA, Nancy, France, February 10, 2005.
    D. S. Graça: A digression over the General Purpose Analog Computer.
38. Séminaire Informatique Fondamentale, LORIA/INRIA, Nancy, France, February 3, 2005.
    M. Campagnolo: Real recursive functions and their hierarchies: structural and computational complexity.
39. Protocol eXchange Seminar, Naval Postgraduate School, Monterey, CA, USA, February 1-2, 2005.
    P. Adão: Key cycles and formal encryption.

10- Publications

The Center maintains an archive on the WWW of the publications of its current members since 1980 with a search facility.

In total, CLC members (as of December 31, 2005) published, during 2005, 13 articles in international jouranls and serials, 8 chapters in internationally published books, and 4 articles in proceedings of international conferences. The full list follows, including submitted and accepted papers during 2005:

10.1- Publications by current members appeared in 2005

10.1.1- Articles in international journals with refereeing

1. C. Caleiro, L. Viganò, and D. Basin. Deconstructing Alice and Bob. Electronic Notes in Theoretical Computer Science, 135(1):3--22, 2005. Preliminary version presented at ICALP'05 ARSPA Workshop.
   Get a preprint: 05-CVB-alice&bob.pdf 
2. C. Caleiro, L. Viganò, and D. Basin. Metareasoning about security protocols using distributed temporal logic. Electronic Notes in Theoretical Computer Science, 125(1):67--89, 2005. Preliminary version presented at IJCAR'04 ARSPA Workshop.
   Get a preprint: 04-CVB-fiblog15s2.pdf 
3. C. Caleiro, L. Viganò, and D. Basin. Relating strand spaces and distributed temporal logic for security protocol analysis. Logic Journal of the IGPL, 13(6):637--664, 2005.
   Get a preprint: 04-CVB-fiblog15s3.pdf 
4. R. Chadha, J. Mitchell, A. Scedrov, and V. Shmatikov. Contract signing, optimism and advantage. Journal of Logic and Algebraic Programming (Special issue on Modeling and Verification of Cryptographic Protocols), 64(2):189--218, 2005. Full version of rchadha:mit:sce:shmat:03.
   Get a preprint: 04-CMSS-advantage.pdf 
5. J. Marcos. Logics of essence and accident. Bulletin of the Section of Logic, 34(1):43--56, 2005.
   Get a preprint: 04-M-LEA.pdf 
6. J. Marcos. Nearly every normal modal logic is paranormal. Logique et Analyse, 48:279--300, 2005.
   Get a preprint: 04-M-Paranormal.pdf 
7. J. Marcos. On negation: Pure local rules. Journal of Applied Logic, 3(1):185--219, 2005.
   Get a preprint: 04-M-onplr.pdf 
8. P. Mateus, J. Rasga, and C. Sernadas. Modal sequent calculi labelled with truth values: Cut elimination. Logic Journal of the IGPL, 13(2):173--199, 2005.
   Get a preprint: 04-MRS-fiblog20.ps  04-MRS-fiblog20.pdf 
9. K. Ojakian. Upper and lower ramsey bounds in bounded arithmetic. Annals of Pure and Applied Logic, 135:135--150, 2005.
   Get a preprint: 05-O-ramsey.pdf 

10.1.2- Articles in international serials with refereeing

1. P. Adão, G. Bana, J. Herzog, and A. Scedrov. Soundness of formal encryption in the presence of key-cycles. In S. De Capitani di Vimercati, P. Syverson, and D. Gollmann, editors, Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS), volume 3679 of Lecture Notes in Computer Science, pages 374--396. Springer-Verlag, 2005.
   Get a preprint: 05-ABHS-cycles.pdf 
2. C. Caleiro and J. Ramos. Cryptomorphisms at work. In J. Fiadeiro, P. Mosses, and F. Orejas, editors, Recent Trends in Algebraic Development Techniques - Selected Papers, volume 3423 of Lecture Notes in Computer Science, pages 45--60. Springer-Verlag, 2005.
   Get a preprint: 04-CR-fiblog17.ps  04-CR-fiblog17.pdf 
3. D. S. Graça, M. L. Campagnolo, and J. Buescu. Robust simulations of Turing machines with analytic maps and flows. In B. Cooper, B. Löwe, and L. Torenvliet, editors, Proceedings of CiE'05, New Computational Paradigms, volume 3526 of Lecture Notes in Computer Science, pages 169--179. Springer-Verlag, 2005.
   Get a preprint: 05-GCB-stable.ps  05-GCB-stable.pdf 
4. F. van Breugel, C. Hermida, M. Makkai, and J. Worrel. An accessible approach to behavioural pseudo-metrics. In L. Caires, G. F. Italiano, L. Monteiro, C. Palamidessi, and M. Yung, editors, Automata, Languages and Programming ICALP'05, volume 3580 of Lecture Notes in Computer Science, pages 1018--1030. Springer-Verlag, 2005.

10.1.3- Articles in international collections with refereeing

1. C. Caleiro and R. Gonçalves. Equipollent logical systems. In J.-Y. Béziau, editor, Logica Universalis, pages 99--112. Birkhäuser Verlag, 2005.
   Get a preprint: 05-CG-equipollence.pdf 
2. C. Caleiro, W. A. Carnielli, M. E. Coniglio, and J. Marcos. Two's company: ``The humbug of many logical values". In J.-Y. Béziau, editor, Logica Universalis, pages 169--189. Birkhäuser Verlag, 2005.
   Get a preprint: 05-CCCM-dyadic.pdf 
3. C. Caleiro, W. A. Carnielli, J. Rasga, and C. Sernadas. Fibring of logics as a universal construction. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, 2nd Edition, volume 13, pages 123--187. Springer, 2005.
   Get a preprint: 04-CCRS-fiblog23.pdf 
4. C. Caleiro, A. Sernadas, and C. Sernadas. Fibring logics: Past, present and future. In S. Artemov, H. Barringer, A. S. d'Avila Garcez, L. C. Lamb, and J. Woods, editors, We Will Show Them: Essays in Honour of Dov Gabbay, Volume One, pages 363--388. King's College Publications, 2005.
   Get a preprint: 05-CSS-fiblog27.pdf 
5. F. M. Dionísio, P. Gouveia, and J. Marcos. Defining and using deductive systems with Isabelle. In L. Magnani and R. Dossena, editors, Computing, Philosophy, and Cognition, pages 271--293. King's College Publications, 2005.
   Get a preprint: 04-DGM-dlogisa.pdf 
6. J. Marcos. Modality and paraconsistency. In M. Bilkova and L. Behounek, editors, The Logica Yearbook 2004, pages 213--222. Filosofia, 2005.
   Get a preprint: 04-M-ModPar.pdf 
7. J. Marcos. On a problem of da Costa. In G. Sica, editor, Essays on the Foundations of Mathematics and Logic, volume 2, pages 39--55. Polimetrica, 2005.
   Get a preprint: 05-M-P12.pdf 
8. P. Mateus, A. Sernadas, and C. Sernadas. Exogenous semantics approach to enriching logics. In G. Sica, editor, Essays on the Foundations of Mathematics and Logic, volume 1, pages 165--194. Polimetrica, 2005.
   Get a preprint: 05-MSS-quantlog03.pdf 

10.1.4- Articles in proceedings of international conferences with refereeing

1. P. Adão, G. Bana, and A. Scedrov. Computational and information-theoretic soundness and completeness of formal encryption. In Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW), pages 170--184, Aix-en-Provence, France, June 20-22, 2005. IEEE Computer Society Press.
   Get a preprint: 04-ABS-encryption.pdf 
2. M. Alves and C. Lourenço. Selenoprotein discovery using neural networks. In N. Guimarães and P. Isaías, editors, Proceedings of the International Conference on Applied Computing (IADIS'05), pages 519--526, Algarve, Portugal, February 22-25, 2005.
   Get a preprint: 05-AL-iadis.pdf 
3. S. Costa, C. Cardeira, J. Pargana, F. M. Dionísio, and P. A. Santos. Systems and signals online questions and grading. In Lucia lo Bello and Thile Sauter, editors, Proceedings of the 10th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2005), pages 41--47. IEEE, 2005. Special Session on E-learning and Remote Laboratories.
   Get a preprint: 05-CCPDS-ssoqg.pdf 
4. J. Rasga. Cut elimination in propositional based logics. In P. Bruscoli, F. Lamarche, and C. Stewart, editors, Proceedings of Structures and Deduction - the Quest for the Essence of Proofs (satellite workshop of ICALP 2005), pages 205--214. Technische Universität Dresden, 2005.
   Get a preprint: 05-R-quantfib2s.pdf 

10.1.5- Other publications

1. C. Caleiro and R. Gonçalves. On the algebraization of valuation semantics. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Presented at 1st World Congress on Universal Logic, Montreux, Switzerland, March 31 - April 3, 2005. Extended abstract. Full version to be submitted.
   Get a preprint: 05-CG-valuation.pdf 
2. W. A. Carnielli and P. Mateus, editors. Selected papers from CombLog'04, volume 13(6) -- Special issue of Logic Journal of the IGPL, 2005.
3. J. Marcos, D. Batens, and W. A. Carnielli, editors. A Paraconsistent Decagon, volume 3(1) -- Special issue of Journal of Applied Logic, 2005.
4. P. Mateus and A. Sernadas. Complete exogenous quantum propositional logic. Technical report, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Extended abstract. Short presentation at LICS 2005, Chicago, USA, June 26-29.
   Get a preprint: 05-MS-quantlog01sp.pdf 
5. J. Rasga. Complexity analysis of cut elimination in first order based logics. Technical report, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Extended abstract. Presented at PCC -- Proof, Computation, Complexity, July 16-17, Lisboa, Affiliated Workshop of ICALP 2005.
   Get a preprint: 05-R-quantfib04s.pdf 

10.2- Publications by current members accepted in 2005

1. O. Bournez, M. L. Campagnolo, D. S. Graça, and E. Hainry. The General Purpose Analog Computer and Computable Analysis are two equivalent paradigms of analog computation. In J.-Y. Cai, S. B. Cooper, and A. Li, editors, Theory and Applications of Models of Computation TAMC'06, volume 3959 of Lecture Notes in Computer Science, pages 631--643. Springer-Verlag, in print.
   Get a preprint: 06-BCGH-tamc.pdf
2. C. Caleiro, P. Mateus, A. Sernadas, and C. Sernadas. Quantum institutions. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, editors, Festschrift, Lecture Notes in Computer Science. Springer-Verlag, in print.
   Get a preprint: 05-CMSS-quantlog06.pdf 
3. W. A. Carnielli, M. E. Coniglio, and J. Marcos. Logics of formal inconsistency. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 14. Kluwer Academic Publishers, 2nd edition, in print.
   Get a preprint: 03-CCM-lfi.pdf
4. J. M. B. Carreiras, J. M. C. Pereira, M. L. Campagnolo, and Y. E. Shimabukuro. Assessing the extent of agriculture/pasture and secondary succession forest in the Brazilian Legal Amazon using SPOT VEGETATION data. Remote Sensing of Environment, 101:283--298, in print.
   Get a preprint: 06-CPCS-amazon.pdf
5. R. Chadha, S. Kremer, and A. Scedrov. Formal analysis of multi-party contract signing. Journal of Automated Reasoning (Special Issue on Automated Reasoning for Security Protocol Analysis), in print. Full version of rchadha:skr:sce:04.
   Get a preprint: 05-CKS-jar.pdf 
6. R. Chadha, D. Macedonio, and V. Sassone. A hybrid intuitionistic logic: semantics and decidability. Journal of Logic and Computation (Special issue on Logics for Resources, Processes and Programs), in print.
   Get a preprint: 05-CMS-jlc.pdf 
7. L. Cruz-Filipe and P. Letouzey. A large-scale experiment in executing extracted programs. Electronic Notes in Theoretical Computer Science, in print. To be presented at CALCULEMUS 2005, July 18-19, 2005, Newcastle upon Tyne, Affiliated Workshop of Formal Methods 2005.
   Get a preprint: 05-CL-extrcomp.ps  05-CL-extrcomp.pdf 
8. P. Mateus and Y. Omar. A quantum algorithm for closest pattern matching. In D. Angelakis and M. Christandl, editors, Proceedings of NATO ASI Quantum Computation and Information, Chania, Crete, Greece, May 2-13, in print. IOS Press. Short version of pmat:yo:05.
   Get a preprint: 05-MO-quantlog05s.pdf 
9. P. Mateus and A. Sernadas. Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation, in print. ArXiv math.LO/0503453.
   Get a preprint: 05-MS-quantlog01.pdf 
10. P. Adão and P. Mateus. A process algebra for reasoning about quantum security. Electronic Notes in Theoretical Computer Science, to appear. Preliminary version to be presented at 3rd International Workshop on Quantum Programming Languages, June 30 - July 1, 2005, Chicago, Affiliated Workshop of LICS 2005.
    Get a preprint: 05-AM-quantlog04.pdf 
11. J. Marcos. Possible-translations semantics for some weak classically-based paraconsistent logics. Journal of Applied Non-Classical Logics, to appear.
    Get a preprint: 04-M-PTS4swcbPL.pdf 
12. J. Marcos. Ineffable inconsistencies. In J.-Y. Béziau and W. A. Carnielli, editors, Paraconsistency with no Frontiers, Proceedings of the III World Congress on Paraconsistency, held in Toulouse, FR, July 28-31, 2003, volume 4 of Studies in Logic and Practical Reasoning, pages 301--311. Elsevier Science, Amsterdam, in print.
    Get a preprint: 04-M-ii.pdf 
13. A. Vallecillo, V. T. Vasconcelos, and A. Ravara. Typing the behavior of software components using session types. Fundamenta Informaticae, to appear. Full version of val:vv:amar:02.
    Get a preprint: 05-VVR-compsessions.pdf 

10.3- Publications by current members submitted in 2005

1. P. Adão, G. Bana, J. Herzog, and A. Scedrov. Soundness and completeness of formal encryption: the cases of key-cycles and partial information leakage. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
   Get a preprint: 05-ABHS-encryption-cycles.ps  05-ABHS-encryption-cycles.pdf 
2. P. Baltazar. M-solid varieties of languages. Preprint, CAUL, Department of Mathematics, Universidade de Lisboa, 2005. Submitted for publication.
   Get a preprint: 05-B-msolid.pdf 
3. C. Caleiro and J. Ramos. From fibring to cryptofibring: a solution to the collapsing problem. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
   Get a preprint: 05-CR-fib2crypto.pdf
4. C. Caleiro, L. Viganò, and D. Basin. On the expresiveness of a message sequence formalism for security protocols. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
   Get a preprint: 05-CVB-expressiveness.pdf 
5. R. Chadha, P. Mateus, A. Sernadas, and C. Sernadas. Extending classical logic for reasoning about quantum systems. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
   Get a preprint: 05-CMSS-quantlog07.pdf 
6. L. Cruz-Filipe and C. Sernadas. Sequent calculi based on derivations. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
   Get a preprint: 05-CS-quantfib01.pdf 
7. L. Cruz-Filipe, A. Sernadas, and C. Sernadas. Heterogeneous fibring of deductive systems via abstract proof systems. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication.
   Get a preprint: 05-CSS-fiblog26.pdf 
8. C. Lourenço. Dynamical reservoir properties as network effects. In M. Verleysen, editor, Proceedings of the 14th European Symposium on Artificial Neural Networks (ESANN'06), Bruges, Belgium, April 26-28, in print. ESANN.
9. J. Rasga. Cut elimination for a class of propositional based logics. Preprint, CLC, Department of Mathematics, Instituto Superior Técnico, 1049-001 Lisboa, Portugal, 2005. Submitted for publication. Full version of jfr:05a.
   Get a preprint: 05-R-quantfib2.pdf 

11- Awards and distinctions

During 2005, the following distinctions were awarded to CLC members:

1. R. Gonçalves, PGEI research grant from Fundação Calouste Gulbenkian, 2005.
2. L. Cruz-Filipe and P. Letouzey, CALCULEMUS Workshop 2005 (Affiliated workshop of FM'05), Newcastle-upon-Tyne, UK, July 18-19, 2005. Winner of best paper award. A large-scale experiment in executing extracted programs.
3. C. Caleiro and R. Gonçalves, 1st World Congress on Universal Logic, Montreux, Switzerland, March 31 - April 3, 2005. Winner of the best paper contest about "How to define identity between logics?". Equipollent logical systems.

The work Análise de sistemas de prova de conhecimento nulo was submitted by P. Mateus to the Portuguese IBM Scientific Prize 2005. This work has been awarded the prize and the formal ceremony will take place in 2006.