Quelques correspondances entre systèmes fonctionnels et systèmes formels; Correspondance de Curry-Howard ou preuve/programme

Ref: http://fr.wikipedia.org/wiki/Correspondance_de_Curry-Howard

La correspondance de Curry-Howard a établi un pont entre théorie de la démonstration et informatique théorique.
Le logicien français, Jean-Louis Krivine a fait le rapport entre différents théorèmes mathématiques et les programmes informatiques qu'ils représentent [Jean-Louis Krivine, Une preuve formelle et intuitionniste du théorème de complétude de la logique classique, Bull. Symb. Log. 2, 4, p. 405-421 (1996)]:

•     l'absurde (appelé « bottom » : \perp) correspond à une instruction d'échappement, d'exception, ou à un programme qui ne finit pas (un terme non-typable dans le lambda-calcul simplement typé).
•     le théorème d'incomplétude de Gödel qui dit qu'il y a des théorèmes que l'on ne peut pas démontrer correspond à un programme de réparation de fichiers.[réf. souhaitée]
•     le théorème de complétude de Gödel correspond lui à un désassembleur interactif de programmes

Quelques correspondances entre systèmes fonctionnels et systèmes formels

Système fonctionnel	Système formel
Calcul des constructions (Thierry Coquand)	?
Système F (Jean-Yves Girard)	Arithmétique de Peano du second ordre / Logique intuitionniste du second ordre
Système T (Kurt Gödel)	Arithmétique de Peano du premier ordre / Logique intuitionniste du premier ordre
Système T1	?
T0 (Récursion primitive) (Stephen Cole Kleene ? Thoralf Skolem ?)	Arithmétique primitive récursive
Lambda-calcul simplement typé	Calcul propositionnel minimal implicatif (déduction naturelle)
Logique combinatoire	Calcul propositionnel minimal implicatif (à la Hilbert)
Calcul lambda-µ de Parigot	Déduction naturelle en calcul propositionnel classique
Calcul lambda-µ-µ~ de Curien et Herbelin	Calcul des séquents classique
Calcul symétrique de Berardi et calcul dual de Wadler	Calcul des séquents avec et

pdf ou html full texte et référence dans Zotero.

Actuellement pour sauvegarder mes pdf, et mes pages html d'articles ou de brevets et aussi mes sites utiles, j'utilise le célèbre open source zotero.

Il existe deux grands soucis avec zotero malgré sa puissance.
1)Il est assez énervant de jonglet avec les serveurs mandataires dans zotero. Une université et un organisme type CNRS paient très cher l'accès à des bouquets permettant la lecture et la sauvegarde d'un "full" texte d'un article scientifique (il faut toujours sauvegarder ses pdf car ces organismes ne paient que l'accès sur une durée de 1an). Il existe deux types d'accès :

• soit par n° IP (faire attention au proxy) ou 
• soit avec un mot de passe.

Zotero a tendance à passer en direct sans les serveurs mandataires...

2)Lien pdf (ou full html) avec la référence. Lorsque le pdf n'a pas de metadonnées ou si elles sont incorrectes (assez souvent!) alors il faut aussi mettre la référence et le lien entre le pdf et sa référence correcete dans la même collection dans son zotero. C'est coûteux en temps...
La solution que je propose est de bien gérer le corpus d'accès aux ref (et abstract) et de sauver la ref dans zotero (via les catalogues) puis de basculer vers le site d'accès pdf ou html complet en sachant que les éditeurs "oublient" souvent de mettre les métadonnées.
Le corpus de ce type de one-click service est : http://www.zotero.org/translators/

Web of science (WoS), la plus grande banque d'articles scientifique, ne fonctionne pas bien avec zotero (WoS est aussi l'éditeur de endnote qui contrairement à Zotero est payant).
Voir: http://ex-ample.blogspot.com/2011/12/solution-of-error-could-not-save-item.html

Ce corpus de sites "zotero compatibles" contient 7types où les références (attention à vérifier la qualité et le nombre de champs) sont accessibles en one-click import dans zotero (dans l'omnibarre):

1. des libraires style Amazon
2. des moteurs de recherche (google scholar, google books, scirius)
3. des catalogues de bibliothèques comme sudoc (ou de votre université) ou comme worldcat, ou catalogue d'organisme comme medline (les références y sont souvent très bien cataloguées avec les champs complets et corrects)
4. des logiciels de gestion biblio en ligne comme citeUlike,
5. des archives ouvertes comme hal, arXiv, citeSeer...
6. les ressources à abonnement où on peut récupérer le(s) pdf: WoS, Sciencedirect, springerLink, wiley, IEEExplore, spie, (en eco factiva)
7. les ressources open access comme l'éditeur PLoS, biomed... ou des sites comme revues.org avec URL pérenne (ou equivalente à un DOI) ou encore le célèbre wikipedia (vérfier la qualité des références absoluement).

 -----

----------------
Merci à Dominique du SCD Sciences de l'Université St-Etienne