What I Always Wanted to Know about Second Class Valuesfestschrift
Second class values are allocated on the run-time stack and they may contain pointers
to other values on the stack. They were first discussed in connection with the
infamous funarg problem, but then forgotten as heap-allocated closures were
discovered.
Recent work has resurrected the interest in second class values as they allow us
to safely allocate some data structures (e.g., closures) on the run-time stack.
This approach has the advantage of avoiding the cost and the
unpredictable timing of garbage collection for
these structures as their deallocation takes no extra time when the
stack is popped.
A system with qualified types ensures that second class values do not
escape across stack pops.
We take a second look at this work and extend/modify their formal framework
with first-class and second-class references in the style of ML. Along
the way we answer a question that left us mystified in the previous
work: What, exactly, is the meaning of a type qualifier?
Wed 15 OctDisplayed time zone: Perth change
13:40 - 15:25 | Proof we need. Proof!OlivierFest at Peony West Chair(s): Xavier Rival Inria - CNRS - Ecole Normale Superieure de Paris - PSL University | ||
13:40 25mTalk | What I Always Wanted to Know about Second Class Valuesfestschrift OlivierFest Peter Thiemann University of Freiburg DOI | ||
14:05 25mTalk | A Tale of Two Zippersfestschrift OlivierFest DOI | ||
14:30 25mTalk | Verified Nanopasses for Compiling Conditionalsfestschrift OlivierFest Jeremy G. Siek Indiana University DOI | ||
14:55 15mTalk | Verifying Effectful Programs via Answer-Type Modification OlivierFest Taro Sekiyama National Institute of Informatics | ||
15:10 15mTalk | From Delimited Continuations to Staged Logics OlivierFest Wei-Ngan Chin National University of Singapore, Darius Foo National University of Singapore, Yahui Song Standard Chartered Bank | ||
