| The Matita interactive theorem prover A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi Automated Deduction–CADE-23: 23rd International Conference on Automated …, 2011 | 112 | 2011 |
| User interaction with the Matita proof assistant A Asperti, C Sacerdoti Coen, E Tassi, S Zacchiroli Journal of Automated Reasoning 39, 109-139, 2007 | 104 | 2007 |
| Mathematical knowledge management in HELM A Asperti, L Padovani, C Sacerdoti Coen, F Guidi, I Schena Annals of Mathematics and Artificial Intelligence 38, 27-46, 2003 | 102 | 2003 |
| A content based mathematical search engine: Whelp A Asperti, F Guidi, CS Coen, E Tassi, S Zacchiroli Types for Proofs and Programs: International Workshop, TYPES 2004, Jouy-en …, 2006 | 77 | 2006 |
| 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 | 72 | 2001 |
| Hints in unification A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009 | 71 | 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 | 61 | 2015 |
| On the relative usefulness of fireballs B Accattoli, CS Coen 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 141-155, 2015 | 52 | 2015 |
| Certified complexity (cerco) RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ... Foundational and Practical Aspects of Resource Analysis: Third International …, 2014 | 50 | 2014 |
| Crafting a proof assistant A Asperti, CS Coen, E Tassi, S Zacchiroli Types for Proofs and Programs: International Workshop, TYPES 2006 …, 2007 | 50 | 2007 |
| A survey on retrieval of mathematical knowledge F Guidi, C Sacerdoti Coen Mathematics in Computer Science 10 (4), 409-427, 2016 | 47 | 2016 |
| 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 | 44 | 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, 71-144, 2009 | 38 | 2009 |
| A survey on retrieval of mathematical knowledge F Guidi, C Sacerdoti Coen International Conference on Intelligent Computer Mathematics, 296-315, 2015 | 31 | 2015 |
| 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 | 31 | 2001 |
| 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 | 26 | 2021 |
| Tinycals: step by step tacticals CS Coen, E Tassi, S Zacchiroli Electronic Notes in Theoretical Computer Science 174 (2), 125-142, 2007 | 25 | 2007 |
| A semi-reflexive tactic for (sub-) equational reasoning CS Coen Types for Proofs and Programs: International Workshop, TYPES 2004, Jouy-en …, 2006 | 25 | 2006 |
| Mathematical knowledge management and interactive theorem proving CS Coen PhD thesis, University of Bologna, 2004. Technical Report UBLCS 2004-5, 2004 | 25 | 2004 |
aspertiUniversity of Bologna在 cs.unibo.it 的电子邮件经过验证
