For a new seminar on the proofs and algorithms pole of LIX, we are happy to welcome Jui-Hsuan Wu (one of our own Ph.D. students at LIX), invited by the PARTOUT team.

Note that this talk is the last one in PARTOUT before the summer holidays. We will resume our seminar in September.

Abstract: 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.

Join Zoom Meeting

• URL: https://us02web.zoom.us/j/89155612228?pwd=aU5RYXAvYXpvbmFROG44OVpUVkxSZz09
• Meeting ID: 891 5561 2228
• Passcode: ZLEY8Z

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