programming language designers

Abstract: We present a new proof of weak normalization for intuitionistic natural deduction. The distinguishing features of this proof are that it works only with cuts rather than cut segments, provides explicit local rules for determining whether to contract a whole proof or reduce one of its subproofs, and in the latter case, which subproof to reduce. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.

Abstract: We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.

Abstract: Emil Post's productive sets are not even semi-computable, let alone computable, being thus essentially incomputable. Accordingly, formal languages whose set of words is a (completely) productive set are essentially undecidable. In this article, I elaborate on Post productivity from the viewpoint of formal language theory: I design formal grammars that emulate the construction of productive sets of natural numbers and are thus beyond Turing-decidability.

Abstract: Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel's system T to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.

Abstract: This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a program will not get stuck. Previous work has provided such guarantees for consistent erased postulates, i.e. postulates that are restricted to be used in erased contexts. Here those guarantees are extended to type theory with identity types. Similar ideas provide a simple way to support quotient types: it is shown that one can let things like "the equivalence classes for two related values are equal" be erased postulates and have an eliminator that only computes for the equivalence class constructor, and still get a guarantee that programs will compute correctly. Another question is whether programs compute correctly if one is allowed to transport (cast) using erased identity proofs. It is shown that this is safe in the absence of quotients and postulates, and in the presence of quotients and erased postulates that can be implemented using equality reflection. However, unrestricted transports of this kind are not compatible with erased, postulated univalence. For that reason the text includes a study of the function []-cong, which encapsulates a limited form of transport for erased identity proofs. The text is accompanied by machine-checked Agda proofs.