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

pepm-2019-papers
14:00 - 15:30: PEPM 2019 - Session 5 at Sala X
Chair(s): Alberto PettorossiUniversity of Rome Tor Vergata, Italy
pepm-2019-papers14:00 - 14:30
Talk
Kenichi AsaiOchanomizu University
DOI File Attached
pepm-2019-papers14:30 - 15:00
Talk
Tamino DauthKarlsruhe University of Applied Sciences, Germany, Martin SulzmannKarlsruhe University of Applied Sciences, Germany
DOI File Attached
pepm-2019-papers15:00 - 15:28
Talk
Jeremy YallopUniversity of Cambridge, UK, Oleg Kiselyov
DOI Pre-print
pepm-2019-papers15:28 - 15:30
Poster
Tamino DauthKarlsruhe University of Applied Sciences, Germany, Martin SulzmannKarlsruhe University of Applied Sciences, Germany