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): Adrian Sampson, Sheng Chen
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
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20: R-2OOPSLA at SPLASH-I +12h
Chair(s): Adrian SampsonCornell University, Sheng ChenUniversity of Louisiana at Lafayette
09:00 - 09:20
Talk
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
09:20 - 09:40
Talk
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
09:40 - 10:00
Talk
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
10:00 - 10:20
Talk
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached
21:00 - 22:20: R-2OOPSLA at SPLASH-I
Chair(s): Sheng ChenUniversity of Louisiana at Lafayette, John Peter CamporaUniversity of Louisiana at Lafayette
21:00 - 21:20
Talk
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
21:20 - 21:40
Talk
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
21:40 - 22:00
Talk
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
22:00 - 22:20
Talk
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached