Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 14:00 - 14:30 at Sala X - Session 5 Chair(s): Alberto Pettorossi

It is well known that the computational content of a termination proof of a calculus is an interpreter that computes the result of an input term. Traditionally, such extraction has been tried for a calculus with deterministic reduction rules, producing the result as a value, i.e., in weak head normal form where no redexes are reduced under lambda. In this paper, we consider non-deterministic reduction rules where any redexes can be reduced, even the ones under lambda, and extract a partial evaluator, rather than an interpreter, that produces the
result in normal form. We formalize a call-by-name, simply-typed, lambda calculus in the Agda proof assistant and prove its termination using a logical predicate. We observe that the extracted program can be regarded as an online partial evaluator and present future perspectives about how we can extend the framework to a call-by-value calculus.

pepm2019-slides.pdf (main.pdf)204KiB

Tue 15 Jan

Displayed time zone: Belfast change

14:00 - 15:30
Session 5PEPM at Sala X
Chair(s): Alberto Pettorossi University of Rome Tor Vergata, Italy
14:00
30m
Talk
Extracting a Call-by-Name Partial Evaluator from a Proof of Termination
PEPM
Kenichi Asai Ochanomizu University
DOI File Attached
14:30
30m
Talk
Futures and Promises in Haskell and Scala
PEPM
Tamino Dauth Karlsruhe University of Applied Sciences, Germany, Martin Sulzmann Karlsruhe University of Applied Sciences, Germany
DOI File Attached
15:00
28m
Talk
Generating Mutually Recursive Definitions
PEPM
Jeremy Yallop University of Cambridge, UK, Oleg Kiselyov
DOI Pre-print
15:28
2m
Poster
Advanced Futures and Promises in C++ (poster)
PEPM
Tamino Dauth Karlsruhe University of Applied Sciences, Germany, Martin Sulzmann Karlsruhe University of Applied Sciences, Germany