Matita is an interactive theorem prover being developed by the Helm team at the University
of Bologna. Its stable version 0.5. x may be downloaded at http://matita. cs. unibo. it. The tool …

The paper describes the refinement algorithm for the Calculus of (Co) Inductive
Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement …

In a controversial paper (De Millo et al. 1979) at the end of the 1970's, RA De Millo, RJ
Lipton and AJ Perlis argued against formal verifications of programs, mostly motivating their …

The paper describes the new kernel for the Calculus of Inductive Constructions (CIC)
implemented inside the Matita Interactive Theorem Prover. The design of the new kernel has …

In spite of the remarkable achievements recently obtained in the field of mechanization of
formal reasoning, the overall usability of interactive provers does not seem to be sensibly …

The recent achievements obtained by means of Interactive Theorem Provers in the
automatic verification of complex mathematical results have reopened an old and interesting …

We present a formalisation of a constructive proof of Lebesgue's Dominated Convergence
Theorem given by the Sacerdoti Coen and Zoli in [CSCZ]. The proof is done in the abstract …

We present a formalisation of the Agrawal-Kayal-Saxena (AKS) algorithm, a deterministic
polynomial-time primality test. This algorithm was first announced by the AKS team in 2002 …

We present a proof of the fact that 2^ n ≤ lcm {1, 2, 3,\dots,(n+ 1)\}. This result has a
standard proof via an integral, but our proof is purely number theoretic, requiring little more …

We present a proof of the fact that for n ≥ 0 n≥ 0. This result has a standard proof via an
integral, but our proof is purely number-theoretic, requiring little more than inductions based …