Claudio Sacerdoti Coen;Enrico Tassi, Nonuniform Coercions via Unification Hints, «ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE», 2011, 53, pp. 16 - 29 [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]
Coordinamento del progetto: Certified Complexity (CerCo).
C. Sacerdoti Coen, Declarative Representation of Proof Terms, «JOURNAL OF AUTOMATED REASONING», 2010, 44, pp. 25 - 52 [articolo]
M. Cimini; C. Sacerdoti Coen; D. Sangiorgi, Functions as Processes: Termination and the lambda mu mu~ - Calculus, in: Lecture Notes in Computer Science, BERLIN, Springer, 2010, 6084, pp. 73 - 86 (atti di: 5th International Symposium on Trustworthly Global Computing - TGC 2010, Munich, Germany, February 24-26, 2010) [Contributo in Atti di convegno]
C. Sacerdoti Coen; S. Valentini, General Recursion and Formal Topology, in: Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, s.l, Electronic Proceedings in Theoretical Computer Sci, 2010, 43, pp. 65 - 75 (atti di: Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010), Edinburgh, 15th July 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]
C. Sacerdoti Coen, A User Interface for a Mathematical System that Allows Ambiguous
Formulae, in: , 2009, 226, pp. 67 - 87 (atti di: 8th International Workshop On User Interfaces for Theorem Provers, Montréal, Québec, Canada, 22nd August 2008) [Contributo in Atti di convegno]
A., Asperti; W., Ricciotti; C., Sacerdoti Coen; E.,Tassi, Hints in Unification, in: Theorem Proving in Higher Order Logics, «LECTURE NOTES IN COMPUTER SCIENCE», 2009, 5674, pp. 84 - 98 (atti di: Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, Germany, August 17-20, 2009) [Contributo in Atti di convegno]
Carette, J.; Dixon, L.; SACERDOTI COEN, Claudio; Watt, S. M., Intelligent Computer Mathematics, BERLIN, Springer, 2009, pp. 494 (Lecture Notes in Artificial Intelligence). [curatela]
A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli, Matita 0.5.8, 2009. [software]
SACERDOTI COEN, Claudio; Tassi, Enrico, Natural Deduction Environment for Matita, in: Intelligent Computer Mathematics, BERLIN, Springer-Verlag, 2009, 5625, pp. 486 - 491 (atti di: 8th International Conference on Mathematical Knowledge Management (MKM 09), Grand Bend, Canada, 10-12/07/2009) [Contributo in Atti di convegno]
C. Sacerdoti Coen; E. Tassi, A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita, «JOURNAL OF FORMALIZED REASONING», 2008, 1, pp. 51 - 89 [articolo]
