Changes between Version 49 and Version 50 of WikiStart


Ignore:
Timestamp:
May 15, 2013, 11:16:56 AM (4 years ago)
Author:
sacerdot
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v49 v50  
    7171  * An executable formalisation of the MCS-51 microprocessor in Matita. Dominic P. Mulligan and Claudio Sacerdoti Coen.  Submitted to FMCAD 2011.
    7272  * [http://hal.archives-ouvertes.fr/hal-00524715/fr/ Certifying cost annotations in compilers].  Roberto M. Amadio, Nicolas Ayache, Yann Régis-Gianas and Ronan Saillard.  Technical Report, Université Paris Diderot (Paris 7).
    73   * A Canonical Locally Named Representation of Binding, R. Pollack, M. Sato and W. Ricciotti, Journal of Automated Reasoning,
    74   * Certifying and reasoning on cost annotations of functional programs, R.M. Amadio, Y. Regis‐Gianas, In proceedings of Foundations and Practical Aspects of Resource Analysis (FOPARA 2011), LNCS, 71277:72‐89,
    75 
     73  * [http://homepages.inf.ed.ac.uk/rpollack/export/PollackSatoRicciottiJAR.pdf A Canonical Locally Named Representation of Binding], R. Pollack, M. Sato and W. Ricciotti, Journal of Automated Reasoning,
     74  * [http://arxiv.org/abs/1110.2350 Certifying and reasoning on cost annotations of functional programs], R.M. Amadio, Y. Regis‐Gianas, In proceedings of Foundations and Practical Aspects of Resource Analysis (FOPARA 2011), LNCS, 71277:72‐89
     75  * [http://arxiv.org/abs/1102.4971 An Elementary Affine λ‐Calculus with Multithreading and Side Effects], A. Madet, R.M. Amadio., In Proceedings Typed Lambda Calculi and Applications (TLCA 2011), Springer LNCS 6690:138‐152, 2011
     76  * Certified Complexity, R. Amadio, A. Asperti, N. Ayache, B. Campbell, D. Mulligan, R. Pollack, Y. Regis‐Gianas, C. Sacerdoti Coen, I. Stark, in Procedia Computer Science, Volume 7, 2011, Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11), 175‐177
     77  * [http://matita.cs.unibo.it/PAPERS/system_description2011.pdf The Matita Interactive Theorem Prover], A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi, In Automated Deduction – CADE‐23, LECTURE NOTES IN COMPUTER SCIENCE, ISBN:978‐3‐642‐22437‐9, Pages 64‐69, Volume 6803, Year 2011
     78  * [http://hal.inria.fr/hal-00702665/ Certifying and Reasoning on Cost Annotations in C Programs], N. Ayache, R.M. Amadio, Y. Régis‐Gianas, in Proc. FMICS, Springer LNCS 7437: 32‐46, 2012
     79  * [http://www.cs.unibo.it/~asperti/PAPERS/rating.pdf Rating Disambiguation Errors], A. Asperti, W. Ricciotti, In Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP 2012), LNCS, Volume 7679, Pages 240‐‐255, Springer, 2012
     80  * Certifying and reasoning on cost annotations of functional programs, R.M. Amadio, Y. Régis‐Gianas, in Higher‐order and Symbolic Computation, to appear, 2012
     81  * [http://proval.lri.fr/publications/bobot12icfem.pdf Separation Predicates: A Taste of Separation Logic in First‐Order Logic], F. Bobot, J.‐C. Filliatre, in Proc. IFCEM, Springer LNCS 7635:167‐181, 2012
     82  * [http://www.cs.unibo.it/~asperti/PAPERS/matitaweb.pdf A Web Interface for Matita], A. Asperti, W. Ricciotti, In Proceedings of the Conference on Intelligent Computer Mathematics (CICM 2012), LNAI, Volume 7362/2012, Pages 417‐421
     83  * [http://arxiv.org/abs/1206.4833 Indexed Realizability for Bounded‐Time Programming with References and Type Fixpoints], A. Brunel, A. Madet, In Proc. APLAS, Springer LNCS 7705:264‐279 , 2012
     84  * [http://hal.inria.fr/docs/00/73/55/44/PDF/ppdp19-madet.pdf A polynomial time λ‐calculus with multithreading and side effects], A. Madet in Proc. ACM‐PPDP, pages 55‐66, 2012
     85  * [http://homepages.inf.ed.ac.uk/bcampbe2/compcert/ An executable semantics for CompCert C], B. Campbell, in Proceedings of Certified Proofs and Programs 2012, LNCS 7679:60‐75, 2012
     86  * On the Correctness of an Optimising Assembler for the Intel MCS‐51 Microprocessor, D. Mulligan, C. Sacerdoti Coen, in Proceedings of Certified Proofs and Programs 2012, LNCS 7679:43‐59, 2012: raw-attachment:cpp-2011.pdf
     87  * [http://www.cs.unibo.it/~tranquil/content/docs/indlabels.pdf Indexed Labels for Loop Iteration Dependent Costs], P. Tranquilli, in Proceedings of the 11th International Workshop on Quantitative Aspects of Programming Languages and
     88Systems (QAPL 2013), Rome, 23rd‐24th March 2013, Electronic Proceedings in Theoretical Computer Science, 2013
    7689=== Learn More ===
    7790 1. Concept and Objectives, progress beyond state-of-the-art, S/T methodology and work plan