Sfoglia per Autore
A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
2008 C. Sacerdoti Coen; E. Tassi
A new type for tactics
2009 A. Asperti; W. Ricciotti; E. Tassi; C. Sacerdoti Coen
Hints in Unification
2009 A., Asperti; W., Ricciotti; C., Sacerdoti Coen; E.,Tassi
Natural Deduction Environment for Matita
2009 SACERDOTI COEN, Claudio; Tassi, Enrico
A User Interface for a Mathematical System that Allows Ambiguous Formulae
2009 C. Sacerdoti Coen
Matita 0.5.8
2009 A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli
Intelligent Computer Mathematics
2009 Carette, J.; Dixon, L.; SACERDOTI COEN, Claudio; Watt, S. M.
A compact kernel for the calculus of inductive constructions
2009 A.Asperti; W.Ricciotti; C.Sacerdoti Coen; E.Tassi
Certified Complexity (CerCo)
2010 C. Sacerdoti Coen
General Recursion and Formal Topology
2010 C. Sacerdoti Coen; S. Valentini
Some Considerations on the Usability of Interactive Provers.
2010 A., Asperti; C., Sacerdoti Coen
Declarative Representation of Proof Terms
2010 C. Sacerdoti Coen
Functions as Processes: Termination and the lambda mu mu~ - Calculus
2010 M. Cimini; C. Sacerdoti Coen; D. Sangiorgi
Nonuniform Coercions via Unification Hints
2011 Claudio Sacerdoti Coen;Enrico Tassi
A Foundational View on Integration Problems
2011 F.Rabe; M.Kohlhase; C.Sacerdoti Coen
The Matita Interactive Theorem Prover
2011 Asperti, Andrea; Ricciotti, Wilmer; SACERDOTI COEN, Claudio; Tassi, E.
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.
2011 Asperti, Andrea; Maietti, M. E.; SACERDOTI COEN, Claudio; Sambin, G.; Valentini, S.
Formalising Overlap Algebras in Matita
2011 C. Sacerdoti Coen; E. Tassi
Certified Complexity
2011 R. Armadio; A. Asperti; N. Ayache; B. Campbell; D. Mulligan; R. Pollack; Y. Regis-Gianas; C. Sacerdoti Coen; I. Stark
Matita 0.99.1
2012 A. Asperti; F. Guidi; W. Ricciotti; C. Sacerdoti Coen; E. Tassi
| Titolo | Autore(i) | Anno | Periodico | Editore | Tipo | File |
|---|---|---|---|---|---|---|
| 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 | - |
| 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 | - |
| Hints in Unification | A., Asperti; W., Ricciotti; C., Sacerdoti Coen; E.,Tassi | 2009-01-01 | - | - | 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 User Interface for a Mathematical System that Allows Ambiguous Formulae | C. Sacerdoti Coen | 2009-01-01 | ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | - | 4.01 Contributo in Atti di convegno | - |
| Matita 0.5.8 | A.Asperti; C.Sacerdoti Coen; E.Tassi; S.Zacchiroli | 2009-01-01 | - | - | 7.04 Software | - |
| Intelligent Computer Mathematics | Carette, J.; Dixon, L.; SACERDOTI COEN, Claudio; Watt, S. M. | 2009-01-01 | - | Springer | 3.02 Curatela | - |
| A compact kernel for the calculus of inductive constructions | A.Asperti; W.Ricciotti; C.Sacerdoti Coen; E.Tassi | 2009-01-01 | SADHANA (BANGALORE) | - | 1.01 Articolo in rivista | - |
| Certified Complexity (CerCo) | C. Sacerdoti Coen | 2010-01-01 | - | - | 8.04 Coordinamento di progetti di ricerca | - |
| General Recursion and Formal Topology | C. Sacerdoti Coen; S. Valentini | 2010-01-01 | - | Electronic Proceedings in Theoretical Computer Sci | 4.01 Contributo in Atti di convegno | - |
| Some Considerations on the Usability of Interactive Provers. | A., Asperti; C., Sacerdoti Coen | 2010-01-01 | - | - | 4.01 Contributo in Atti di convegno | - |
| Declarative Representation of Proof Terms | C. Sacerdoti Coen | 2010-01-01 | JOURNAL OF AUTOMATED REASONING | - | 1.01 Articolo in rivista | - |
| Functions as Processes: Termination and the lambda mu mu~ - Calculus | M. Cimini; C. Sacerdoti Coen; D. Sangiorgi | 2010-01-01 | - | Springer | 4.01 Contributo in Atti di convegno | - |
| Nonuniform Coercions via Unification Hints | Claudio Sacerdoti Coen;Enrico Tassi | 2011-01-01 | ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | - | 1.01 Articolo in rivista | - |
| A Foundational View on Integration Problems | F.Rabe; M.Kohlhase; C.Sacerdoti Coen | 2011-01-01 | - | Springer-Verlag | 4.01 Contributo in Atti di convegno | - |
| The Matita Interactive Theorem Prover | Asperti, Andrea; Ricciotti, Wilmer; SACERDOTI COEN, Claudio; Tassi, E. | 2011-01-01 | - | Springer-Verlag | 4.01 Contributo in Atti di convegno | - |
| Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. | Asperti, Andrea; Maietti, M. E.; SACERDOTI COEN, Claudio; Sambin, G.; Valentini, S. | 2011-01-01 | - | Springer-Verlag | 4.01 Contributo in Atti di convegno | - |
| Formalising Overlap Algebras in Matita | C. Sacerdoti Coen; E. Tassi | 2011-01-01 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | - | 1.01 Articolo in rivista | - |
| Certified Complexity | R. Armadio; A. Asperti; N. Ayache; B. Campbell; D. Mulligan; R. Pollack; Y. Regis-Gianas; C. Sace...rdoti Coen; I. Stark | 2011-01-01 | PROCEDIA COMPUTER SCIENCE | - | 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 | - |
Legenda icone
- file ad accesso aperto
- file disponibili sulla rete interna
- file disponibili agli utenti autorizzati
- file disponibili solo agli amministratori
- file sotto embargo
- nessun file disponibile