Louis Mandel (IBM) gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Joshua Auerbach, Martin Hirzel, Avraham Shinnar, Jerome Simeon, IBM Research, USA.
Prototyping a Query Compiler using Coq (Experience Report)
Loading Video...
Designing and prototyping new features is important in many industrial projects. Functional programming and formal verification tools can prove valuable for that purpose, but lead to challenges when integrating with existing product code or when planning technology transfer.
This article reports on our experience using the Coq proof assistant as a prototyping environment for building a query compiler intended for use in IBM's ODM Insights product. We discuss the pros and cons of using Coq for this purpose and describe our methodology for porting the compiler to Java, as required for product integration.
People:
Oxford Unit:
Keywords:
More in this Series...
ICFP 2017 is the 22nd ACM SIGPLAN International Conference on Functional Programming.
ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. The conference covers the entire spectrum of work, from practice to theory, including its peripheries. This year, there are keynotes from Chris Martens and John Launchbury; unfortunately, Rich Hickey was unable to attend as originally...
Subscribe
Download Media
- Video (434.25 MB)