By Anthony Cantor (University of Iowa PhD student)

Thanks to travel funds generously provided by my advisor, Aaron Stump, as well as the FLOC student travel grant, I was recently fortunate enough to spend a week in Oxford at FLOC 2018. Not only was it an enriching experience, but it was also my first time presenting research. Over the course of the pre-FLOC workshop weekend and the block 1 conferences I saw numerous thought-provoking and enlightening presentations, so I’d like to share some of the highlights here.

Term Assignment for Admissible Rules in Intuitionistic Logic
One of my favorites from my day at the Classical Logic and Computation workshop was Matteo Manighetti’s presentation of an extension of intuitionistic logic that supports admissible intuitionistic rules (with co-author Andrea Condoluci). He explained that if the provability of a formula A implies the provability of a formula B, then the rule A/B is admissible, and if the formula A→B is provable then the rule A/B is derivable. As far as I can tell, these definitions express the difference between meta-theoretic implication and object implication. In classical logic every admissible rule is derivable, but this is not the case in intuitionistic logic: apparently the rule ¬A→(B∨C) / (¬A→B)∨(¬A→C) is admissible but not derivable (this is called “Harrop’s rule”). Manighetti continued by describing an extension of intuitionistic logic obtained by adding axioms corresponding to the admissible rules, and a corresponding Curry-Howard term assignment. I’m really looking forward to reading this paper when it appears in the workshop proceedings because I’m very curious about the details of some of the proofs of theorems that Manighetti claimed during the presentation: one was the disjunction property, and the other he called a “classification” lemma. At the moment I’m quite interested in these sorts of proofs because I’m currently working with Aaron to prove a logical constructiveness result.

Proof Nets and Linear Logic
While at FLOC I attended two great presentations on the subject of proof nets: a presentation on proof nets for bi-intuitionistic linear logic by Willem Heijltjes, and a presentation on a new type of proof nets for multiplicative linear logic by Dominic Hughes. These two presentations caught my interest because of the logic under consideration in the former (bi-intuitionistic logic), and the concept of canonicity in the latter (these two topics relate to research I’ve been working on with Aaron).

Regardless of their potential relevance to my research interests, I’m happy to have attended these presentations because they both had a common property that taught me a lesson about designing slides: when possible, omit words (especially sentences) from a slide. Both of these presentations did a good job of focusing my attention on a particular point of the slide (usually some part of a proof derivation). Throughout the conference I often got lost because I was trying to read sentences on slides instead of focusing on the speaker. By omitting unnecessary words, these presentations kept my eyes on the right part of the slide, and my ears on the speaker. Interestingly, the two presentations differed greatly in terms of the their depth. Heijltjes’ presentation contained a lot details and examples, and Hughes’ stayed extremely high level.

Inspired by Heijltjes and Hughes, I’ve begun exploring linear logic and proof nets via Girard’s “Linear Logic”, a reference cited in both of their papers[1][2]. So far it’s been very rewarding. In particular, I quite liked the following observation made by Girard regarding the connection between the ⊢ relation and constructiveness:

Now, what is the meaning of the separation ⊢? The classical answer is “to separate positive and negative occurrences”. This is factually true but shallow; we shall get a better answer by asking a better question: what in the essence of ⊢ makes the two latter logics more constructive than the classical one? For this the answer is simple: take a proof of the existence or the disjunction property; we use the fact that the last rule used is an introduction, which we cannot do classically because of a possible contraction. Therefore, in the minimal and intuitionistic cases, ⊢ serves to mark a place where contraction (and maybe weakening too) is forbidden; classically speaking, the ⊢ does not have such a meaning, and this is why lazy people very often only keep the right-hand side of classical sequents. Once we have recognized that the constructive features of intuitionistic logic come from the dumping of structural rules on a specific place in the sequents, we are ready to face the consequences of this remark: the limitation should be generalized to the other rooms, i.e., weakening and contraction disappear. As soon as weakening and contraction have been forbidden, we are in linear logic.

