Forum Programmation.autre Question sur Coq et la tactique induction

Posté par . Licence CC by-sa.
Tags :
2
24
oct.
2019

Bonjour à tous

Récemment, j'ai décidé de m'intéresser un peu à la théorie des types et de la démonstration. Quelques vieilles dépêches y sont pour un peu, et le sujet m'avait toujours un peu intrigué.
Après quelques recherches, j'ai trouvé et commencé l'excellent Logic Foundations.
J'en suis arrivé lentement mais sûrement au chapitre sur les propositions inductives (IndProp).
Et là j'ai un petit soucis…

Lemma le_trans : forall m n o, m <= n -> n <= o
(...)

Journal Xavier Leroy est le lauréat 2016 du Prix Milner.

Posté par . Licence CC by-sa.
52
25
nov.
2016

Hier, jeudi 24 novembre 2016, Xavier Leroy a reçu le prix Milner à Londres à la Royal Society. Le prix Milner est le plus grand prix européen en informatique; il est décerné conjointement par la Royal Society, l'Académie des Sciences et l'académie allemande Leopoldina. Il est décerné en l'honneur de l'informaticien britannique Robin Milner qui fut lauréat du Prix Turing en 1992.

Le prix revient cette année à Xavier Leroy pour ses travaux tant théoriques que pratiques sur la fiabilité (...)