Résultats de complétude pour des classes de types du système AF2

J.-L. Krivine introduced the AF2 type system in order to obtain programs ($λ$-terms) which calculate functions, by writing demonstrations of their totalities. We present in this paper two results of completness for some types of AF2 and for many notions of reductions. These results generalize a theo...

Full description

Bibliographic Details
Main Authors: Farkh, Samir, Nour, Karim
Format: Text
Language:unknown
Published: arXiv 2009
Subjects:
Logic math.LO
FOS Mathematics
sami
Online Access:https://dx.doi.org/10.48550/arxiv.0905.0575
https://arxiv.org/abs/0905.0575
id ftdatacite:10.48550/arxiv.0905.0575
record_format openpolar
spelling ftdatacite:10.48550/arxiv.0905.0575 2023-05-15T18:11:26+02:00 Résultats de complétude pour des classes de types du système AF2 Farkh, Samir Nour, Karim 2009 https://dx.doi.org/10.48550/arxiv.0905.0575 https://arxiv.org/abs/0905.0575 unknown arXiv arXiv.org perpetual, non-exclusive license http://arxiv.org/licenses/nonexclusive-distrib/1.0/ Logic math.LO FOS Mathematics article-journal Article ScholarlyArticle Text 2009 ftdatacite https://doi.org/10.48550/arxiv.0905.0575 2022-04-01T15:02:10Z J.-L. Krivine introduced the AF2 type system in order to obtain programs ($λ$-terms) which calculate functions, by writing demonstrations of their totalities. We present in this paper two results of completness for some types of AF2 and for many notions of reductions. These results generalize a theorem of R. Labib-Sami established in the system F of J.-Y. Girard. Text sami DataCite Metadata Store (German National Library of Science and Technology)
institution Open Polar
collection DataCite Metadata Store (German National Library of Science and Technology)
op_collection_id ftdatacite
language unknown
topic Logic math.LO
FOS Mathematics
spellingShingle Logic math.LO
FOS Mathematics
Farkh, Samir
Nour, Karim
Résultats de complétude pour des classes de types du système AF2
topic_facet Logic math.LO
FOS Mathematics
description J.-L. Krivine introduced the AF2 type system in order to obtain programs ($λ$-terms) which calculate functions, by writing demonstrations of their totalities. We present in this paper two results of completness for some types of AF2 and for many notions of reductions. These results generalize a theorem of R. Labib-Sami established in the system F of J.-Y. Girard.
format Text
author Farkh, Samir
Nour, Karim
author_facet Farkh, Samir
Nour, Karim
author_sort Farkh, Samir
title Résultats de complétude pour des classes de types du système AF2
title_short Résultats de complétude pour des classes de types du système AF2
title_full Résultats de complétude pour des classes de types du système AF2
title_fullStr Résultats de complétude pour des classes de types du système AF2
title_full_unstemmed Résultats de complétude pour des classes de types du système AF2
title_sort résultats de complétude pour des classes de types du système af2
publisher arXiv
publishDate 2009
url https://dx.doi.org/10.48550/arxiv.0905.0575
https://arxiv.org/abs/0905.0575
genre sami
genre_facet sami
op_rights arXiv.org perpetual, non-exclusive license
http://arxiv.org/licenses/nonexclusive-distrib/1.0/
op_doi https://doi.org/10.48550/arxiv.0905.0575
_version_ 1766184099751395328

Similar Items