wiki:Proposal2.2.1

Version 1 (modified by sacerdot, 7 years ago) (diff)

--

UNIBO

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 http://matita.cs.unibo.it/Matita interactive theorem prover.

Role in the project and main tasks

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

Relevant previous experience (Formalization and Management of Knowledge)

  • 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)
  • 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)

Staff members involved (UNIBO)

Claudio Sacerdoti Coen Researcher University of Bologna
Andrea Asperti Professor University of Bologna
Research fellow (24 months) to be hired with project fundings
PostDoc? (24 months) to be hired with project fundings

Key person

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:

  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.
  2. 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.
  3. 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.