Keywords: Type theory Interactive theorem proving Mathematical knowledge management Lambda-calculus Programming languages Smart contracts

Associate Professor

Department of Computer Science and Engineering

Academic discipline: INF/01 Informatics

Director of First Cycle Degree in Computer Science

Keywords: Type theory Interactive theorem proving Mathematical knowledge management Lambda-calculus Programming languages Smart contracts

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.