Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application
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...
Main Authors: | , , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
1998
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.366.9790 http://hal.archives-ouvertes.fr/docs/00/38/11/55/PDF/THESE.pdf |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.366.9790 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.366.9790 2023-05-15T18:11:14+02:00 Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application Samir Farkh Karim Nour Lama Equipe De Logique Université De Savoie The Pennsylvania State University CiteSeerX Archives 1998 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.366.9790 http://hal.archives-ouvertes.fr/docs/00/38/11/55/PDF/THESE.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.366.9790 http://hal.archives-ouvertes.fr/docs/00/38/11/55/PDF/THESE.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://hal.archives-ouvertes.fr/docs/00/38/11/55/PDF/THESE.pdf text 1998 ftciteseerx 2016-01-08T01:05:42Z 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 Lama Equipe De Logique Université De Savoie |
spellingShingle |
Samir Farkh Karim Nour Lama Equipe De Logique Université De Savoie Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application |
author_facet |
Samir Farkh Karim Nour Lama Equipe De Logique Université De Savoie |
author_sort |
Samir Farkh |
title |
Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application |
title_short |
Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application |
title_full |
Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application |
title_fullStr |
Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application |
title_full_unstemmed |
Résultats de complétude pour des classes de types du système AF2”, Informatique Théorique et Application |
title_sort |
résultats de complétude pour des classes de types du système af2”, informatique théorique et application |
publishDate |
1998 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.366.9790 http://hal.archives-ouvertes.fr/docs/00/38/11/55/PDF/THESE.pdf |
genre |
sami |
genre_facet |
sami |
op_source |
http://hal.archives-ouvertes.fr/docs/00/38/11/55/PDF/THESE.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.366.9790 http://hal.archives-ouvertes.fr/docs/00/38/11/55/PDF/THESE.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766183923847528448 |