Merci pour tes slides, dont j'aime bien le ton et le contenu! Tout naïf que je suis je n'avais pas fait explicitement le rapprochement entre l'isomorphisme de Curry-Howard et la logique intuitionniste. :) Je vais donc t'obliger à faire le SAV. :D
La façon de comprendre la traduction entre de "truth" et "falsity" en termes de CS "type singleton" et "type vide" est que "A implique B est vraie" et "il existe une et une seule fonction de A vers B", correct?
Est-ce qu'il n'y a pas un poly que tu pourrais me recommander. Je suis mathématicien mais je ne suis pas très familier avec le domaine de la logique proprement dite ou la théorie des types, donc je pense que je pourrais arriver à profiter un peu d'un cours de DEA ou de Master.
[^] # Re: Le web
Posté par Michaël (site web personnel) . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 2.
Merci pour tes slides, dont j'aime bien le ton et le contenu! Tout naïf que je suis je n'avais pas fait explicitement le rapprochement entre l'isomorphisme de Curry-Howard et la logique intuitionniste. :) Je vais donc t'obliger à faire le SAV. :D
La façon de comprendre la traduction entre de "truth" et "falsity" en termes de CS "type singleton" et "type vide" est que "A implique B est vraie" et "il existe une et une seule fonction de A vers B", correct?
Est-ce qu'il n'y a pas un poly que tu pourrais me recommander. Je suis mathématicien mais je ne suis pas très familier avec le domaine de la logique proprement dite ou la théorie des types, donc je pense que je pourrais arriver à profiter un peu d'un cours de DEA ou de Master.