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

Added section on Matita

File:
1 edited

Legend:

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

    r3605 r3619  
    291291  key = {jessie}
    292292}
     293
     294@article
     295{ asperti:user:2007,
     296  author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
     297  title = {User interaction with the {Matita} proof assistant},
     298  journal = {Automated Reasoning},
     299  pages = {109--139},
     300  volume = {39},
     301  issue = {2},
     302  year = {2007}
     303}
     304
     305@article
     306{ sacerdoti-coen:tinycals:2007,
     307  author = {Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
     308  title = {{Tinycals}: Step by Step Tacticals},
     309  journal = {Electronic Notes in Theoretical Computer Science},
     310  volume = {174},
     311  number = {2},
     312  pages = {125--142},
     313  doi = {http://dx.doi.org/10.1016/j.entcs.2006.09.026},
     314  year = {2007}
     315}
     316
     317@incollection
     318{ sozeau:subset:2007,
     319  author = {Matthieu Sozeau},
     320  title = {Subset Coercions in {Coq}},
     321  booktitle = {Types for Proofs and Programs},
     322  volume = {4502},
     323  series = {Lecture Notes in Computer Science},
     324  doi = {10.1007/978-3-540-74464-1_16},
     325  pages = {237--252},
     326  year = {2007}
     327}
     328
     329@inproceedings
     330{ asperti:higher-order:2007,
     331  author = {Andrea Asperti and Enrico Tassi},
     332  title = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case},
     333  booktitle = {Towards Mechanized Mathematical Assistants: Calculemus},
     334  pages = {146--160},
     335  series = {Lecture Notes in Computer Science},
     336  volume = {4573},
     337  year = 2007
     338}
     339
     340@inproceedings
     341{ bove:brief:2009,
     342  author = {Ana Bove and Peter Dybjer and Ulf Norell},
     343  title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types},
     344  booktitle = {Theorem Proving in Higher-order Logics {(TPHOLs)}},
     345  year = {2009}
     346}
     347
     348@manual
     349{ coq:2004,
     350  title = {The {Coq} proof assistant reference manual},
     351  author =  {{The Coq development team}},
     352  organization = {{LogiCal Project}},
     353  note = {Version 8.0},
     354  year = {2004},
     355  url = {http://coq.inria.fr}
     356}
     357
     358@misc
     359{ cerco:2011,
     360  title = {The {CerCo} {FET-Open} project},
     361  howpublished = {\url{http://cerco.cs.unibo.it/}},
     362  year = {2011},
     363  key = {CerCo:2011}
     364}
Note: See TracChangeset for help on using the changeset viewer.