Changes between Version 1 and Version 2 of Proposal2.2

Jun 15, 2010, 1:03:04 PM (10 years ago)



  • Proposal2.2

    v1 v2  
    1 === UNIBO ===
     1=== Beneficiaries ===
    3 The Department of Computer Science of the University of Bologna covers a wide range of research areas in the field of Information and Communication Technologies, with particular emphasis on distributed and real time system, and theory and implementation of programming languages. The HELM team, active since year 2000 and coordinated by Prof. Asperti, is focused on the study and implementation of tools and techniques for the automation of formal reasoning, and the certification of software properties, resulting in the recent release of the interactive theorem prover.
     3  * [wiki:UNIBO]
     4  * [wiki:UPD]
     5  * [wiki:UEDIN]
    5 == Role in the project and main tasks ==
     7== Consortium as a whole ==
    7 UNIBO is the Project coordinator, hence responsible for the Project Management activities of WPround(0+1:0). It is also responsible for WPround(3+1:0), namely the development of the certified back-end of the CerCo compiler and WPround(5+1:0)dissemination and exploitation. It will also actively participate to the design and implementation of the untrusted prototype compiler (WPround(1+1:0)) and the management of complexity assertions and automation of complexity proofs (WPround(4+1:0)).
     9The participants to the consortium group together the minimal set of skills, know how and resources capable of achieving the project objectives. The project lies at the intersection between complexity, formal checking and compilers, requiring not only experts of the three fields, but also people with some knowledge and sensibility towards all the different topics.
    9 == Relevant previous experience (Formalization and Management of Knowledge) ==
     11The main research field of UNIBO is currently on tools and techniques for the automation of formal reasoning, and especially on the development of the new Interactive Theorem Prover Matita and its applications to correctness proofs for critical software applications. The group has direct experience on the formalization of micro-controllers in Matita, as testified by an executable specification for all models of Freescale 8bit micro-controllers available at the address� The formalization captures all ALU families (Families HC05/HC08/RS08/HCS08) and all kind of memories that can be installed (RAM, ROM, Flash). The formalization comprise the computational cost of every machine operation, allowing to reason at the level of granularity of single clock cycles. An OCaml emulator running at reasonable speed has also been automatically extracted from the executable specification. In addition, the UNIBO site has past didactical and experimental experience in compiler construction, and good knowledge of complexity theory. In particular, Andrea Asperti held the chair in Programming Languages and Compilers in the period 1992-2000, writing scientific and didactical monographs on the topics,[[footnode.html#foot700|^6^]] and is currently teaching Computability and Complexity Theory.
    11   * European projects: EU Project IST-2001-33562 MoWGLI (coordinator: Prof. Andrea Asperti; WP leader: Dr. Claudio Sacerdoti Coen), EU Project IST-2001-37057 MKM-NET (member), TMR-Network LINEAR (member)
    12   * Recent national and local projects: PRIN 2002-06 McTafi (national, member), DAMA (Strategic Project of Universiy of Bologna; coordinator: Dr. Claudio Sacerdoti Coen), ``Formalization of Formal Topology by means of the interactive theorem prover Matita'' (Strategic Project of the University of Padova; member)
     13The present research focus of UPD is mostly on complexity aspects, and resource control for real time systems, but they are expert in compiler construction, and comprise members with good experience in the use of interactive provers. In particular, Roberto Amadio is currently teaching a course on Syntax Analysis and Compilers at the University of Paris Diderot and he recently coordinated the National Project�amadio/Criss/criss.htmlCriss, comprising the development of a small�amadio/Criss/shape-analysis.htmlcompiler for a first order functional language, producing bytecode annotated with relevant complexity information using shape analysis. This compiler was programmed in OCaml.
    14 == Staff members involved (UNIBO) ==
     15Finally, UEDIN offers much experience in the theory and implementation of programming languages, with particular emphasis on the formal engineering of their metatheory. Randy Pollack is the author of LEGO, a well known Interactive Prover of the nineties (no longer maintained) that was used by many students and researchers. Prior to that, Pollack had been an industrial software engineer specializing in real-time systems. He is currently working in the Mobility and Security Group at UEDIN, which has participated in 2 recent EU projects on formal certification of resource properties.[[footnode.html#foot925|^7^]] Pollack was also on the steering committee of the recently completed EU Coordination Action In addition, UEDIN has significant research groups in areas of complexity and compilers.
    16 || Claudio Sacerdoti Coen || Researcher University of Bologna ||
    17 || Andrea Asperti || Professor University of Bologna ||
    18 || Research fellow (24 months) || to be hired with project fundings ||
    19 || PostDoc (24 months) || to be hired with project fundings ||
     17All the partners have previously worked, alone or together, in European projects of different nature and sizes, including RTD projects. The above mentioned projects have successfully completed, demonstrating the capabilities of the CerCo partners of carrying out projects of European dimension, as well as their positive attitude to collaborative work. In many cases, the partners CerCo Consortium have acted as project coordinators; as such, they are well aware of execution and management policies of EU-funded projects. [[BR]]
    21 === Key person ===
     19=== Sub-contracting ===
    23 Claudio Sacerdoti Coen was born in 1976. He got a Ph.D. in Computer Science by the University of Bologna in 2004. After a Post-Doc at INRIA-Futurs (FR), he became a Ricercatore (permanent researcher) in Computer Science at the University of Bologna, where he has been teaching Operating Systems and Logic. His main research interests are the development of interactive theorem provers, their application to the formalization of mathematics, and knowledge management of formal mathematics. He is the author of over 30 peer-reviewed publications in mathematical knowledge management, type theory and automated reasoning. Recent publications relevant to the project comprise:
    25   1. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi. A compact kernel for the calculus of inductive constructions. In Special Issue on Interactive Proving and Proof Checking of the Academy Journal of Engineering Sciences (Sadhana) of the Indian Academy of Sciences. SADHANA. vol. 34(1), pp. 71-144, 2009.
    26   1. A.Asperti, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli. User Interaction with the Matita Proof Assistant. Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving, 39(2), pp.109-139, 2007.
    27   1. C.Sacerdoti Coen. Declarative Representation of Proof Terms. In Special Issue on Programming Languages for Mechanized Mathematical Systems, Journal of Automated Reasoning, to appear in 2009.
     21Subcontractors will only be used for production of Certificates of Financial Statements, as required by FP7 rules. Other subcontracting has not resulted to be necessary since all competences required for carrying out the action are represented within the consortium. [[BR]]