ACL2 2014 PROCEEDINGS

Editors: Freek Verbeek and Julien Schmaltz

Authors	Title	Talk
Matt Kaufmann and J Moore	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4	Jul 12 09:30
Jared Davis and Matt Kaufmann	Industrial-Strength Documentation for ACL2	Jul 12 09:00
Harsh Raju Chamarthi, Peter Dillinger and Panagiotis Manolios	Data Definitions in ACL2 Sedan	Jul 12 11:45
Benjamin Selfridge and Eric Smith	Polymorphic Types In ACL2	Jul 12 11:15
Jónathan Heras and Ekaterina Komendantskaya	ACL2(ml): Machine-Learning for ACL2	Jul 12 12:15
Sebastiaan Joosten, Cezary Kaliszyk and Josef Urban	Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems	Jul 12 10:45
Ruben Gamboa and John Cowles	On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics	Jul 12 16:30
John Cowles and Ruben Gamboa	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis	Jul 13 09:30
Ruben Gamboa and John Cowles	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent	Jul 13 09:00
Disha Puri, Sandip Ray, Kecheng Hao and Fei Xie	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis	Jul 13 12:15
Benjamin Selfridge	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory	Jul 13 11:45
David Russinoff and John O'Leary	Modeling Algorithms in SystemC and ACL2	Jul 13 10:45
David Hardin, Jennifer Davis, David Greve and Jedidiah McClurg	Development of a Translator from LLVM to ACL2	Jul 13 11:15