Rencontre,
May 5, 2022

## Nathanaëlle Courant (INRIA), Testing convertibility in parallel

### Schedule

- May 5, 2022, 14:00 - 15:00

### Abstract

In this talk, I will present a machine for testing the convertibility of
lambda-terms. This machine is based on implementations of strong
call-by-need evaluation, and is able to exploit that convertibility is
closed by context: to prove that `f x`

is convertible with `f y`

when
`f`

is a constant, it it enough to prove that `x`

and `y`

are
convertible. However, it is sometimes more efficient to unfold `f`

to
prove convertibility, for instance if it does not use its argument. Our
machine solves both convertibility problems in parallel while sharing
computations, and stops as soon as it is able to conclude about the
initial problem.