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 Times are displayed in time zone: Greenwich Mean Time : Belfast change
|15:00 - 15:23|
|Prototyping a Query Compiler using Coq (Experience Report)|
Joshua AuerbachIBM Research, Martin HirzelIBM Research, Louis MandelIBM Research, Avraham ShinnarIBM Research, Jerome SimeonIBM ResearchDOI
|15:23 - 15:46|
|A Framework for Adaptive Differential Privacy|
Daniel Winograd-CortUniversity of Pennsylvania, USA, Andreas HaeberlenUniversity of Pennsylvania, USA, Aaron RothUniversity of Pennsylvania, USA, Benjamin C. PierceUniversity of PennsylvaniaDOI
|15:46 - 16:10|
|Symbolic Conditioning of Arrays in Probabilistic Programs|