Comprendre les expressions régulières avec Regexper

Les expressions rationnelles, ou expressions régulières, sont un outil très puissant pour manipuler les chaines de caractères dans les langages de programmation. Perl en fait son principe fondamental, mais on les trouve aussi dans les langages plus habituels comme en Java avec la méthode "matches". Elles sont présentées au chapitre 3 du cours e-miage B209.

Il existe un outil intéressant permettant de représenter de manière graphique de telles expressions : Regexper (http://www.regexper.com/).

Par exemple, l'expression "a*|(b+c)*b" donnera :

A tester d'urgence !

Books and papers every graduate student should read

Une série de références de livres pour tout étudiant en informatique (en particulier autour des langages de programmation et des compilateurs).

Books and papers every graduate student should read

Bayesian Reasoning and Machine Learning

"Bayesian Reasoning and Machine Learning", By David Barber

The last decade has seen considerable growth in interest in Arti cial Intelligence and Machine Learning. In the broadest sense, these elds aim to `learn something useful' about the environment within which the organism operates. How gathered information is processed leads to the development of algorithms how to process high dimensional data and deal with uncertainty. In the early stages of research in Machine Learning and related areas, similar techniques were discovered in relatively isolated research communities. Whilst not all techniques have a natural description in terms of probability theory, many do, and it is the framework of Graphical Models (a marriage between graph and probability theory) that has enabled the understanding and transference of ideas from statistical physics, statistics, machine learning and information theory. To this extent it is now reasonable to expect that machine learning researchers are familiar with the basics of statistical modelling techniques.

This book concentrates on the probabilistic aspects of information processing and machine learning.

The 2012 version of the book : http://web4.cs.ucl.ac.uk/staff/D.Barber/textbook/270212.pdf
The book website :  http://www.cs.ucl.ac.uk/staff/d.barber/brml/
The author website : http://web4.cs.ucl.ac.uk/staff/D.Barber/pmwiki/pmwiki.php?n=Brml.HomePage

Preuves de programmes en COQ

Un podcast vidéo (fuscia.info) sur un langage permettant la preuve de fonctions : COQ.


Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits.

Dans ce cours, sont présentés les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique d'ordre supérieur. Tous ces aspects reposent sur l'utilisation avancée de la notion de typage et sur les relations intimes entre types, spécifications, et calculs.


L'auteur Yves Bertot est chercheur à l'INRIA et travaille avec le système depuis une vingtaine d'années.  Il a utilisé ce système pour des études d'algorithmes en technologie des langages de programmation, géométrie, arithmétique des ordinateurs, ...

Ce cours vidéo s'adresse à un public informaticien avec des prérequis qui sont partagés par la majeure partie des ingénieurs du milieu industriel.

A voir sur :
Preuves de programmes en coq - Yves Bertot INRIA

C'est en licence CC-By.

Interstices - À propos des compilateurs

Instructif à propos des compilateurs et de la preuve de programmes :
Interstices - À propos des compilateurs

A voir aussi : http://interstices.info/jcms/n_52365/comment-faire-confiance-a-un-compilateur