I share with Pierre Dagand the pleasure of having finished the redaction of a small article on realizability for JFLA 15 (Journées francophones des langages applicatifs). It is a rather simple presentation of the computational content of adequacy proofs, which we hoped to understand better by exhibiting their proof terms as well-typed lambda-terms in a dependently typed meta-language.

http://gallium.inria.fr/~scherer/research/norm_by_rea/dagand-scherer-jfla15.pdf

A frustrating aspect of the paper is that it has much less than what we originally hoped to discuss. We initially looked at realizability proofs for System L-style sequent calculi, and I conceived the lambda-calculus adequacy as merely an introduction. The introduction filled the 15 pages limit and it became the whole thing. Excluded from this work yet very much desirable are;

  • an extension to second-order quantification (impredicative polymorphism)
  • an extension to classical calculus through an explicit call/cc primitive
  • an extension to strong normalization rather than weak normalization
  • an adaptation to typed polarized System L as presented in Guillaume Munch-Maccagnoni’s work

The reason I started looking at this is that I wanted to understand better the way logical relations “work” surprisingly well to build strong meta-theoretical results. This probably first requires understanding better the links between this explicit computational content and the idealized presentation of orthogonality in Bernardy and Lasson’ “Realizability and Parametrcity in Pure Type Systems”.

The reviews we got from the JFLA reviewers were extremely, surprisingly helpful (I suppose reviewers at larger conferences have on average more papers to review). As we expected and hoped, they unearthed references to Related Work that we were not aware of, and this submission was very efficient at forcing us to explore the whole area more in depth.

Pierre had the courage to do mechanized formalizations of this work, in both Agda and Coq, which turned out reasonably well, although it only covers the first part of the paper – this is not our main gig. We are quite lucky he did that effort upfront, because it is increasingly hard to escape the peer pressure to proof-assist these days; our submitted version didn’t come with the formalization (we felt it was too rough to be useful), and the reviewers demanded too see it. A very natural request for an article about writing a dependently-typed programs, and – of course – the process of cleaning it up made Pierre notice a handful of typing mistakes I made when LaTeXing the proof terms. Not yet ready to defend.

http://gallium.inria.fr/~scherer/research/norm_by_rea/html/Norm.html

.

Post Scriptum: François also has a JFLA paper!

Depth-first search and strong connectivity in Coq
François Pottier

Using Coq, we mechanize Wegener’s proof of Kosaraju’s linear-time algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depth-first search algorithm.

[..]

As should be clear from this three-line description, Kosaraju’s algorithm is significantly simpler than Tarjan’s. Although the textbook proofs of this algorithm are still somewhat complex, Wegener [8] presents a beautiful reconstruction of the algorithm, which can be considered an explanation and a proof (albeit an informal one). [..]

One attractive feature of this proof is that, in contrast with Cormen et al.’s [2], it never mentions the “times” at which vertices are visited. Instead, it is expressed purely in terms of graphs, forests, and their structural properties. This gives it a more “declarative”, as opposed to “imperative”, flavor. [..]

In the paper, we elide the details of our machine-checked version of Wegener’s proof. We give only an outline of the proof, insofar as a (formalist!) teacher might explain it. We explicitly state several definitions and lemmas, but omit or inline a number of “trivial” auxiliary lemmas. We accompany each lemma with a hand-written proof, formulated in a clear but informal style, and collect these proofs in an appendix