source: Papers/itp-2013/ccexec.bib @ 3435

Entry made up

@article{MilnerWeyhrauch72,
  title = {Proving compiler correctness in a mechanized logic},
  author = {R. Milner and R. Weyhrauch},
  journal = {Machine Intelligence},
  year = 1972,
  volume = 7,
  pages = {51--70},
  editors = {Bernard Meltzer and Donald Michie},
  publisher = {Edinburgh University Press}
}

Entry from ACM Digital Library.

@inproceedings{Tatlock:2010:BEV:1806596.1806611,
 author = {Tatlock, Zachary and Lerner, Sorin},
 title = {Bringing extensibility to verified compilers},
 booktitle = {Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation},
 series = {PLDI '10},
 year = {2010},
 isbn = {978-1-4503-0019-3},
 location = {Toronto, Ontario, Canada},
 pages = {111--121},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1806596.1806611},
 doi = {http://doi.acm.org/10.1145/1806596.1806611},
 acmid = {1806611},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {compiler optimization, correctness, extensibility},
}

Entry from ACM Digitial Library.  (With name fixup)

@inproceedings{Sevcik:2011:RCV:1926385.1926393,
 author = {\v{S}ev\v{c}\'{i}k, Jaroslav and Vafeiadis, Viktor and Zappa Nardelli, Francesco and Jagannathan, Suresh and Sewell, Peter},
 title = {Relaxed-memory concurrency and verified compilation},
 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '11},
 year = {2011},
 isbn = {978-1-4503-0490-0},
 location = {Austin, Texas, USA},
 pages = {43--54},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1926385.1926393},
 doi = {http://doi.acm.org/10.1145/1926385.1926393},
 acmid = {1926393},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {relaxed memory models, semantics, verifying compilation},
}

Entry from ACM Digital Library.

@article{Leroy:2009:FVR:1538788.1538814,
 author = {Leroy, Xavier},
 title = {Formal verification of a realistic compiler},
 journal = {Commun. ACM},
 issue_date = {July 2009},
 volume = {52},
 issue = {7},
 month = jul,
 year = {2009},
 issn = {0001-0782},
 pages = {107--115},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/1538788.1538814},
 doi = {http://doi.acm.org/10.1145/1538788.1538814},
 acmid = {1538814},
 publisher = {ACM},
 address = {New York, NY, USA},
}

Entry from ACM Digital Library.

@inproceedings{1328444,
 author = {Jean-Baptiste Tristan and Xavier Leroy},
 title = {Formal verification of translation validators: a case study on instruction scheduling optimizations},
 booktitle = {POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {2008},
 isbn = {978-1-59593-689-9},
 pages = {17--27},
 location = {San Francisco, California, USA},
 doi = {http://doi.acm.org/10.1145/1328438.1328444},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

Entry made up.

@inproceedings{coqextr02,
  title  = {A New Extraction for {C}oq},
  author = {Pierre Letouzey},
  booktitle = {Types for Proofs and Programs (TYPES 2002)},
  year   = 2003,
  volume = 2646,
  series = {Lecture Notes in Computer Science},
  pages  = {200--219},
  publisher = {Springer-Verlag},
  doi    = {10.1007/3-540-39185-1_12}
}

Entry from Springerlink with obvious corrections.

@article {springerlink:10.1007/s10817-009-9148-3,
   author = {Blazy, Sandrine and Leroy, Xavier},
   affiliation = {ENSIIE 1 square de la Résistance 91025 Evry cedex France},
   title = {Mechanized Semantics for the {Clight} Subset of the {C} Language},
   journal = {Journal of Automated Reasoning},
   publisher = {Springer Netherlands},
   issn = {0168-7433},
   keyword = {Computer Science},
   pages = {263-288},
   volume = {43},
   issue = {3},
   url = {http://dx.doi.org/10.1007/s10817-009-9148-3},
   doi = {10.1007/s10817-009-9148-3},
   abstract = {This article presents the formal semantics of a large subset of the C language called Clight. Clight includes pointer arithmetic, struct and union types, C loops and structured switch statements. Clight is the source language of the CompCert verified compiler. The formal semantics of Clight is a big-step operational semantics that observes both terminating and diverging executions and produces traces of input/output events. The formal semantics of Clight is mechanized using the Coq proof assistant. In addition to the semantics of Clight, this article describes its integration in the CompCert verified compiler and several ways by which the semantics was validated.},
   year = {2009}
}

Entry made up

@manual{coq83,
  title = {The {Coq} Proof Assistant: Reference Manual, Version 8.3},
  author = {The Coq Development Team},
  organization = {INRIA},
  year = 2010,
  url = {http://coq.inria.fr/distrib/8.3pl2/refman/}
}

Entry made up

@techreport{c99,
  title = {Programming languages --- {C}},
  key = {C99},
  institution = {ISO},
  year = {1999},
  type = {International standard},
  number = {ISO/IEC 9899:1999}
}

Entry made up.

@article{compcert1,
  author = {Xavier Leroy},
  title = {Formal verification of a realistic compiler},
  journal = {Communications of the ACM},
  year = 2009,
  volume = 52,
  number = 7,
  pages = {107--115},
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/1538788.1538814},
  hal = {http://hal.archives-ouvertes.fr/inria-00415861/},
  pubkind = {journal-int-mono},
  abstract = {This paper reports on the development and formal verification (proof
of semantic preservation) of CompCert, a compiler from Clight (a
large subset of the C programming language) to PowerPC assembly code,
using the Coq proof assistant both for programming the compiler and
for proving its correctness.  Such a verified compiler is useful in
the context of critical software and its formal verification: the
verification of the compiler guarantees that the safety properties
proved on the source code hold for the executable compiled code as
well.}
}

@article{compcert2,
  title = {Formal Verification of a {C}-like Memory Model and Its Uses for Verifying Program Transformations},
  author = {Xavier Leroy and Sandrine Blazy},
  journal = {Journal of Automated Reasoning},
  year = 2008,
  volume = 41,
  number = 1,
  pages = {1--31},
  doi = {10.1007/s10817-008-9099-0}
}

@article{compcert3,
  author = {Xavier Leroy},
  title = {A formally verified compiler back-end},
  journal = {Journal of Automated Reasoning},
  volume = 43,
  number = 4,
  pages = {363--446},
  year = 2009,
  url = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
  hal = {http://hal.inria.fr/inria-00360768/},
  pubkind = {journal-int-mono}
}


Entry from ACM Digital Library with obvious correction.

@inproceedings{Yang:2011:FUB:1993498.1993532,
 author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
 title = {Finding and understanding bugs in {C} compilers},
 booktitle = {Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation},
 series = {PLDI '11},
 year = {2011},
 isbn = {978-1-4503-0663-8},
 location = {San Jose, California, USA},
 pages = {283--294},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1993498.1993532},
 doi = {http://doi.acm.org/10.1145/1993498.1993532},
 acmid = {1993532},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {automated testing, compiler defect, compiler testing, random program generation, random testing},
}

Entry made up.

@inproceedings{cil02,
  title  = {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs},
  author = {George C. Necula and Scott McPeak and Shree P. Rahul and Westley Weimer},
  booktitle = {Compiler Construction: 11th International Conference (CC 2002)},
  pages = {213--228},
  year   = 2002,
  editor = {R. Nigel Horspool},
  volume = 2304,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  doi = {10.1007/3-540-45937-5_16}
}

Entry made up.

@manual{gccint4.4,
  title = {{GNU} {Compiler} {Collection} {(GCC)} Internals},
  note = {Version 4.4.3},
  organization = {Free Software Foundation},
  year = 2008
}

Entry from ACM Digital Library with corrected accent, capital.

@inproceedings{Ellison:2012:EFS:2103656.2103719,
 author = {Ellison, Chucky and Ro{\c s}u, Grigore},
 title = {An executable formal semantics of {C} with applications},
 booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '12},
 year = {2012},
 isbn = {978-1-4503-1083-3},
 location = {Philadelphia, PA, USA},
 pages = {533--544},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2103656.2103719},
 doi = {10.1145/2103656.2103719},
 acmid = {2103719},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {C, k, semantics},
} 

Entry from Springerlink. Note -> DOI.

@Inproceedings{clockfunctions,
  author    = "S. Ray and J S. Moore",
  title     = "{Proof Styles in Operational Semantics}",
  editor    = "A. J. Hu and A. K. Martin",
  booktitle = "{Proceedings of the $5$th International Conference on 
                Formal Methods in Computer-Aided Design (FMCAD 2004)}",
  series    = "{LNCS}",
  volume    = "3312",
  address   = "{Austin, TX}",
  publisher = "{Springer}",
  month     = nov,
  pages     = "67-81",
  year      = 2004
}

@article {piton,
   author = {Moore, J Strother},
   title = {A mechanically verified language implementation},
   journal = {Journal of Automated Reasoning},
   publisher = {Springer Netherlands},
   issn = {0168-7433},
   keyword = {Computer Science},
   pages = {461-492},
   volume = {5},
   issue = {4},
   url = {http://dx.doi.org/10.1007/BF00243133},
   doi = {10.1007/BF00243133},
   abstract = {This paper briefly describes a programming language, its implementation on a microprocessor via a compiler and link-assembler, and the mechanically checked proof of the correctness of the implementation. The programming language, called Piton, is a high-level assembly language designed for verified applications and as the target language for high-level language compilers. It provides executeonly programs, recursive subroutine call and return, stack based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven abstract data types including integers, data addresses, program addresses and subroutine names. Piton is formally specified by an interpreter written for it in the computational logic of Boyer and Moore. Piton has been implemented on the FM8502, a general purpose microprocessor whose gate-level design has been mechanically proved to implement its machine code interpreter. The FM8502 implementation of Piton is via a function in the Boyer-Moore logic which maps a Piton initial state into an FM8502 binary core image. The compiler and link-assembler are both defined as functions in the logic. The implementation requires approximately 36K bytes and 1400 lines of prettyprinted source code in the Pure Lisp-like syntax of the logic. The implementation has been mechanically proved correct. In particular, if a Piton state can be run to completion without error, then the final values of all the global data structures can be ascertained from an inspection of an FM8502 core image obtained by running the core image produced by the compiler and link-assembler. Thus, verified Piton programs running on FM8502 can be thought of as having been verified down to the gate level.},
   year = {1989}
}

Entry from Springerlink, plus accent fix and doi changed to doi rather than
note. And capital.

@incollection {springerlink:10.1007/978-3-642-22863-6_17,
   author = {Lochbihler, Andreas and Bulwahn, Lukas},
   affiliation = {Karlsruher Institut f{\"{u}}r Technologie, Germany},
   title = {Animating the Formalised Semantics of a {J}ava-Like Language},
   booktitle = {Interactive Theorem Proving},
   series = {Lecture Notes in Computer Science},
   editor = {van Eekelen, Marko and Geuvers, Herman and Schmaltz, Julien and Wiedijk, Freek},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-22862-9},
   keyword = {Computer Science},
   pages = {216-232},
   volume = {6898},
   url = {http://dx.doi.org/10.1007/978-3-642-22863-6_17},
   doi = {10.1007/978-3-642-22863-6_17},
   abstract = {Considerable effort has gone into the techniques of extracting executable code from formal specifications and animating them. We show how to apply these techniques to the large JinjaThreads formalisation. It models a substantial subset of multithreaded Java source and bytecode in Isabelle/HOL and focuses on proofs and modularity whereas code generation was of little concern in its design. Employing Isabelle’s code generation facilities, we obtain a verified Java interpreter that is sufficiently efficient for running small Java programs. To this end, we present refined implementations for common notions such as the reflexive transitive closure and Russell’s definite description operator. From our experience, we distill simple guidelines on how to develop future formalisations with executability in mind.},
   year = {2011}
}

Entry from ACM Digital Library (I've only searched it for testing, not read it).

@article{Klein:2006:MMJ:1146809.1146811,
 author = {Klein, Gerwin and Nipkow, Tobias},
 title = {A machine-checked model for a {Java}-like language, virtual machine, and compiler},
 journal = {ACM Trans. Program. Lang. Syst.},
 issue_date = {July 2006},
 volume = {28},
 number = {4},
 month = jul,
 year = {2006},
 issn = {0164-0925},
 pages = {619--695},
 numpages = {77},
 url = {http://doi.acm.org/10.1145/1146809.1146811},
 doi = {10.1145/1146809.1146811},
 acmid = {1146811},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Java, operational semantics, theorem proving},
} 

Entry from sciencedirect. Remove dodgy number and note.

@article{Leinenbach200823,
title = "Pervasive Compiler Verification – From Verified Programs to Verified Systems",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "217",
pages = "23 - 40",
year = "2008",
issn = "1571-0661",
doi = "10.1016/j.entcs.2008.06.040",
url = "http://www.sciencedirect.com/science/article/pii/S1571066108003836",
author = "Dirk Leinenbach and Elena Petrova",
keywords = "Compiler Verification",
keywords = "Theorem Proving",
keywords = "System Verification",
keywords = "HOL",
keywords = "Hoare Logic",
abstract = "We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties from the C0 layer to the assembler and hardware layers. The compiler verification is split into two parts: the correctness of the compiling specification (which can be translated to executable ML code via Isabelle's code generator) and the correctness of a C0 implementation of this specification. We also sketch a method to solve the boot strap problem, i.e., how to obtain a trustworthy binary of the C0 compiler from its C0 implementation. Ultimately, this allows to prove pervasively the correctness of compiled C0 programs in the real system."
}

@book{while,
 author = {Nielson, Flemming and Nielson, Hanne R. and Hankin, Chris},
 title = {Principles of Program Analysis},
 year = {1999},
 isbn = {3540654100},
 publisher = {Springer-Verlag New York, Inc.},
 address = {Secaucus, NJ, USA},
}

@incollection{easylabelling,
year={2012},
isbn={978-3-642-32468-0},
booktitle={Formal Methods for Industrial Critical Systems},
volume={7437},
series={Lecture Notes in Computer Science},
editor={Stoelinga, Mariëlle and Pinger, Ralf},
doi={10.1007/978-3-642-32469-7_3},
title={Certifying and Reasoning on Cost Annotations in {C} Programs},
url={http://dx.doi.org/10.1007/978-3-642-32469-7_3},
publisher={Springer Berlin Heidelberg},
author={Ayache, Nicolas and Amadio, RobertoM. and R\'egis-Gianas, Yann},
pages={32-46}
}

@incollection{functionallabelling,
year={2012},
isbn={978-3-642-32494-9},
booktitle={Foundational and Practical Aspects of Resource Analysis},
volume={7177},
series={Lecture Notes in Computer Science},
editor={Peña, Ricardo and Eekelen, Marko and Shkaravska, Olha},
doi={10.1007/978-3-642-32495-6_5},
title={Certifying and Reasoning on Cost Annotations of Functional Programs},
url={http://dx.doi.org/10.1007/978-3-642-32495-6_5},
publisher={Springer Berlin Heidelberg},
author={Amadio, RobertoM. and R\'egis-Gianas, Yann},
pages={72-89},
note={Extended version to appear in Higher Order and Symbolic Computation, 2013}
}

@inproceedings{framaC,
 author = {Cuoq, Pascal and Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
 title = {Frama-C: a software analysis perspective},
 booktitle = {Proceedings of the 10th international conference on Software Engineering and Formal Methods},
 series = {SEFM'12},
 year = {2012},
 isbn = {978-3-642-33825-0},
 location = {Thessaloniki, Greece},
 pages = {233--247},
 numpages = {15},
 url = {http://dx.doi.org/10.1007/978-3-642-33826-7_16},
 doi = {10.1007/978-3-642-33826-7_16},
 acmid = {2404250},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 

@article{cerco,
  INIauthor    = {R. Amadio and A. Asperti and N. Ayache and
                  B. Campbell and D. Mulligan and R. Pollack and
                  Y. R{\'e}gis-Gianas and C. {Sacerdoti Coen} and I.
                  Stark},
  author    = {Roberto Amadio and Andrea Asperti and Nicholas Ayache and
                  Brian Campbell and Dominic Mulligan and Randy Pollack and
                  Yann R{\'e}gis-Gianas and Claudio {Sacerdoti Coen} and Ian
                  Stark},
  title     = {Certified Complexity},
  journal   = {Procedia Computer Science},
  volume    = 7,
  year      = 2011,
  pages     = {175--177},
  doi       = {10.1016/j.procs.2011.09.054}
}

Entry from springerlink with accent corrections.

@incollection {springerlink:10.1007/978-3-642-11970-5_13,
   author = {Rideau, Silvain and Leroy, Xavier},
   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure 45 rue d’Ulm 75005 Paris France},
   title = {Validating Register Allocation and Spilling},
   booktitle = {Compiler Construction},
   series = {Lecture Notes in Computer Science},
   editor = {Gupta, Rajiv},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-11969-9},
   keyword = {Computer Science},
   pages = {224-243},
   volume = {6011},
   url = {http://dx.doi.org/10.1007/978-3-642-11970-5_13},
   doi = {10.1007/978-3-642-11970-5_13},
   abstract = {Following the translation validation approach to high-assurance compilation, we describe a new algorithm for validating a posteriori the results of a run of register allocation. The algorithm is based on backward dataflow inference of equations between variables, registers and stack locations, and can cope with sophisticated forms of spilling and live range splitting, as well as many architectural irregularities such as overlapping registers. The soundness of the algorithm was mechanically proved using the Coq proof assistant.},
   year = {2010}
}

Entry from springerlink with accent and title corrections.

@incollection {springerlink:10.1007/978-3-642-28869-2_20,
   author = {Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and Leroy, Xavier},
   affiliation = {{\'{E}}cole Normale Sup{\'{e}}rieure, France},
   title = {Validating {LR(1)} Parsers},
   booktitle = {Programming Languages and Systems},
   series = {Lecture Notes in Computer Science},
   editor = {Seidl, Helmut},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-28868-5},
   keyword = {Computer Science},
   pages = {397-416},
   volume = {7211},
   url = {http://dx.doi.org/10.1007/978-3-642-28869-2_20},
   doi = {10.1007/978-3-642-28869-2_20},
   abstract = {An LR (1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar and an automaton , checks that and agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct . The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.},
   year = {2012}
}


@misc{fopara,
  author = {R.~M. Amadio and N.~Ayache and F.~Bobot and J.~P. Boender and B.~Campbell and I.~Garnier and A.~Madet and J.~McKinna and D.~P. Mulligan and M.~Piccolo and R.~Pollack and Y.~R\'egis-Gianas and C.~Sacerdoti Coen and I.~Stark and P.~Tranquilli},
  title = {Certified Complexity (CerCo)},
  note = {Submitted to FOPARA 2013},
  year = 2013
}

@techreport{EDI-INF-RR-1412,
  author = {Brian Campbell and Randy Pollack},
  title = {Executable Formal Semantics of {C}},
  institution = {School of Informatics, University of Edinburgh},
  year = 2010,
  number = {EDI-INF-RR-1412}
}

Entry from springerlink, with obvious capitalisation correction and note -> doi.

@incollection {springerlink:10.1007/3-540-49519-3_22,
   author = {Strother Moore, J.},
   affiliation = {The University of Texas at Austin Department of Computer Sciences Austin TX 78712-1188},
   title = {Symbolic Simulation: An {ACL2} Approach},
   booktitle = {Formal Methods in Computer-Aided Design},
   series = {Lecture Notes in Computer Science},
   editor = {Gopalakrishnan, Ganesh and Windley, Phillip},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-540-65191-8},
   keyword = {Computer Science},
   pages = {530-530},
   volume = {1522},
   url = {http://dx.doi.org/10.1007/3-540-49519-3_22},
   doi = {10.1007/3-540-49519-3_22},
   abstract = {Executable formal specification can allow engineers to test (or simulate ) the specified system on concrete data before the system is implemented. This is beginning to gain acceptance and is just the formal analogue of the standard practice of building simulators in conventional programming languages such as C. A largely unexplored but potentially very useful next step is symbolic simulation , the “execution” of the formal specification on indeterminant data. With the right interface, this need not require much additional training of the engineers using the tool. It allows many tests to be collapsed into one. Furthermore, it familiarizes the working engineer with the abstractions and notation used in the design, thus allowing team members to speak clearly to one another. We illustrate these ideas with a formal specification of a simple computing machine in ACL2. We sketch some requirements on the interface, which we call a symbolic spreadsheet .},
   year = {1998}
}


Entry from springerlink. Note -> doi.

@incollection {springerlink:10.1007/978-3-642-03359-9_11,
   author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
   affiliation = {Technische Universitüt München Institut für Informatik Boltzmannstraße 3 85748 Garching Germany},
   title = {Turning Inductive into Equational Specifications},
   booktitle = {Theorem Proving in Higher Order Logics},
   series = {Lecture Notes in Computer Science},
   editor = {Berghofer, Stefan and Nipkow, Tobias and Urban, Christian and Wenzel, Makarius},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-03358-2},
   keyword = {Computer Science},
   pages = {131-146},
   volume = {5674},
   url = {http://dx.doi.org/10.1007/978-3-642-03359-9_11},
   doi = {10.1007/978-3-642-03359-9_11},
   abstract = {Inductively defined predicates are frequently used in formal specifications. Using the theorem prover Isabelle , we describe an approach to turn a class of systems of inductively defined predicates into a system of equations using data flow analysis; the translation is carried out inside the logic and resulting equations can be turned into functional program code in SML , OCaml or Haskell using the existing code generator of Isabelle . Thus we extend the scope of code generation in Isabelle from functional to functional-logic programs while leaving the trusted foundations of code generation itself intact.},
   year = {2009}
}

@Unpublished{loopoptimizations,
 author = {Paolo Tranquilli},
 title = {Indexed Labels for Loop Iteration Dependent Costs},
 note = {to appear in Electronic Proceedings in Theoretical Computer Science, proceedings of Quantitative Aspects of
Programming Languages and Systems (QAPL 2013)},
 month = jan,
 year = {2013},
 url = {http://www.cs.unibo.it/~tranquil/content/docs/indlabels.pdf}
}

@incollection{matita1,
year={2011},
isbn={978-3-642-22437-9},
booktitle={Automated Deduction – CADE-23},
volume={6803},
series={Lecture Notes in Computer Science},
editor={Bjørner, Nikolaj and Sofronie-Stokkermans, Viorica},
doi={10.1007/978-3-642-22438-6_7},
title={The Matita Interactive Theorem Prover},
url={http://dx.doi.org/10.1007/978-3-642-22438-6_7},
publisher={Springer Berlin Heidelberg},
author={Asperti, Andrea and Ricciotti, Wilmer and Sacerdoti Coen, Claudio and Tassi, Enrico},
pages={64-69}
}

@article{matita2,
year={2007},
issn={0168-7433},
journal={Journal of Automated Reasoning},
volume={39},
issue={2},
doi={10.1007/s10817-007-9070-5},
title={User Interaction with the Matita Proof Assistant},
url={http://dx.doi.org/10.1007/s10817-007-9070-5},
publisher={Springer Netherlands},
keywords={Proof assistant; Interactive theorem proving; Digital libraries; XML; Mathematical knowledge management; Authoring},
author={Asperti, Andrea and Sacerdoti Coen, Claudio and Tassi, Enrico and Zacchiroli, Stefano},
pages={109-139},
language={English}
}