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"?
Type de document :
Pré-publication, Document de travail
2014
Liste complète des métadonnées

https://hal.inria.fr/hal-01094120
Contributeur : Scherer Gabriel <>
Soumis le : jeudi 11 décembre 2014 - 16:34:09
Dernière modification le : mercredi 14 décembre 2016 - 01:07:26
Document(s) archivé(s) le : samedi 15 avril 2017 - 07:50:15

Fichier

2-or-more-approximation.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01094120, version 1

Collections

Citation

Gabriel Scherer. 2-or-more approximation for intuitionistic logic. 2014. <hal-01094120>

Partager

Métriques

Consultations de
la notice

116

Téléchargements du document

43