ECOOP 2022
Mon 6 June - Thu 7 July 2022 Berlin, Germany
Wed 8 Jun 2022 13:50 - 14:10 at Aurora Borealis 1 - Verification and Compilation Chair(s): Alexander J. Summers
Thu 23 Jun 2022 17:15 - 17:45 at Zoom - VCOOP 5 Chair(s): Philipp Haller

Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the “fast-math-style” optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers.

This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.

Wed 8 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Verification and CompilationResearch Papers / Hub Talks at Aurora Borealis 1
Chair(s): Alexander J. Summers University of British Columbia
13:30
20m
Talk
A Compiler for Sound Floating-Point ComputationsHub Talk
Hub Talks
Joao Rivera ETH Zurich, Franz Franchetti Carnegie Mellon University, USA, Markus Püschel ETH Zurich
Link to publication DOI
13:50
20m
Talk
Verified Compilation and Optimization of Floating-Point Programs in CakeMLArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Heiko Becker MPI-SWS, Robert Rabe TU Munich, Eva Darulova Uppsala University, Magnus O. Myreen Chalmers University of Technology, Zachary Tatlock University of Washington, Ramana Kumar DeepMind, Yong Kiam Tan Carnegie Mellon University, Anthony Fox Arm Limited
14:10
20m
Talk
REST: Integrating Term Rewriting with Program VerificationArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Zachary Grannan University of British Columbia, Eva Darulova Uppsala University, Alexander J. Summers University of British Columbia, Niki Vazou IMDEA Software Institute
14:30
20m
Talk
Defining Corecursive Functions in Coq Using ApproximationsVCOOP 2022ECOOP 2022
Research Papers
Vlad Rusu Inria, Lille, France, David Nowak CRIStAL, CNRS & University of Lille

Thu 23 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:45 - 18:15
VCOOP 5Research Papers at Zoom
Chair(s): Philipp Haller KTH
16:45
30m
Talk
Vincent: Green Hot Methods in the JVMVCOOP 2022
Research Papers
Kenan Liu SUNY Binghamton, Khaled Mahmoud SUNY Binghamton, USA, Joonhwan Yoo SUNY Binghamton, Yu David Liu SUNY Binghamton
Pre-print
17:15
30m
Talk
Verified Compilation and Optimization of Floating-Point Programs in CakeMLArtifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Heiko Becker MPI-SWS, Robert Rabe TU Munich, Eva Darulova Uppsala University, Magnus O. Myreen Chalmers University of Technology, Zachary Tatlock University of Washington, Ramana Kumar DeepMind, Yong Kiam Tan Carnegie Mellon University, Anthony Fox Arm Limited
17:45
30m
Talk
Compiling Volatile Correctly in JavaArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalVCOOP 2022
Research Papers
Shuyang Liu UCLA, John Bender Sandia National Laboratories, Jens Palsberg University of California at Los Angeles
Hide past events