Sampling β-normal linear λ-terms

Abstract Leveraging our recent work on the enumeration of β-redices in closed linear λ-terms, we present an algorithm for sampling β-normal closed linear λ-terms and their corresponding maps. Such terms correspond to proofs of tautologies in implicational linear logic and their generation is of interest in various domains, including the testing of linear logic theorem provers.