Yang, Lu; Zhou, Chaochen; Zhan, Naijun; Xia, Bican Recent advances in program verification through computer algebra. (English) Zbl 1267.68099 Front. Comput. Sci. China 4, No. 1, 1-16 (2010). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{L. Yang} et al., Front. Comput. Sci. China 4, No. 1, 1--16 (2010; Zbl 1267.68099) Full Text: DOI
Bertot, Yves A short presentation of Coq. (English) Zbl 1165.68449 Mohamed, Otmane Ait (ed.) et al., Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18–21, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-71065-3/pbk). Lecture Notes in Computer Science 5170, 12-16 (2008). MSC: 68T15 PDFBibTeX XMLCite \textit{Y. Bertot}, Lect. Notes Comput. Sci. 5170, 12--16 (2008; Zbl 1165.68449) Full Text: DOI
Mulhern, Anne; Fischer, Charles; Liblit, Ben Tool support for proof engineering. (English) Zbl 1278.68275 Autexier, Serge (ed.) et al., Proceedings of the 7th workshop on user interfaces for theorem provers (UITP 2006), Seattle, WA, USA, August 21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 2, 75-86 (2007). MSC: 68T15 PDFBibTeX XMLCite \textit{A. Mulhern} et al., Electron. Notes Theor. Comput. Sci. 174, No. 2, 75--86 (2007; Zbl 1278.68275) Full Text: DOI
Jacobs, Bart; Smetsers, Sjaak; Schreur, Ronny Wichers Code-carrying theories. (English) Zbl 1121.68030 Formal Asp. Comput. 19, No. 2, 191-203 (2007). MSC: 68N30 68N18 68T15 PDFBibTeX XMLCite \textit{B. Jacobs} et al., Formal Asp. Comput. 19, No. 2, 191--203 (2007; Zbl 1121.68030) Full Text: DOI
Berger, Ulrich; Berghofer, Stefan; Letouzey, Pierre; Schwichtenberg, Helmut Program extraction from normalization proofs. (English) Zbl 1095.03016 Stud. Log. 82, No. 1, 25-49 (2006). MSC: 03B70 03B35 03B40 03F05 68N30 PDFBibTeX XMLCite \textit{U. Berger} et al., Stud. Log. 82, No. 1, 25--49 (2006; Zbl 1095.03016) Full Text: DOI HAL
Berger, Ulrich Uniform Heyting arithmetic. (English) Zbl 1081.03057 Ann. Pure Appl. Logic 133, No. 1-3, 125-148 (2005). MSC: 03F30 03F07 03B70 PDFBibTeX XMLCite \textit{U. Berger}, Ann. Pure Appl. Logic 133, No. 1--3, 125--148 (2005; Zbl 1081.03057) Full Text: DOI
Parent, C. Developing certified programs in the system Coq. The program tactic. (English) Zbl 1527.68134 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 291-312 (1994). MSC: 68Q60 03B70 68N30 68V15 PDFBibTeX XMLCite \textit{C. Parent}, Lect. Notes Comput. Sci. 806, 291--312 (1994; Zbl 1527.68134) Full Text: DOI
Hayashi, Susumu Logic of refinement types. (English) Zbl 1527.68040 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 108-126 (1994). MSC: 68N30 03B38 03B40 03B70 PDFBibTeX XMLCite \textit{S. Hayashi}, Lect. Notes Comput. Sci. 806, 108--126 (1994; Zbl 1527.68040) Full Text: DOI