The Matita interactive theorem prover A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi Automated Deduction–CADE-23: 23rd International Conference on Automated …, 2011 | 115 | 2011 |

Hints in unification A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009 | 71 | 2009 |

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 canonical locally named representation of binding R Pollack, M Sato, W Ricciotti Journal of Automated Reasoning 49 (2), 185-207, 2012 | 36 | 2012 |

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

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

Matita tutorial A Asperti, W Ricciotti, CS Coen Journal of Formalized Reasoning 7 (2), 91-199, 2014 | 24 | 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 | 22 | 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 Types for Proofs and Programs: International Conference, TYPES 2008 Torino …, 2009 | 11 | 2009 |

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

Strongly-Normalizing Higher-Order Relational Queries W Ricciotti, J Cheney Logical Methods in Computer Science 18, 2022 | 9 | 2022 |

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

Query lifting W Ricciotti, J Cheney Programming Languages and Systems 12648, 579-606, 2021 | 8 | 2021 |

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

A Formalization of SQL with Nulls W Ricciotti, J Cheney Journal of Automated Reasoning 66 (4), 989-1030, 2022 | 5 | 2022 |

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

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