COPLAS talk: Dmitriy Traytel: Binding-aware datatypes and inductive predicates in Isabelle/HOL
Speaker
Dmitriy is associate professor at DIKU on the UCPH promotion program. He has co-authored a number of papers that have received best paper awards (including this one at POPL 2025). For more information see https://traytel.bitbucket.io.
Title
Binding-aware datatypes and inductive predicates in Isabelle/HOL
Abstract
This talk will describe ongoing work aiming to provide flexible definitional and reasoning infrastructure for syntax with bindings in the Isabelle/HOL proof assistant. I will first survey already existing nameless (via de Bruijn indices) and nameful (Nominal and Nominal2) approaches. Our approach belongs to the nameful family and generalizes prior work by replacing syntactic formats with general semantic conditions and by accommodating infinitary syntax. I will demonstrate the advantages of these generalizations for typical examples such as the lambda calculus and the pi calculus as well as for the more exotic infinitary affine lambda calculus by Mazza. The presentation will be demonstration-driven and will showcase the infrastructure and automation we provide in Isabelle. For a description of this work’s theoretical foundations I refer to our POPL’19 and POPL’25 papers.
This is joint work with Jan van Brügge and Andrei Popescu, with prior contributions by Jasmin Blanchette, Lorenzo Gheri, James McKinna, Matthias Roshardt, and Pascal Stoop.
Host
Fritz Henglein (DIKU)
All are welcome. No registration required. Feel free to forward this invitation.
The Copenhagen Programming Languages Seminar (COPLAS) is a collaboration between DTU, ITU, Roskilde University and UCPH. To be informed about COPLAS activities and related talks, join this mailing list.