TASSI, ENRICO
TASSI, ENRICO
DIP. DI SCIENZE DELL'INFORMAZIONE
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
2012 A. Asperti; W. Ricciotti; C. Sacerdoti Coen; E. Tassi
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover
2012 A. Asperti; W. Ricciotti; C. Sacerdoti Coen; E. Tassi
Matita 0.99.1
2012 A. Asperti; F. Guidi; W. Ricciotti; C. Sacerdoti Coen; E. Tassi
Formalising Overlap Algebras in Matita
2011 C. Sacerdoti Coen; E. Tassi
A new type for tactics
2009 A. Asperti; W. Ricciotti; E. Tassi; C. Sacerdoti Coen
Natural Deduction Environment for Matita
2009 SACERDOTI COEN, Claudio; Tassi, Enrico
A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
2008 C. Sacerdoti Coen; E. Tassi
Matita 0.5.7
2008 A.Asperti; C.Sacerdoti Coen; W. Ricciotti; E.Tassi; S.Zacchiroli
Working with Mathematical Structures in Type Theory
2008 SACERDOTI COEN, Claudio; Tassi, Enrico
Crafting a Proof Assistant
2007 A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli
Higher order proof reconstruction from paramodulation-based refutations: the unit equality case.
2007 A.Asperti; E.Tassi.
Matita
2007 A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli
Tinycals: Step by Step Tacticals
2007 SACERDOTI COEN, Claudio; Tassi, Enrico; Zacchiroli, Stefano
User Interaction with the Matita Proof Assistant
2007 A.Asperti; C.Sacerdoti Coen; E. Tassi; S.Zacchiroli
A content based mathematical search engine: Whelp
2005 A.Asperti; F.Guidi; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli
User Level Networking-Personal IP: assigning each user his/her own IP addresses in multiuser operating systems
2004 A. Pira; E. Tassi; R. Davoli
| Titolo | Autore(i) | Anno | Periodico | Editore | Tipo | File |
|---|---|---|---|---|---|---|
| A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions | A. Asperti; W. Ricciotti; C. Sacerdoti Coen; E. Tassi | 2012-01-01 | LOGICAL METHODS IN COMPUTER SCIENCE | - | 1.01 Articolo in rivista | - |
| Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover | A. Asperti; W. Ricciotti; C. Sacerdoti Coen; E. Tassi | 2012-01-01 | JOURNAL OF AUTOMATED REASONING | - | 1.01 Articolo in rivista | - |
| Matita 0.99.1 | A. Asperti; F. Guidi; W. Ricciotti; C. Sacerdoti Coen; E. Tassi | 2012-01-01 | - | - | 7.04 Software | - |
| Formalising Overlap Algebras in Matita | C. Sacerdoti Coen; E. Tassi | 2011-01-01 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | - | 1.01 Articolo in rivista | - |
| A new type for tactics | A. Asperti; W. Ricciotti; E. Tassi; C. Sacerdoti Coen | 2009-01-01 | - | s.n | 4.01 Contributo in Atti di convegno | - |
| Natural Deduction Environment for Matita | SACERDOTI COEN, Claudio; Tassi, Enrico | 2009-01-01 | - | Springer-Verlag | 4.01 Contributo in Atti di convegno | - |
| A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita | C. Sacerdoti Coen; E. Tassi | 2008-01-01 | JOURNAL OF FORMALIZED REASONING | - | 1.01 Articolo in rivista | - |
| Matita 0.5.7 | A.Asperti; C.Sacerdoti Coen; W. Ricciotti; E.Tassi; S.Zacchiroli | 2008-01-01 | - | - | 7.04 Software | - |
| Working with Mathematical Structures in Type Theory | SACERDOTI COEN, Claudio; Tassi, Enrico | 2008-01-01 | LECTURE NOTES IN COMPUTER SCIENCE | - | 4.01 Contributo in Atti di convegno | - |
| Crafting a Proof Assistant | A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli | 2007-01-01 | - | - | 4.01 Contributo in Atti di convegno | - |
| Higher order proof reconstruction from paramodulation-based refutations: the unit equality case. | A.Asperti; E.Tassi. | 2007-01-01 | - | - | 4.01 Contributo in Atti di convegno | - |
| Matita | A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli | 2007-01-01 | - | - | 7.04 Software | - |
| Tinycals: Step by Step Tacticals | SACERDOTI COEN, Claudio; Tassi, Enrico; Zacchiroli, Stefano | 2007-01-01 | ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | - | 4.01 Contributo in Atti di convegno | - |
| User Interaction with the Matita Proof Assistant | A.Asperti; C.Sacerdoti Coen; E. Tassi; S.Zacchiroli | 2007-01-01 | JOURNAL OF AUTOMATED REASONING | - | 1.01 Articolo in rivista | - |
| A content based mathematical search engine: Whelp | A.Asperti; F.Guidi; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli | 2005-01-01 | - | Springer | 4.01 Contributo in Atti di convegno | - |
| User Level Networking-Personal IP: assigning each user his/her own IP addresses in multiuser operating systems | A. Pira; E. Tassi; R. Davoli | 2004-01-01 | - | IEEE | 4.01 Contributo in Atti di convegno | - |