Blockchain Verification
Grigore Rosu’s presentation on formally verifying blockchain contracts and virtual machines also stood out. In his talk Rosu advocated the use of a single framework called “K” to generate a suite of language and runtime tools related to a blockchain specification, as opposed to constructing the components first and attempting formal verification as an afterthought. The system uses a logic called “Matching Logic” to generate the components based on configurations containing semantic and syntactic rules. Rosu claimed that many previous methods for defining computational semantics have drawbacks, and that the “K” framework “keeps the advantages of those methods, but without the drawbacks”. Unfortunately he didn’t explain how exactly the “K” framework achieves this, but he did enumerate a rather impressive list of languages that are currently supported by the “K” framework, which included C, Java, and the Ethereum VM. I had a hard time following a lot of the detail about how matching logic enables auto-generation of effective language tools, but I’m at least convinced that it would probably be a lot of fun to try out his framework on a toy language.

Finally, another standout event was most certainly the pair of talks given by Silvio Micali and Henk Barendregt in memory of Corrado Böhm. After relaying some personal memories, Barendregt presented some highlights of Böhm’s career. He first discussed some of Böhm’s early work on self compilation and bootstrapping. In particular, Böhm proved that one could start with a handwritten slow compiler, and then use that compiler to compile itself to obtain faster and faster compilers. Barendregt also touched on a few other important results achieved by Böhm, and ended by discussing Böhm’s passion for research: apparently Böhm was still stating open problems even while in his 90’s. Barendregt’s conclusion was memorable: “keeping asking questions, it keeps you young.”

This past Tuesday (June 19) I gave the second lecture in the series I am working on, about optimal beta-reduction.  The screencast can be found here.  This lecture covers the basic nondeterministic graph reduction rules for lazy duplication.  The notes you will see my writing are here in ora and jpeg formats.  The lambdascope implementation I try using (and many thanks to Jan Rochel for this!) can be found here on hackage.  The lambdascope paper can be found here.

It is a warm start to summer here in Iowa, and among other interesting things to think about, I have been studying the subject of optimal beta-reduction, which has been developed from Jean-Jacques Levy’s dissertation in the 1970s to John Lamping’s 1990 POPL paper, and beyond.  I am using an amazing book by Andrea Asperti and Stefano Guerrini: The Optimal Implementation of Functional Programming Languages.

To help myself learn this, I am giving (and have decided to record) some lectures on the topic.  I am definitely not an expert, only an aspirant!  If you happen to watch these and find errors or confusions, please correct me.  The screencast for the first lecture, covering some main points of Chapter 2 of Asperti and Guerrini, is here.  The notes you will see me writing in the screencast are here, in jpg and ora formats.

I am interested in this because my friend Victor Maia of Ethereum Foundation is considering using a variant of Lamping’s abstract algorithm to run smart contracts in Ethereum, to be written in pure lambda calculus and verified with Cedille (the tool we are working on here now the past few years).

As you may know (for example, from my interview a little while back on the fantastic Type Theory Podcast), we are working here at U. Iowa on a new dependent type theory implementation called Cedille.  It is based on a new extrinsic (aka Curry-style) type theory, and aims to be a very compact theory in which standard parts of dependent type theory like inductive (and hopefully coinductive) datatypes can be defined from the more primitive constructs of the theory.

At our first Cedille meeting of the fall semester — also in attendance Larry Diehl, Richard Blair, Chris Jenkins, Tony Cantor, Colin McDonald, Nadav Kohen — I gave a rather long overview of the current state of Cedille, which I recorded as a screencast and as the notes I was drawing (.ora and .jpg formats) while talking.  While we are (still! [sigh]) not quite ready to make a public release, I think we will get there this fall, as I mention in the screencast.  A few quick highlights are: we have a derivation of induction that is parametrized by a functor (actually, we have two: one for Church encoding and one for Mendler encoding); we can do some surprising and cool things with casts, which are derivable in the theory, including define within Cedille monotone recursive types and get proof reuse between types which can be cast to each other, like lists and vectors; and we just need to complete a (very basic) module system and solve an unpleasant performance issue with our parser, and we should be ready to make a release.

I recently (May 1) gave a short presentation touching on ethics and technology, as well as the ethics of Internet pornography.  I am sharing the slides here.  Sadly, most of the references on the seemingly unending list of harms and evils associated with pornography are behind paywalls, although the article by Max Waltman is freely available.  As always when reading about this topic, please be aware that some of the material can be quite upsetting for people who have experienced sexual assault, abuse, childhood assault, or other traumatic experiences, as well as for young readers.