[Colloq] Thesis Presentation - Fabian Muehlboeck - Checking Binding Hygiene Statically - Thursday, April 25th, 1:30pm, 366 WVH

[Jessica Biron]

Checking Binding Hygiene Statically (With few annotations and meaningful explanations for errors) 

Fabian Muehlboeck 

Thursday, April 25th 
1:30pm 366 WVH 

Abstract: 

Macros are a powerful facility for various applications, from simple syntax extensions to creating domain specific languages. However, they have suffered from the fact that the structure of variable bindings in a program is only implicitly encoded in the program text – which can cause results not intended by either the macro writer or user by violating hygiene. We present the core details of a developing system (by Stansifer and Wand) to statically ensure the preservation of alpha-equivalence and therefore hygiene. Our contribution comes in two parts. The first is that we finished the implementation of the system by creating an interface to an SMT-solver to discharge proof obligations generated by the system. The second part concerns the usability of this system: we implemented a language with ML-like syntax similar to that found in the implantations of related work, and are able to show that the burden on the programmer to write down annotations is comparable to similar systems because many annotations can be inferred. We also show how errors can be explained to the user when proof obligations cannot be discharged.