wiki:Proposal4

Version 1 (modified by sacerdot, 7 years ago) (diff)

--

Bibliography

A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi. A compact kernel for the calculus of inductive constructions. In Special Issue on Iteractive Proving and Proof Checking of the Academy Journal of Engineering Sciences (Sadhana) of the Indian Academy of Sciences. SADHANA (BANGALORE). vol. 34(1), pp. 71 - 144 ISSN: 0256-2499, 2009.

A.Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. User Interaction with the Matita Proof Assistant. Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving, 39(2), pp.109-139, 2007.

A. Asperti, C. Sacerdoti Coen, E. Tassi, S. Zacchiroli. Crafting a Proof Assistant In Proceedings of Types 2006, Lecture Notes in Computer Science (LNCS), Vol. 4502, pp. 18-32, 2007.

Aydemir and Bohannon and Fairbairn and Foster and Pierce and Sewell and Vytiniotis and Washburn and Weirich and Zdancewic. Mechanized metatheory for the masses: The POPLmark Challenge. International Conference on Theorem Proving in Higher Order Logics (TPHOLs) 2005.

B.Aydemir, A.Chargueraud, B.C.Pierce, R.Pollack, S.Weiric. Engineering Formal Methatheory. Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008)

A.W.Appel, J.Palsberg. Modern Compiler Implementation in Java. Cambridge University Press, 1998.

J.Avigad, K.Donnelly, D.Gray, P.Raff. A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic (TOCL). Volume 9, Issue 1 (December 2007)

A.Chlipala. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. Proceedings of ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI'07). June 2007.

Maulik A. Dave. Compiler verification: a bibliography. ACM SIGSOFT Software Engineering Notes, Volume 28, Issue 6 (Nov. 2003).

A. Dold, V. Vialard. A Mechanically Verified Compiling Specification for a Lisp Compiler. Proc. of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2001), December 13-15, Bangalore, India. Springer LNCS 2245.

J-C. Filliatre, C Marché. Multi-Prover Verification of C Programs. In Sixth International Conference on Formal Engineering Methods (ICFEM), volume 3308 of Lecture Notes in Computer Science, pages 15-29, Seattle, November 2004. Springer-Verlag.

G. Gonthier. Formal Proof-The Four-Color Theorem. Notices of the AMS, Vol 55, no. 11, pp. 1382-1393.

G.Goos, W.Zimmermann. Verification of Compilers, Bernhard Steffen and Ernst Rüdiger Olderog (Ed.), Correct System Design, p. 201-230, Springer, Nov 1999.

T.C.Hales. Formalizing the Proof of the Kepler Conjecture. Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004), Park City, Utah, USA, September 14-17, 2004. K.Slind, A.Bunker, G.Gopalakrishnan (Eds.) LNCS 3223 Springer 2004.

G.Klein, T.Nipkow. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 28 , Issue 4 (July 2006).

D.Mackenzie. What in the Name of Euclid Is Going On Here? Science 4 March 2005. Vol. 307. no. 5714, pp. 1402 - 1403.

S.S.Muchnick. Advanced Compiler Design Implementation. Morgan Kaufmann, 1997.

:: D.Leinenbach, W.J.Paul, E.Petrova. Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes. SEFM 2005: 2-12.

X.Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Proceedings of Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006)

X.Leroy. Formal verification of a realistic compiler. To appear in Communications of the ACM, 2009.

X.Leroy, S.Blazy, Z.Dargaye. Formal verification of a C compiler front-end. Proceedings of Formal Methods 2006, LNCS 4085.

X.Leroy, J-B Tristan. Formal verification of translation validators: A case study on instruction scheduling optimizations. Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008)

S.Peyton Jones, N.Ramsey, F.Reig. C-: A portable assembly language that supports garbage collection. Invited talk at PPDP'99, LNCS Vol1702, pp.1-28.

M.Strecker. Formal Verification of a Java Compiler in Isabelle. Proceedings of the 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002. LNCS vol.2392, pp.63-77.