R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2

J.-L. Krivine introduced the AF2 type system in order to obtain programs ($\lambda$-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...

Full description

Bibliographic Details
Main Authors: Farkh, Samir, Nour, Karim
Format: Text
Language:unknown
Published: 2009
Subjects:
Mathematics - Logic
Eme
Lambda
sami
Online Access:http://arxiv.org/abs/0905.0575
id ftarxivpreprints:oai:arXiv.org:0905.0575
record_format openpolar
spelling ftarxivpreprints:oai:arXiv.org:0905.0575 2023-09-05T13:22:54+02:00 R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2 Farkh, Samir Nour, Karim 2009-05-05 http://arxiv.org/abs/0905.0575 unknown http://arxiv.org/abs/0905.0575 Informatique Th\'eorique et Applications 31, 6 (1998) 513-537 Mathematics - Logic text 2009 ftarxivpreprints 2023-08-16T12:00:22Z J.-L. Krivine introduced the AF2 type system in order to obtain programs ($\lambda$-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 ArXiv.org (Cornell University Library) Eme ENVELOPE(-58.667,-58.667,-62.250,-62.250) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300)
institution Open Polar
collection ArXiv.org (Cornell University Library)
op_collection_id ftarxivpreprints
language unknown
topic Mathematics - Logic
spellingShingle Mathematics - Logic
Farkh, Samir
Nour, Karim
R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2
topic_facet Mathematics - Logic
description J.-L. Krivine introduced the AF2 type system in order to obtain programs ($\lambda$-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\'esultats de compl\'etude pour des classes de types du syst\`eme AF2
title_short R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2
title_full R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2
title_fullStr R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2
title_full_unstemmed R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2
title_sort r\'esultats de compl\'etude pour des classes de types du syst\`eme af2
publishDate 2009
url http://arxiv.org/abs/0905.0575
long_lat ENVELOPE(-58.667,-58.667,-62.250,-62.250)
ENVELOPE(-62.983,-62.983,-64.300,-64.300)
geographic Eme
Lambda
geographic_facet Eme
Lambda
genre sami
genre_facet sami
op_relation http://arxiv.org/abs/0905.0575
Informatique Th\'eorique et Applications 31, 6 (1998) 513-537
_version_ 1776203474032132096

Similar Items