LAMA- Equipe de Logique

Abstract. 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...

Full description

Bibliographic Details
Main Authors: Samir Farkh, Karim Nour, Université De Savoie
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published:
Subjects:
sami
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.250.8508
http://arxiv.org/pdf/0905.0575v1.pdf
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.250.8508
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.250.8508 2023-05-15T18:11:12+02:00 LAMA- Equipe de Logique Samir Farkh Karim Nour Université De Savoie The Pennsylvania State University CiteSeerX Archives 905 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.250.8508 http://arxiv.org/pdf/0905.0575v1.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.250.8508 http://arxiv.org/pdf/0905.0575v1.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://arxiv.org/pdf/0905.0575v1.pdf text ftciteseerx 2016-01-07T19:44:30Z Abstract. 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. Résumé. J.-L. Krivine a introduit le système de typage AF2 pour obtenir des programmes (λtermes) calculant des fonctions en écrivant des démonstrations de leur totalité. Nous présentons dans ce papier des résultats de complétude pour certains types de AF2 et pour plusieurs notions de réductions. Ces résultats généralisent un théorème de R. Labib-Sami établi dans le système F de J.-Y. Girard. Text sami Unknown
institution Open Polar
collection Unknown
op_collection_id ftciteseerx
language English
description Abstract. 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. Résumé. J.-L. Krivine a introduit le système de typage AF2 pour obtenir des programmes (λtermes) calculant des fonctions en écrivant des démonstrations de leur totalité. Nous présentons dans ce papier des résultats de complétude pour certains types de AF2 et pour plusieurs notions de réductions. Ces résultats généralisent un théorème de R. Labib-Sami établi dans le système F de J.-Y. Girard.
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Samir Farkh
Karim Nour
Université De Savoie
spellingShingle Samir Farkh
Karim Nour
Université De Savoie
LAMA- Equipe de Logique
author_facet Samir Farkh
Karim Nour
Université De Savoie
author_sort Samir Farkh
title LAMA- Equipe de Logique
title_short LAMA- Equipe de Logique
title_full LAMA- Equipe de Logique
title_fullStr LAMA- Equipe de Logique
title_full_unstemmed LAMA- Equipe de Logique
title_sort lama- equipe de logique
publishDate
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.250.8508
http://arxiv.org/pdf/0905.0575v1.pdf
genre sami
genre_facet sami
op_source http://arxiv.org/pdf/0905.0575v1.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.250.8508
http://arxiv.org/pdf/0905.0575v1.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766183892258127872

Similar Items