# Enrico Tassi Homepage / Publications

A language of patterns for subterm selection with Georges Gonthier. Published in the proceedings of ITP 2012, LNCS, Volume 7406, Year 2012, Pages 361-376, DOI: , ISBN: . Download

A bi-directional refinement algorithm for the Calculus of (Co)Inductive Constructions with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen. Published in Logical Methods in Computer Science, volume 8, Pages 1-49, 2012. DOI:10.2168/LMCS-8(1:18)2012. ISSN: 1860-5974 . Download The Matita Interactive Theorem Prover with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen. Published in the proceedings of CADE 2011, LNCS 6803, 2011, Pages 64-69, ISBN 978-3-642-22437-9. Download Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen. Published in the journal of Automated Rasoning, Special Issue on the Poplmark Challenge, Pages 1-25, Year 2011. ISSN: 0168-7433. DOI: 10.1007/s10817-011-9228-z Download Pointed Regular Expressions with Andrea Asperti and Claudio Sacerdoti Coen. Submitted to the LATA2011 conference. Download Formalizing Overlap Algebras in Matita with Claudio Sacerdoti Coen. Journal Mathematical Structures in Computer Science, Volume 21, Issue 3, Pages 1-31, Year 2011. ISSN: 0960-1295. EISSN: 1469-8072. DOI: 10.1017/S0960129511000107. Download Superposition as a logical glue with Andrea Asperti. Published in the proceedings of TYPES 2009, EPTCS Volume 53, Pages 1-15, Year 2011, ISSN: 2075-2180, DOI: 10.4204/EPTCS.53. Download Nonuniform Coercions via Unification Hints with Claudio Sacerdoti Coen. Published in the proceedings of TYPES 2009, EPTCS Volume 53, Pages 16-29, Year 2011, ISSN: 2075-2180, DOI: 10.4204/EPTCS.53. Download Slides Smart Matching with Andrea Asperti. Published in the proceedings of MKM2010, LNCS, Volume 6167/2010, Year 2010, Pages 263-277, DOI 10.1007/978-3-642-14128-7_23, ISBN 978-3-642-14127-0 Download A new type for tactics with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen. To appear in the proceedings of ACM SIGSAM PLMMS 2009, ISBN 978-1-60558-735-6. Published as technical report UBLCS-2009-14. Download Slides Hints in Unification with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen. Published in the proceedings of TPHOLs 2009, LNCS, Volume 5674/2009, Pages 84-98, DOI 10.1007/978-3-642-03359-9, ISBN 978-3-642-03358-2 Download Slides Natural deduction environment for Matita with Claudio Sacerdoti Coen. Published in the proceedings of MKM2009, Volume 5625, Pages 486-491, ISBN 978-3-642-02613-3, DOI 10.1007/978-3-642-02614-0_40 Download Slides A compact kernel for the calculus of inductive constructions with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen. Published in the Journal Sadhana, Volume 34, Pages 71-144, Year 2009. ISSN: 0256-2499 Download Slides A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita with Claudio Sacerdoti Coen. Published by the Journal of Formalized Reasoning , Issue 1, Volume 1, Pages 51-89, Year 2008. ISSN: 1972-5787. Download An interactive driver for goal directed proof strategies with Andrea Asperti. Published in the Proceedings of UITP 2008: 8th International Workshop On User Interfaces for Theorem Provers, 22 August 2008, Montréal, Québec, Canada. ENTCS, Volume 226, 3 January 2009, Pages 89-105, ISSN 1571-0661, DOI 10.1016/j.entcs.2008.12.099Download Slides Working with Mathematical Structures in Type Theory with Sacerdoti Coen. Published in the Proceedings of TYPES 2007: Conference of the Types Project, 2-5 May 2007 Cividale del Friuli (Udine), Italy. LNCS, ISSN 0302-9743 (Print) 1611-3349 (Online), DOI 10.1007/978-3-540-68103-8, ISBN 978-3-540-68084-0, Pages 157-172, Volume 4941, Year 2008. Download Slides A modular formalisation of finite group theory with Georges Gonthier, Assia Mahboubi , Laurence Rideau and Laurent Thery.

Published in the Proceedings of TPHOL 2007: The 20th International Conference on Theorem Proving in Higher Order Logics. LNCS, Volume 4732, ISBN: 978-3-540-74590-7, DOI: 10.1007/978-3-540-74591-4, Pages: 86-101, 2007. Download Higher order proof reconstruction from paramodulation-based refutations: the unit equality case with Andrea Asperti. Published in the Proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. LNAI, Volume 4573, ISBN: 978-3-540-73083-5, 2007. Download Slides Crafting a Proof Assistant with Andrea Asperti, Claudio Sacerdoti Coen, Stefano Zacchiroli. Published in the Proceedings of Types 2006: Conference of the Types Project. Nottingham, UK -- April 18-21, 2006. LNCS Volume 4502, Springer Berlin / Heidelberg, ISBN 978-3-540-74463-4, pp. 18-32, 2007. Download Slides User Interaction with the Matita Proof Assistant with Andrea Asperti, Claudio Sacerdoti Coen, Stefano Zacchiroli. Published in the Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving, Springer Netherlands, ISSN 0168-7433, Volume 39, Issue 2, August 2007, Pages: 109-139. Download Tinycals: Step by Step Tacticals with Claudio Sacerdoti Coen, Stefano Zacchiroli. In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle, WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 - 142, ISSN:1571-0661 Download Slides Modified Realizability and Inductive Types with Andrea Asperti, June 2006. Technical report [UBLCS-2006-18][tr200618]. Download A content based mathematical search engine: Whelp with Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, and Stefano Zacchiroli.

Published In Proceedings of TYPES 2004 conference: Types for Proofs and Programs. Paris, France -- December 15-18, 2004. LNCS 3839, Springer Berlin / Heidelberg, ISBN 3-540-31428-8, pp. 17-32, 2006. Download User Level Networking-Personal IP: assigning each user his/her own IP addresses in multiuser operating systems with Alessandro Pira and Renzo Davoli. Published in the proceedings of ICN04, IEEE International Conference on Networking, February 29 - March 4 2004, Guadeloupe, French Caribbean. Download