For the next seminar of the proofs and algorithms pole of LIX, we are happy to welcome Ambroise Lafont (UNSW Sydney), who will be visiting the Partout team for the day. Note this will be a hybrid seminar, simultaneously taking place at Salle Marcel-Paul Schützenberger and on BBB.

Abstract: By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.

Joint work with Tom & Andre Hirschowitz, Marco Maggesi

The list of next seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/calendar.ics