Please come to Nara park and check it by yourself

Written by Yuki Nishida
Published: 2016-11-02 (last updated: 2016-11-02)

Hello everyone, I'm Yuki Nishida and a PhD student of Atsushi Igarashi at Kyoto University, Japan. I am studying type inference problems for type systems which have refinement types (also known as subset types) and dependent types. It is also related to statically verification for program specifications though I currently focus on the syntactic perspective of those types.

In this conference, I was attending as one of student volunteer (SV) co-chairs. Almost attendees, even other SVs, did not recognize me as one of them because there was a veteran SV co-chair, who worked a lot. So thanks a lot for Gabriel Scherer again here. Anyway, I introduce what SV co-chairs did in this conference for ones who are interested in those. Before beginning the conference, we invited applications of SVs. There was more applications than quota, so we did a selection basically by lottery. After that, we allocated tasks for the selected SVs. Our work was supposed to be almost over at this point since we assigned almost tasks during the conference to SVs. However that was not. The biggest task we did not expected is arrangement of rooms for meetings. It was hard task and I did not expect I tired physically. That said, although there were few small problems, SV tasks almost went well with good volunteers and we were able to finish the conference with no big trouble.

There are many interesting talks during the conference and co-located work shops, but here I introduce a few talks I was especially interested in. Will other posts introduce other talks?

  • Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data by Jesper Cockx, Dominique Devriese and Frank Piessens (doi, draft, talk video) An unification framework from not only the ordinarily syntactic perspective but also the semantic perspective. Therefore, unification introduced in this paper returns not only unifiers but also proofs of equivalences. This paper is very useful for our study because if we construct unification rules, the more rules unification has, the better it can be. This paper will give us some answer for this problem.
  • Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong) by Eric Seidel, Ranjit Jhala and Westley Weimer (doi, arXiv, talk video) Witness generator for ill-typed program. Ill-typed programs will have some input which go program into wrong state. The tool introduced in this paper finds a such input and display an execution sequence how go wrong with the input. The paper also insist that the tool is more useful for debugging than only using ordinarily compiler's type error messages.

Lastly, I mention the conference venue a little. There are a lot of deer around the venue. They are so clever, so they do not touch deer treats stored for them in a park stall, even if there is no keeper. Once someone buys the treats, deer hard chase them and rob them. There must be company. Please come to Nara park and check it by yourself if you have a chance to visit Nara.