Proofs and algorithms seminar: Jui-Hsuan Wu (Ray) on Monday 27 June 2022 at 14h00

===== Seminar of the proofs and algorithms pole =====

Hello everybody,

For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Jui-Hsuan Wu (Ray) (LIX), invited by the PARTOUT team.

***** Monday 27 June 2022 at 14h00, https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVpUVkxSZz09 *****

Jui-Hsuan Wu (Ray) -- A positive perspective on term representation

The structure of terms and expressions are represented variously via, say, labeled trees or directed acyclic graphs (DAGs). When such expressions contain bindings, additional devices are needed. In this talk, I will present the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative bias, LJF proofs encode term structures as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive bias, LJF proofs yield a structure in which explicit sharing of term structures is possible. In this situation, cut elimination yields a different notion of substitution. To illustrate these two approaches to term representation, I will give an example by applying them to the encoding of untyped λ-terms.




The list of next seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics