2-or-more approximation for intuitionistic logic

Abstract : 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"?
Document type :
Preprints, Working Papers, ...
Liste complète des métadonnées

https://hal.inria.fr/hal-01094120
Contributor : Scherer Gabriel <>
Submitted on : Thursday, December 11, 2014 - 4:34:09 PM
Last modification on : Tuesday, November 20, 2018 - 11:06:03 PM
Document(s) archivé(s) le : Saturday, April 15, 2017 - 7:50:15 AM

File

2-or-more-approximation.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01094120, version 1

Collections

Citation

Gabriel Scherer. 2-or-more approximation for intuitionistic logic. 2014. 〈hal-01094120〉

Share

Metrics

Record views

138

Files downloads

54