2-or-more approximation for intuitionistic logic

Gabriel Scherer (1)

1 GALLIUM - Programming languages, types, compilation and proofs

In the context of the simply-typed lambda-calculus (propositionalintuitionistic logic) with products and sums, we will answer the followingquestion. Given a fixed logic proof and typing environment, the number of possible programs that correspond to this proof depends on the number of free variables of each type in the type environment. If we are not interested in the precise number of programs but only "zero, one, or two-or-more", is it correct to approximate the number of variables at each type by "zero, one, or two-or-more"?

Domaines: Langage de programmation [cs.PL]

Gabriel Scherer. 2-or-more approximation for intuitionistic logic. 2014. ⟨hal-01094120⟩