I have not posted in a while – no one told me this professor gig was so busy – and so I figured I would start with an easy post. Last week I attended Trends in Functional Programming 2016 which was held at the University of Maryland in College Park just outside of Washington DC.
I did not give a talk, but could not pass the opportunity up to attend. First, the trip was dirt cheap. I think the entire trip ran me about $1200 which is crazy cheap. The registration for the conference was only $100; which included coffee, tea, and snacks during breaks, lunch everyday, a trip to DC which included several museums, and finally, a fancy dinner at a fancy restaurant. Furthermore, it was not very far to travel. Check out the website for more on the venue.
Secondly, a former student of mine, Chad Reynolds, who while a student at Augusta University took my Concepts of Programming Languages course, and as it turns out, loved it. He is now a PhD student at University of Iowa studying under the direction of my PhD advisor Aaron Stump. Chad gave his first conference talk at TFP, and I am really happy I got to go and see it. Below are a few pictures I took of him in action.His talk went very well, and the research seemed to be well received by who was there. For more information about his work check out their paper.
The most enjoyable part of the conference for me was the social interaction. There were a few people I got to see that I have not seen in a while, and there were a few people I have talked to over the Internet, but have never met in person that I finally got to meet. In addition, I made a few new connections as well.
On Tuesday there was a one day workshop called Trends in Functional Programming in Education which was interesting and fun. The talks were great, and there was a lot of very interesting discussion.The picture on the right was 3D printed, and was designed by a functional DSL called Bricklayer. It has been used to teach functional programming to K-12 students. Bricklayer supports building 3D printed objects, and the ability to build complex objects in Minecraft! I did not even know you could compile to Minecraft.
One thing I learned about Clojure is that it is interpreted into Java, and so very simple type errors result in very complex error messages which makes it hard to use Clojure for teaching. Luckily, Elena Machkasova and her students are fixing that problem. Check out the picture to the left – by clicking it to enlarge it – of an error message in Clojure which results from trying to add the number one with a string.The complete error message is about thirty lines long. To make matters worse the error message talks about internal Java libraries and types, and is not specific to Clojure. This is a complete design malfunction. We can do better!
There were two invited talks for TFP. The first by Ronald Garcia who gave an exquisite introduction to to gradual type systems – which combine static and dynamic typing – and using them for enforcement of secure information flow.
This talk really got me thinking. I have been somewhat interested in secure information flow, but have not gotten around to reading about it. Ron explained that in these type systems one labels types with security levels that could be used to prevent higher secure computation from interacting in an inappropriate way with lower security computation. For example, \( T_L T_H \) would be the type of a function that takes in lower security data and produces high security data. Now most likely we would not want \(T_H T_L\), because this could leak higher secure information.
The idea I had was that if we could form a categorical model for these type systems, then we could use it to gain a higher level analysis by abstracting away the syntax into a theory consisting of only types, security levels, and how these interact (the arrows). I am hoping to think more about this, but there is one big open question, what is the categorical model of gradual typing? I think I have an idea, but will need to think more about it.
The second invited talk was by Steve Zdancewic on his recent project called ExCape. One of the fruits of this project is a tool for type-directed program synthesis. The programmer provides a type, and a few test cases of how the program should operate, and then the tool finds a program with the corresponding type that runs appropriately on the given test cases. Now if not enough test cases are given, then one might obtain the wrong program. So the synthesized program may need to be further verified for correctness.
One example Steve gave was a synthesized version of the free variable function for the \(\)-calculus. You can see it in the below image on the right.
One application Steve gave for this was that it could be used to synthesize student feedback when grading programming assignments. This could work out pretty well, because students may give partial answers, or incorrect answers, and the tool could synthesize the part of the student solution that is missing or incorrect.
The trip to DC was also very exciting for me personally, because I had never been before. Chad and I decided to do a bunch of site seeing and went to the Lincoln Memorial and the National Mall. Brent Yorgey, Chad, and I also went over to The White House which was a lot of fun. Here are a bunch of pictures from DC:The statue is a 3D printed version of a famous one that I forgot the name of now. The original is most likely to fragile to have out for the public and so it was replicated. The image just after the one of The White House consists of these terrain looking formations that are completely made out of index cards. They were amazing! The stick huts actually had doors and people were allowed to go into them. All of these pictures were taken of art in the famous Renwick Gallery.
Visiting DC was not the only first I got to mark off the bucket list. I also rode in my first Uber.
The experience was great, and I was surprised at how fast and easy it was. I am now an Uber fan. Finally, I got to also ride in a propeller plane for the first time. It was awesome!
TFP and TFPiE was a great experience, and I highly recommend it! Consider going next year. For now though, you can find links to all the accepted papers, and slides for the invited talks over here.