‹Programming› 2019
Mon 1 - Thu 4 April 2019 Genoa, Italy
Tue 2 Apr 2019 09:00 - 10:30 at Colombo - Opening Talk

Almost every programming language’s syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of alpha-equivalence, capture avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope safe operation (e.g., renaming, substitution, desugaring, printing, etc.), and then again for correctness proofs. We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving.

Tue 2 Apr

cocodo-2019
09:00 - 10:30: CoCoDo 2019 - Opening Talk at Colombo
cocodo-201909:00 - 10:30
Talk
Guillaume AllaisUniversity of Strathclyde