Pure Type Systems with Definitions

I reread “Pure Type Systems with Definitions” (Severi and Poll, 1994) and had a Skype meeting about it. It was a real pleasure rereading the paper. The paper is surprisingly beginner friendly. I’d expect most people with a CS 245E and CS 444 background to be able to enjoy the paper.

The discussion was also helpful. It was nice to learn that I’m not the only one unhappy about their gaps in knowledge in the more Curry-Howard parts of PL. One of the things that came up in our discussion, although I hadn’t really given it too much thought earlier, is that the completion defined in the paper is exactly what we would expect our systems to have. On the other hand, it wasn’t clear to me that we really needed completion in its entirety to prove beta-delta reduction to be strongly normalizing. To me, looking at the examples, it seems like adding a Type₂ to λC might be enough. We discussed that deeply nested let-bindings might cause a problem and that we expect the authors to have at least noted it if smaller extensions were good enough in certain cases. We also noted that the mutual induction in the paper is nice and simple, and necessary because of the way they defined delta-reduction.

Class Hierarchy Analysis and Rapid Type Analysis papers

I read two papers to catch up on CMPUT 500. In the course we are trying to build accurate call graphs, but the papers were written from the perspective of trying to replace or optimize dynamic dispatch in compiled code.

I read “Optimization of Object-Oriented Programs Using Static Class Hierarchy Analysis” (Dean et al, 1995). It seems Class Hierarchy Analysis (CHA) is exactly where you would start for replacing virtual calls with dynamic dispatch or for whole program call-graph construction. But I liked how the authors laid out the theory using cones and difference sets. The paper also discussed implementation is some detail.

Also read “Fast Static Analysis of C++ Virtual Function Calls” (Bacon and Sweeney, 1996). This was a paper on Rapid Type Analysis (RTA). RTA essentially prunes the call graph generated by CHA. RTA conservatively figures out which constructors are called in the program and only adds edges to virtual methods if the constructor is possibly called in the program.

Implementation of Functional Programming Languages Chapter 8

Finished reading “Chapter 8: Polymorphic Type-Checking”. I just expected an algorithm to be directly presented, but much of the chapter focused on different constructs and the types that different constructs have. Already having a lot of background in the area, I found the material to be somewhat dry. A large portion of the chapter discussed detail why arguments of functions are given the same type at each of their occurrences in type system presented.

I was surprised to learn that Miranda did not use traditional Hindley-Milner let polymorphism, and this is one place where the book deviates from Miranda.

Older   Newer