Andrea Asperti

Recent Papers

A.Asperti, J.J.Levy. The cost of usage in the lambda calculus, LICS 2013. G.Gonthier, A.Asperti, J.Avigad, Y.Bertot, C.Cohen, F.Garillot, S.Le Roux, A.Mahboubi, R.O'Connor, S.Ould Biha, I.Pasca, L.Rideau, A.Solovyev, E.Tassi and L.Thery. A Machine-Checked Proof of the Odd Order Theorem, ITP 2013. A.Asperti, W.Ricciotti. A proof of Bertrand's postulate, Journal of Formalized Reasoning, V.5, n.1, pp-37-57, 2012. A.Asperti, W.Ricciotti. Rating Disambiguation Errors, CPP'12, LNCS 7679, pp.240-255, 2012. A.Asperti, W.Ricciotti. Formalizing Turing Machines, Wollic'12, LNCS 7456, pp.1-25, 2012. A.Asperti. A compact proof of decidability for regular expression equivalence. ITP 2012. A.Asperti, W.Ricciotti. A Web Interface for Matita. CICM 2012. To appear. A.Asperti. Proof, message and certificate. CICM 2012. To appear. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi. A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions.Logical Methods in Computer Science 8(1): (2012) A. Asperti, F.Guidi. Type Systems for Dummies. Proc. of 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2012): 79-90. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi: The Matita Interactive Theorem Prover. CADE 2011. LNCS 6803:64-69. A.Asperti,J.Avigad. Zen and the Art of Formalization. Mathematical Structures in Computer Science, V.21,n.4:679-682 A.Asperti, M.E.Maietti, C.Sacerdoti Coen, G.Sambin, S.Valentini. Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. Calculemus/MKM 2011. :NCS 6824:278-280 A.Asperti, C.Sacerdoti Coen. Some Considerations on the Usability of Interactive Provers. Proceedings of AISC/MKM/Calculemus 2010, LNCS 6167, pp.147-156. A.Asperti, E.Tassi: Smart Matching. Proceedings of AISC/MKM/Calculemus 2010. LNCS 6167,pp. 263-277. A.Asperti,H.Geuvers,R.Natarajan. Social Processes, Program Verification and all that. Mathematical Structures in Computer Science, vol 19, issue 05, pp 877-896, october 2009. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi. Hints in unification.. Proceedings of TPHOLS'09, LNCS 5674, pp. 84 - 98, 2009. A.Asperti, E.Tassi. Superposition as a logical glue. TYPES 2009, EPTCS, V.53: 1-15 A.Asperti, N.Busi: Mobile Petri nets. Mathematical Structures in Computer Science 19(6): 1265-1278 (2009) A.Asperti, W.Ricciotti. About the Formalization of Some Results by Chebyshev in Number Theory. Proceedings of TYPES'08, LNCS 5497, pp.19-31, 2009. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi. A compact kernel for the calculus of inductive constructions.. In Special Issue on Iteractive Proving and Proof Checking of the Academy Journal of Engineering Sciences (Sadhana) of the Indian Academy of Sciences. SADHANA (BANGALORE). vol. 34(1), pp. 71 - 144, 2009. A.Asperti, E.Tassi An Interactive Driver for Goal-directed Proof Strategies. Electr. Notes Theor. Comput. Sci. 226: 89-105, 2009. A.Asperti, C.Armentano A Page in Number Theory. Journal of Formalized Reasoning, Vol.1, pp.1-23, 2008. A.Asperti The Intensional Content of Rice's Theorem Proceedings of the 35th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2008), San Francisco, USA, 2008. A.Asperti, E.Tassi. Higher order proof reconstruction from paramodulation-based refutations: the unit equality case. Proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. LNCS 4573, 2007. A.Asperti, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli. Crafting a Proof Assistant. Proceedings of Types 2006: Types for Proofs and Programs. Nottingham, UK -- April 18-21, 2006. LNCS 4502, Springer, ISBN 978-3-540-74463-4, pp. 18-32, 2007 A.Asperti, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli. User Interaction with the Matita Proof Assistant. Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving, Springer Netherlands, ISSN 0168-7433, pp. 109-139, 2007 A.Asperti, H.Geuvers, I.Loeb, L.E.Mamane, C.Sacerdoti Coen. An Interactive Algebra Course with Formalised Proofs and Definitions. .Proceedings of the Fourth International Conference on Mathemtical Knowledge Management. Bremen, Germany, July 2005. A.Asperti, F.Guidi, C. Sacerdoti Coen, E. Tassi, S.Zacchiroli A content based mathematical search engine: Whelp Proceedings of the TYPES 2004 Intenrational Conference, Jouy-en-Josas France, December 2004. A.Asperti, P.Coppola, S.Martini. (Optimal) duplication is not elementary recursive. Information and Computation 193 (2004), pp.21-56. Short Popl-00 version. A.Asperti, M.Selmi. Efficient Retrieval of Mathematical Statements. Proceeding of the Third International Conference on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119. A.Asperti, G.Bancerek, A.Trybulec (eds). Proceedings of the Third International Conference on Mathematical Knowledge Management, LNCS 3119. Bialowieza, poland, september 2004. A.Asperti, L.Padovani, C.Sacerdoti Coen, F.Guidi e I.Schena. Mathematical Knowledge Management in HELM. Annals of Mathematics and Artificial Intelligence 38(1): 27--46, 2003. A.Asperti, B.Buchberger, J.H.Davenport (eds). Proceedings of the Second International Conference on Mathematical Knowledge Management, LNCS 2594. Bertinoro, Italy, february 2003. A.Asperti, L.Roversi. Intuitionistic Light Affine Logic. ACM Transactions on Computational Logic (TOCL), Volume 3 , Issue 1, January 2002, pp.137 - 175. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena. Content-centric Logical Environments. Short Presentation at LICS-2000.

home

cv

didattica

papers