# Changeset 3619 for Papers

Ignore:
Timestamp:
Mar 6, 2017, 4:02:43 PM (2 years ago)
Message:

Location:
Papers/jar-cerco-2017
Files:
3 edited

Unmodified
Removed
• ## Papers/jar-cerco-2017/cerco.bib

 r3605 key = {jessie} } @article { asperti:user:2007, author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli}, title = {User interaction with the {Matita} proof assistant}, journal = {Automated Reasoning}, pages = {109--139}, volume = {39}, issue = {2}, year = {2007} } @article { sacerdoti-coen:tinycals:2007, author = {Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli}, title = {{Tinycals}: Step by Step Tacticals}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {174}, number = {2}, pages = {125--142}, doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026}, year = {2007} } @incollection { sozeau:subset:2007, author = {Matthieu Sozeau}, title = {Subset Coercions in {Coq}}, booktitle = {Types for Proofs and Programs}, volume = {4502}, series = {Lecture Notes in Computer Science}, doi = {10.1007/978-3-540-74464-1_16}, pages = {237--252}, year = {2007} } @inproceedings { asperti:higher-order:2007, author = {Andrea Asperti and Enrico Tassi}, title = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case}, booktitle = {Towards Mechanized Mathematical Assistants: Calculemus}, pages = {146--160}, series = {Lecture Notes in Computer Science}, volume = {4573}, year = 2007 } @inproceedings { bove:brief:2009, author = {Ana Bove and Peter Dybjer and Ulf Norell}, title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types}, booktitle = {Theorem Proving in Higher-order Logics {(TPHOLs)}}, year = {2009} } @manual { coq:2004, title = {The {Coq} proof assistant reference manual}, author =  {{The Coq development team}}, organization = {{LogiCal Project}}, note = {Version 8.0}, year = {2004}, url = {http://coq.inria.fr} } @misc { cerco:2011, title = {The {CerCo} {FET-Open} project}, howpublished = {\url{http://cerco.cs.unibo.it/}}, year = {2011}, key = {CerCo:2011} }
• ## Papers/jar-cerco-2017/cerco.tex

 r3615 \lstset{language=C,basicstyle=\tt,basewidth=.5em,lineskip=-1.5pt} \def\lstlanguagefiles{lst-grafite.tex} \newlength{\mylength}
• ## Papers/jar-cerco-2017/introduction.tex

Note: See TracChangeset for help on using the changeset viewer.