SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 09:20 - 09:40 at SPLASH-I - R-2 Chair(s): Sheng Chen, Adrian Sampson
Thu 19 Nov 2020 21:20 - 21:40 at SPLASH-I - R-2 Chair(s): Sheng Chen, John Peter Campora

Garbage collectors relieve the programmer from manual memory
management, but lead to compiler-generated machine code that can
behave differently (e.g.\ out-of-memory errors) from the source
code. To ensure that the generated code behaves exactly like the
source code, programmers need a way to answer questions of the form:
what is a sufficient amount of memory for
my program to never reach an out-of-memory error?

This paper develops a cost semantics that can answer such
questions for CakeML programs. The work described in this paper is
the first to be able to answer such questions with proofs in the
context of a language that depends on garbage collection. We
demonstrate that positive answers can be used to transfer liveness
results proved for the source code to liveness guarantees about the
generated machine code. Without guarantees about space usage, only
safety results can be transferred from source to machine code.

Our cost semantics is phrased in terms of an abstract intermediate
language of the CakeML compiler, but results proved at that level
map directly to the space cost of the compiler-generated machine
code. All of the work described in this paper has been developed in
the HOL4 theorem prover.

Thu 19 Nov

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
R-2OOPSLA at SPLASH-I +12h
Chair(s): Sheng Chen University of Louisiana at Lafayette, Adrian Sampson Cornell University
09:00
20m
Talk
Automatic and Efficient Variability-Aware Lifting of Functional Programs
OOPSLA
Ramy Shahin University of Toronto, Marsha Chechik University of Toronto
Link to publication DOI Pre-print Media Attached
09:20
20m
Talk
Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
OOPSLA
Alejandro Gómez-Londoño Chalmers University of Technology, Johannes Åman Pohjola Data61 at CSIRO / UNSW, Hira Taqdees Syeda Chalmers University of Technology, Magnus O. Myreen Chalmers University of Technology, Yong Kiam Tan Carnegie Mellon University
Link to publication DOI Media Attached
09:40
20m
Talk
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
OOPSLA
Yiyun Liu University of Maryland at College Park, James Parker University of Maryland at College Park, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California at Santa Cruz, Michael Hicks University of Maryland at College Park, Niki Vazou IMDEA Software Institute
Link to publication DOI Media Attached
10:00
20m
Talk
Towards a Formal Foundation of Intermittent Computing
OOPSLA
Milijana Surbatovich Carnegie Mellon University, Brandon Lucia Carnegie Mellon University, Limin Jia Carnegie Mellon University
Link to publication DOI Media Attached
21:00 - 22:20
R-2OOPSLA at SPLASH-I
Chair(s): Sheng Chen University of Louisiana at Lafayette, John Peter Campora University of Louisiana at Lafayette
21:00
20m
Talk
Automatic and Efficient Variability-Aware Lifting of Functional Programs
OOPSLA
Ramy Shahin University of Toronto, Marsha Chechik University of Toronto
Link to publication DOI Pre-print Media Attached
21:20
20m
Talk
Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
OOPSLA
Alejandro Gómez-Londoño Chalmers University of Technology, Johannes Åman Pohjola Data61 at CSIRO / UNSW, Hira Taqdees Syeda Chalmers University of Technology, Magnus O. Myreen Chalmers University of Technology, Yong Kiam Tan Carnegie Mellon University
Link to publication DOI Media Attached
21:40
20m
Talk
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
OOPSLA
Yiyun Liu University of Maryland at College Park, James Parker University of Maryland at College Park, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California at Santa Cruz, Michael Hicks University of Maryland at College Park, Niki Vazou IMDEA Software Institute
Link to publication DOI Media Attached
22:00
20m
Talk
Towards a Formal Foundation of Intermittent Computing
OOPSLA
Milijana Surbatovich Carnegie Mellon University, Brandon Lucia Carnegie Mellon University, Limin Jia Carnegie Mellon University
Link to publication DOI Media Attached