Chlipala, Adam; Malecha, Gregory; Morrisett, Greg; Shinnar, Avraham; Wisnesky, Ryan Effective interactive proofs for higher-order imperative programs. (English) Zbl 1302.68087 Proceedings of the 14th ACM SIGPLAN international conference on functional programming, ICFP ’09, Edinburgh, UK, August 31 – September 2, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-332-7). ACM SIGPLAN Notices 44, No. 9, 79-90 (2009). Cited in 13 Documents MSC: 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68N18 Functional programming and lambda calculus 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:dependent types; functional programming; interactive proof assistants; separation logic Software:Coq; Spec#; Isabelle; Smallfoot; Ynot PDFBibTeX XMLCite \textit{A. Chlipala} et al., in: Proceedings of the 14th ACM SIGPLAN international conference on functional programming, ICFP '09, Edinburgh, UK, August 31 -- September 2, 2009. New York, NY: Association for Computing Machinery (ACM). 79--90 (2009; Zbl 1302.68087) Full Text: DOI Link