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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

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