Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Mon 4 Sep 2017 15:00 - 15:23 at L1 - Applications Chair(s): Alexandra Silva

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.

Mon 4 Sep

Displayed time zone: Belfast change

15:00 - 16:10
ApplicationsResearch Papers at L1
Chair(s): Alexandra Silva University College London
15:00
23m
Talk
Prototyping a Query Compiler using Coq (Experience Report)
Research Papers
Joshua Auerbach IBM Research, Martin Hirzel IBM Research, Louis Mandel IBM Research, Avraham Shinnar IBM Research, Jerome Simeon IBM Research
DOI
15:23
23m
Talk
A Framework for Adaptive Differential Privacy
Research Papers
Daniel Winograd-Cort University of Pennsylvania, USA, Andreas Haeberlen University of Pennsylvania, USA, Aaron Roth University of Pennsylvania, USA, Benjamin C. Pierce University of Pennsylvania
DOI
15:46
23m
Talk
Symbolic Conditioning of Arrays in Probabilistic Programs
Research Papers
Praveen Narayanan Indiana University, USA, Chung-chieh Shan Indiana University, USA
DOI