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 |
| 88 | Systems (QAPL 2013), Rome, 23rd‐24th March 2013, Electronic Proceedings in Theoretical Computer Science, 2013 |