Computer Science Speaking Skills Talk
— 3:00pm
Location:
Virtual Presentation - ET
-
Remote Access - Zoom
Speaker:
JONATHAN STERLING
,
Ph.D. Student
https://www.jonmsterling.com/
Abstraction, composition, and the phase distinction
Programmers use abstraction to hide representation details from ourselves: either to avoid mistakes (e.g. confusing a list index with a length) or to exploit representation invariants (e.g. two implementations of the QUEUE interface are indistinguishable). These abstraction boundaries can unfortunately impede the linking of smaller program units into efficient composite programs, because compilers must exploit representation details in order to produce efficient code. Sometimes seen as the "waterloo of separate compilation", the need to break abstraction is answered by whole-program analysis techniques that break all abstractions (as in the Mlton compiler for Standard ML). Separate compilation, however, has a number of advantages including speed, parallelization, and elegance.
We present an alternative type theoretic account of abstraction-breaking during compilation based on the famous phase distinction of ML languages; rather than distinguishing between compiletime and runtime, we focus on separating "devtime" from compiletime. Our framework allows the programmer to selectively reveal representation details to the compiler without giving up the representation independence properties guaranteed by "devtime" type correctness. We also describe an application to the problem of printf-debugging, which is ordinarily obstructed by abstraction.
Joint work with Robert Harper.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.
Zoom Participation. See announcement.
For More Information:
deb@cs.cmu.edu