Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Constructive natural deduction and its "omega-set" interpretation

Abstract : Various Theories of Types are introduced, by stressing the analogy ‘propositions-as-types’: from propositional to higher order types (and Logic). In accordance with this, proofs are described as terms of various calculi, in particular of polymorphic (second order) λ-calculus. A semantic explanation is then given by interpreting individual types and the collection of all types in two simple categories built out of the natural numbers (the modest sets and the universe of ω-sets). The first part of this paper (syntax) may be viewed as a short tutorial with a constructive understanding of the deduction theorem and some work on the expressive power of first and second order quantification. Also in the second part (semantics, §§6–7) the presentation is meant to be elementary, even though we introduce some new facts on types as quotient sets in order to interpret ‘explicit polymorphism’. (The experienced reader in Type Theory may directly go, at first reading, to §§6–8).
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal-ens.archives-ouvertes.fr/hal-03316282
Contributeur : Usr 3608 République Des Savoirs <>
Soumis le : jeudi 12 août 2021 - 10:55:18
Dernière modification le : vendredi 13 août 2021 - 03:19:35

Fichier

2021_08_12_LongoMoggi-construc...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Giuseppe Longo, Eugenio Moggi. Constructive natural deduction and its "omega-set" interpretation. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 1991, 1 (2), pp.215-253. ⟨10.1017/S0960129500001298⟩. ⟨hal-03316282⟩

Partager

Métriques

Consultations de la notice

34

Téléchargements de fichiers

16