My name is Aaron Hsu, and I'm a computer scientist. I'm changing the way people look at computing and programming languages, what they can do with them, and how they do it.
Lately I have been working on formalizing APL. One of the core problems related to the formalization of APL is how indexing into various arrays that have been derived from other arrays works. In particular, one of the more interesting aspects is the relation between what is known as an
Handwritten versions: Pg. 1, Pg. 2, Pg. 3. Lately I have been playing with the Isabelle proof assistant, and I really like what I have been seeing. Isabelle has a lot of automation, and that is sort of one of my basic prerequisites when investigating proof systems. Isabelle has impressed