A.Asperti; W.Ricciotti, A proof of Bertrand's postulate, «JOURNAL OF FORMALIZED REASONING», 2012, 5, pp. 37 - 57 [articolo]
A. Asperti; W. Ricciotti, A Web Interface for Matita, in: Intelligent Computer Mathematics. CICM 2012., Springer-Verlag, «LECTURE NOTES IN COMPUTER SCIENCE», 2012, 7362, pp. 417 - 421 (atti di: Intelligent Computer Mathematics, CICM 2012, Bremen, Germany, July 8-13, 2012) [Contributo in Atti di convegno]
A. Asperti; W. Ricciotti; C. Sacerdoti Coen; E. Tassi, Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover, «JOURNAL OF AUTOMATED REASONING», 2012, 49(3), pp. 427 - 451 [articolo]
A.Asperti; W.Ricciotti, Formalizing Turing Machines, in: Lecture Notes in Computer Science, Springer Verlag, 2012, 7456, pp. 1 - 25 (atti di: Logic, Language, Information and Computation - 19th International Workshop, WoLLIC 2012, Buenos Aires, Argentina, 3-6 September 2012) [Contributo in Atti di convegno]
A.Asperti; W.Ricciotti, Rating Disambiguation Errors, in: Certified Programs and Proofs. CPP 2012, Springer, «LECTURE NOTES IN COMPUTER SCIENCE», 2012, 7679, pp. 240 - 255 (atti di: Certified Programs and Proofs - CPP 2012, Kyoto, Japan., December 13-15, 2012) [Contributo in Atti di convegno]
A.Asperti; F.Guidi, Type systems for dummies, in: TLDI 2012, s.l, ACM, 2012, pp. 79 - 90 (atti di: Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, Philadelphia, PA, USA, Saturday, January 28, 2012) [Contributo in Atti di convegno]
R. Armadio; A. Asperti; N. Ayache; B. Campbell; D. Mulligan; R. Pollack; Y. Regis-Gianas; C. Sacerdoti Coen; I. Stark, Certified Complexity, «PROCEDIA COMPUTER SCIENCE», 2011, 7, pp. 175 - 177 [articolo]
Asperti, Andrea; Maietti, M. E.; SACERDOTI COEN, Claudio; Sambin, G.; Valentini, S., Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita., in: Lecture Notes in Computer Science, Springer-Verlag, 2011, 6824, pp. 278 - 280 (atti di: Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011., Bertinoro, Italy,, 18-23 Luglio 2011) [Contributo in Atti di convegno]
A. Asperti; E.Tassi, Superposition as a logical glue, «ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE», 2011, 53, pp. 1 - 15 [articolo]
Asperti, Andrea; Ricciotti, Wilmer; SACERDOTI COEN, Claudio; Tassi, E., The Matita Interactive Theorem Prover, in: Lecture Notes in Computer Science, Springer-Verlag, 2011, 6803, pp. 64 - 69 (atti di: 23rd International Conference on Automated Deduction - CADE 23, Wroclaw, Poland, July 31 - August 5, 2011.) [Contributo in Atti di convegno]
A. Asperti; J.Avigad, Zen and the art of formalisation., «MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE», 2011, 21(4), pp. 679 - 682 [articolo]
A.Asperti; E.Tassi, Smart Matching, in: , «LECTURE NOTES IN COMPUTER SCIENCE», 2010, 6167, pp. 263 - 277 (atti di: 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010) [Contributo in Atti di convegno]
A., Asperti; C., Sacerdoti Coen, Some Considerations on the Usability of Interactive Provers., in: Intelligent Computer Mathematics, «LECTURE NOTES IN COMPUTER SCIENCE», 2010, 6167, pp. 147 - 156 (atti di: 17th Symposium, Calculemus 2010, Paris, France, July 5-10, 2010) [Contributo in Atti di convegno]
A.Asperti; W.Ricciotti; C.Sacerdoti Coen; E.Tassi, A compact kernel for the calculus of inductive constructions, «SADHANA (BANGALORE)», 2009, 34, pp. 71 - 144 [articolo]
A. Asperti; W. Ricciotti; E. Tassi; C. Sacerdoti Coen, A new type for tactics, in: PLMMS’09 Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems, s.l, s.n, 2009, pp. 22 - 29 (atti di: International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS09), Munich, Germany, August, 21, 2009) [Contributo in Atti di convegno]