Claudio Sacerdoti Coen

He designs and implements the interactive theorem prover Matita (http://matita.cs.unibo.it). He coordinates an european project on the development and certification of a C compiler that respects the computational complexity and computes exact cost annotations. He coordinated a Strategic Project to build a tool, based on the kernel of Matita, for the interactive learning of proof techniques in Calculus courses. He studies the application of Mathematical Knowledge Management techniques to distributed libraries of formal mathematical proofs, with special attention to indexing and searching of mathematical results in the library and their representation by means of adequate linguistic representations. He studies efficient algorithms for parsing and semantical interpretation of typed, highly ambiguous languages, such as the usual mathematical notation. He studies the correspondence between typed languages Curry-Howard isomorphic to classical logic, declarative languages for mathematical proofs and OMDoc, the de facto standard for the representation in XML of mathematical documents.