| The Matita interactive theorem prover A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi International Conference on Automated Deduction, 64-69, 2011 | 122 | 2011 |
| User interaction with the Matita proof assistant A Asperti, C Sacerdoti Coen, E Tassi, S Zacchiroli Journal of Automated Reasoning 39 (2), 109-139, 2007 | 108 | 2007 |
| Mathematical knowledge management in HELM A Asperti, L Padovani, C Sacerdoti Coen, F Guidi, I Schena Annals of Mathematics and Artificial Intelligence 38 (1), 27-46, 2003 | 103 | 2003 |
| A content based mathematical search engine: Whelp A Asperti, F Guidi, CS Coen, E Tassi, S Zacchiroli International Workshop on Types for Proofs and Programs, 17-32, 2004 | 78 | 2004 |
| Hints in unification A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi International Conference on Theorem Proving in Higher Order Logics, 84-98, 2009 | 74 | 2009 |
| ELPI: fast, embeddable, prolog interpreter C Dunchev, F Guidi, C Sacerdoti Coen, E Tassi Logic for Programming, Artificial Intelligence, and Reasoning, 460-468, 2015 | 72 | 2015 |
| HELM and the semantic math-web A Asperti, L Padovani, CS Coen, I Schena International Conference on Theorem Proving in Higher Order Logics, 59-74, 2001 | 70 | 2001 |
| A survey on retrieval of mathematical knowledge F Guidi, C Sacerdoti Coen Mathematics in Computer Science 10 (4), 409-427, 2016 | 57 | 2016 |
| On the relative usefulness of fireballs B Accattoli, CS Coen 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 141-155, 2015 | 56 | 2015 |
| Certified complexity (cerco) RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ... International Workshop on Foundational and Practical Aspects of Resource …, 2013 | 54 | 2013 |
| Crafting a proof assistant A Asperti, CS Coen, E Tassi, S Zacchiroli International Workshop on Types for Proofs and Programs, 18-32, 2006 | 51 | 2006 |
| Schemapath, a minimal extension to XML Schema for conditional constraints CS Coen, P Marinelli, F Vitali Proceedings of the 13th international conference on World Wide Web, 164-174, 2004 | 46 | 2004 |
| A bi-directional refinement algorithm for the calculus of (co) inductive constructions A Asperti, W Ricciotti, CS Coen, E Tassi Logical Methods in Computer Science 8, 2012 | 40 | 2012 |
| A compact kernel for the calculus of inductive constructions A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi Sadhana 34 (1), 71-144, 2009 | 37 | 2009 |
| Strong call-by-value is reasonable, implosively B Accattoli, A Condoluci, CS Coen 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-14, 2021 | 35 | 2021 |
| SmartTools: a development environment generator based on XML technologies I Attali, C Courbis, P Degenne, A Fau, J Fillon, D Parigot, C Pasquier, ... XML Technologies and Software Engineering, 2001 | 34 | 2001 |
| A survey on retrieval of mathematical knowledge F Guidi, C Sacerdoti Coen International Conference on Intelligent Computer Mathematics, 296-315, 2015 | 31 | 2015 |
| Crumbling abstract machines B Accattoli, A Condoluci, G Guerrieri, CS Coen Proceedings of the 21st International Symposium on Principles and Practice …, 2019 | 29 | 2019 |
| A semi-reflexive tactic for (sub-) equational reasoning CS Coen International Workshop on Types for Proofs and Programs, 98-114, 2004 | 28 | 2004 |
| Matita tutorial A Asperti, W Ricciotti, CS Coen Journal of Formalized Reasoning 7 (2), 91-199, 2014 | 27 | 2014 |
aspertiUniversity of BolognaVerified email at cs.unibo.it
