[Colloq] Thesis Presentation - Fabian Muehlboeck - Checking Binding Hygiene Statically - Friday, April 19th, 3pm, 166 WVH
Jessica Biron
bironje at ccs.neu.edu
Wed Apr 17 14:40:11 EDT 2013
Checking Binding Hygiene Statically (With few annotations and meaningful explanations for errors)
Fabian Muehlboeck
Friday, April 19th
3pm 166 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.
Jessica Biron
Administrative Assistant – Office of the Dean and CCIS Development
College of Computer and Information Science
Northeastern University
202 West Village H
617-373-5204
bironje at ccis.neu.edu
http://www.ccs.neu.edu/
More information about the Colloq
mailing list