D'ailleurs, j'ai l'impression que ta compréhension de ∃x : A. P[x] est aussi un peu biaisée. Un programme de type ∃x : A. P[x] est une paire (t, p) faite d'un programme t : A et d'un programme p : P[t]. C'est la magie de la correspondance de Curry-Howard. Je me permets de mettre un lien vers des slides introductives à moi sur le sujet.
[^] # Re: Le web
Posté par Perthmâd . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 4.
D'ailleurs, j'ai l'impression que ta compréhension de ∃x : A. P[x] est aussi un peu biaisée. Un programme de type ∃x : A. P[x] est une paire (t, p) faite d'un programme t : A et d'un programme p : P[t]. C'est la magie de la correspondance de Curry-Howard. Je me permets de mettre un lien vers des slides introductives à moi sur le sujet.