The Matita interactive theorem prover A Asperti, W Ricciotti, CS Coen, E Tassi International Conference on Automated Deduction, 64-69, 2011 | 99 | 2011 |

Hints in unification A Asperti, W Ricciotti, CS Coen, E Tassi International Conference on Theorem Proving in Higher Order Logics, 84-98, 2009 | 59 | 2009 |

A compact kernel for the calculus of inductive constructions A Asperti, W Ricciotti, CS Coen, E Tassi Sadhana 34 (1), 71-144, 2009 | 36 | 2009 |

A bi-directional refinement algorithm for the calculus of (co) inductive constructions E Tassi, CS Coen, W Ricciotti, A Asperti Logical Methods in Computer Science 8, 2012 | 34 | 2012 |

A canonical locally named representation of binding R Pollack, M Sato, W Ricciotti Journal of Automated Reasoning 49 (2), 185-207, 2012 | 33 | 2012 |

A formalization of multi-tape Turing machines A Asperti, W Ricciotti Theoretical Computer Science 603, 23-42, 2015 | 25 | 2015 |

Formalizing turing machines A Asperti, W Ricciotti International Workshop on Logic, Language, Information, and Computation, 1-25, 2012 | 24 | 2012 |

Matita tutorial A Asperti, W Ricciotti, CS Coen Journal of Formalized Reasoning 7 (2), 91-199, 2014 | 21 | 2014 |

Imperative functional programs that explain their work W Ricciotti, J Stolarek, R Perera, J Cheney Proceedings of the ACM on Programming Languages 1 (ICFP), 1-28, 2017 | 15 | 2017 |

A new type for tactics A Asperti, W Ricciotti, CS Coen, E Tassi PLMMS 9, 229-232, 2009 | 13 | 2009 |

A web interface for Matita A Asperti, W Ricciotti International Conference on Intelligent Computer Mathematics, 417-421, 2012 | 11 | 2012 |

About the formalization of some results by Chebyshev in number theory A Asperti, W Ricciotti International Workshop on Types for Proofs and Programs, 19-31, 2008 | 11 | 2008 |

Strongly normalizing audited computation W Ricciotti, J Cheney arXiv preprint arXiv:1706.03711, 2017 | 8 | 2017 |

A proof of Bertrand's postulate A Asperti, W Ricciotti Journal of Formalized Reasoning 5 (1), 37-57, 2012 | 6 | 2012 |

A core calculus for provenance inspection W Ricciotti Proceedings of the 19th International Symposium on Principles and Practice …, 2017 | 5 | 2017 |

Formal metatheory of programming languages in the Matita interactive theorem prover A Asperti, W Ricciotti, CS Coen, E Tassi Journal of Automated Reasoning 49 (3), 427-451, 2012 | 5 | 2012 |

Strongly-Normalizing Higher-Order Relational Queries W Ricciotti, J Cheney arXiv preprint arXiv:2011.13451, 2020 | 4 | 2020 |

Theoretical and implementation aspects in the mechanization of the metatheory of programming languages W Ricciotti alma, 2011 | 4 | 2011 |

Mixing set and bag semantics W Ricciotti, J Cheney Proceedings of the 17th ACM SIGPLAN International Symposium on Database …, 2019 | 3 | 2019 |

Explicit auditing W Ricciotti, J Cheney International Colloquium on Theoretical Aspects of Computing, 376-395, 2018 | 3 | 2018 |