apl Indexing Arrays 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.
formalism Playing with Isar 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,