|
|
Publications
A Proof of Bertrand's Postulate
with Andrea Asperti
Published in the Journal of Formalized Reasoning, volume 5, pages 37-57, 2012, ISSN: 1972-5787.
[download PDF]
Rating Disambiguation Errors
with Andrea Asperti
Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP 2012), LNCS,
Volume 7679, Pages 240--255, Springer, 2012.
[download PDF]
Formalizing Turing Machines
with Andrea Asperti
Proceedings of the 19th Workshop on Logic, Language, Information and Computation (WoLLIC 2012), LNCS,
Volume 7456, Pages 1--25, Springer, 2012.
[download PDF]
A Web Interface for Matita
with Andrea Asperti
Proceedings of the Conference on Intelligent Computer Mathematics (CICM 2012),
LNAI, Volume 7362/2012, Pages 417-421, DOI:10.1007/978-3-642-31374-5_28, ISBN
978-3-642-31373-8.
[download PDF]
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive
Constructions
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
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 PDF]
The Matita Interactive Theorem Prover
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
23rd International Conference on Automated Deduction, CADE 2011
[download PDF]
Formal Metatheory of Programming Languages in the Matita Interactive Theorem
Prover
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
Published in the Journal of Automated Reasoning, special issue on the PoplMark
challenge, volume 49(3), pages 427-451, October 2012, DOI
10.1007/s10817-011-9228-z.
[download PDF]
A Canonical Locally Named Representation of Binding
with Randy Pollack, Masahiko Sato
Published in the Journal of Automated Reasoning, special issue on Theory and
Applications of Abstraction, Substitution and Naming, volume 49(2), pages
185-207, August 2012, DOI 10.1007/s10817-011-9229-y.
[download PDF]
A new type for tactics
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
To appear in the proceedings of ACM SIGSAM PLMMS 2009, ISBN 978-1-60558-735-6. Published as technical report UBLCS-2009-14.
[download PDF]
Hints in Unification
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
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 PDF]
A compact kernel for the calculus of inductive constructions
with Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi
Published in the Journal Sadhana, Volume 34, Pages 71-144, Year 2009. ISSN: 0256-2499
[download PDF]
About the formalization of some results by Chebyshev in number theory
with Andrea Asperti
Proceedings of TYPES'08, LNCS, Vol. 5497/2009, pages 19-31, DOI
10.1007/978-3-642-02444-3, ISBN 978-3-642-02443-6
[download PDF]
PhD thesis
Theoretical and Implementation Aspects in the Mechanization of the Metatheory of Programming Languages
[download PDF]
A VirtualBox image (tested on VirtualBox v.4.0.0 r69151) of the Matita
interactive theorem prover including the formalizations described in the
thesis can be downloaded
here.
|