Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Prototyping a Query Compiler using Coq (Experience Report)

Series
International Conference on Functional Programming 2017
Video Embed
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.
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.

More in this series

View Series
International Conference on Functional Programming 2017

A Unified Approach to Solving Seven Programming Problems (Functional Pearl)

William E. Byrd, University of Utah, USA, gives the fourth presentation in the second panel, Functional Programming Techniques, in the ICFP 2017 conference.
Previous
International Conference on Functional Programming 2017

A Framework for Adaptive Differential Privacy

Daniel Winograd-Cort University of Pennsylvania, USA, gives the first presentation in the third panel, Applications, in the ICFP 2017 conference. Co-written by Andreas Haeberlen and Aaron Roth, University of Pennsylvania, USA.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Louis Mandel
Keywords
computing
programming
technology
Department: Department of Computer Science
Date Added: 12/12/2017
Duration: 00:19:19

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford