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 |

Hints in unification A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009 | 64 | 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 | 39 | 2012 |

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 compact kernel for the calculus of inductive constructions A Asperti, W Ricciotti, C Sacerdoti Coen, E Tassi Sadhana 34, 71-144, 2009 | 36 | 2009 |

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

Formalizing turing machines A Asperti, W Ricciotti Logic, Language, Information and Computation: 19th International Workshop …, 2012 | 26 | 2012 |

Matita tutorial A Asperti, W Ricciotti, CS Coen Journal of Formalized Reasoning 7 (2), 91-199, 2014 | 22 | 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 | 12 | 2009 |

A web interface for Matita A Asperti, W Ricciotti Intelligent Computer Mathematics: 11th International Conference, AISC 2012 …, 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 |

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

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

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

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

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 | 6 | 2012 |

Query lifting W Ricciotti, J Cheney Programming Languages and Systems LNCS 12648, 579, 2021 | 5 | 2021 |

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

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