Livres sur la sémantique des langages de programmation

31

J'ai lu Nielson & Nielson " Semantics with Applications ", et j'aime vraiment le sujet. J'aimerais avoir un livre de plus sur la sémantique du langage de programmation - mais je ne peux vraiment en obtenir qu'un.

J'ai jeté un œil au livre Turbak / Gifford , mais il est trop long; Je pensais que Winskel irait bien, mais je n'y ai pas accès (ce n'est pas dans notre bibliothèque universitaire, et je manque d'argent), et je ne suis même pas sûr si ce n'est pas daté. Slonneger semble OK, mais la partie pratique le rend un peu trop long, et je ne suis pas très à l'aise avec son style.

Ma question est donc - Winskel est- il un bon livre? Et est-il daté?

Existe-t-il également d'autres livres concis sur le sujet?

reference-request pl.programming-languages semantics denotational-semantics books Geai
la source
5
ajout de liens vers les pages des éditeurs pour tous les livres. pourrait être utile pour ceux qui souhaitent naviguer.
Suresh Venkat
2
Quel genre de sémantique vous intéresse? Dénotation? Opérationnel? Un aperçu?
Ohad Kammar
@Ohad Kammar: Je m'intéresse aux deux.
Jay

Réponses:

31

Tout dépend de la profondeur à laquelle vous voulez aller et de ce que vous savez déjà. Pour un débutant, le livre de Winksel est vraiment sympa, mais oui, il ne vous présente pas l'état de l'art en sémantique tel qu'il a été écrit il y a environ 20 ans. Néanmoins, c'est toujours une bonne première introduction au sujet. Il pourrait également être utile de souligner que T. Nipkow a officialisé une partie substantielle du livre de Winskel dans Isabelle / HOL, voir ici . Donc, si vous voulez apprendre à utiliser des assistants de preuve interactifs avec la compréhension de la sémantique des langages de programmation, vous avez beaucoup de matériel cohérent à utiliser.

D'autres livres plus avancés sont:

  • Gunter, Semantics of Programming Languages , un livre plus avancé axé sur la sémantique dénotationnelle, une approche de la sémantique, qui n'a pas répondu aux attentes. Se concentre sur des langues purement fonctionnelles et ignore la concurrence. C'est le livre à partir duquel j'ai appris la sémantique en tant que premier cycle, et rétrospectivement, j'aurais préféré utiliser le livre de Winksel à la place. Gunter n'est pas une lecture facile pour un débutant.

  • Domaines et lambda-calculi par Amadio et Curien. Un autre livre à venir écrit plus dans la tradition de la théorie des domaines, bien qu'il discute des calculs de processus.

  • Les livres de John Mitchell qui ont déjà été mentionnés ci-dessus. Ils concernent également principalement le calcul séquentiel.

Des livres comme TAPL de Pierce sont très agréables, mais se concentrent étroitement sur un aspect des langages de programmation, à savoir les types, aussi importants soient-ils. Je ne le recommanderais pas comme une première introduction au domaine général des langages de programmation, mais il est obligatoire de le lire pour quiconque souhaite en savoir plus sur les types.

À vrai dire, je pense qu'il n'y a actuellement aucun livre d'introduction à jour sur la sémantique des langues qui reflète les progrès substantiels de la dernière décennie, avec son passage décisif des méthodes de dénotation et du calcul séquentiel à la concurrence (calculs de processus et sémantique des jeux) , la sémantique axiomatique et l'utilisation d'assistants de preuve interactifs dans la vérification.

Mise à jour 22. Avril 2014: Tobias Nipkow et Gerwin Klein ont publié un nouveau livre

qui peut être vu comme «Winskel in Isabelle / HOL». C'est une introduction à la sémantique des langages de programmation (principalement opérationnels et axiomatiques) mais contrairement aux précédentes approches sur papier et stylo, ce livre exprime toutes ses mathématiques en Isabelle / HOL. En d'autres termes, c'est en même temps un livre sur la démonstration des théorèmes.

Le livre est tout neuf, donc je ne l'ai pas utilisé pour l'enseignement, mais il semble vraiment convenir comme une introduction qui est présentée à un niveau inférieur à Software Foundations par Pierce et al.

Martin Berger
la source
2
Y a-t-il un changement par rapport aux méthodes dénotationnelles? Cela me semble plus comme le genre de personnes qui auparavant utilisaient des preuves ondulées à la main, de nos jours, on s'attend à ce qu'elles produisent des preuves formelles. Comme les méthodes de dénotation ne peuvent toujours pas modéliser facilement tout ce que nous faisons et nécessitent de nombreuses autres conditions préalables, ces chercheurs utilisent des méthodes plus accessibles telles que les jeux, les calculs de processus, les assistants de preuve. Je ne sais pas s'il y a une baisse des méthodes de dénotation.
Ohad Kammar
4
Veuillez ne pas confondre la sémantique dénotationnelle avec la théorie des domaines . La sémantique du jeu peut être et est généralement parfaitement dénotationnelle, c'est-à-dire que la signification d'un programme est fonction de la signification de ses parties.
Andrej Bauer
2
J'ai ouvert un nouveau fil concernant ce commentaire. Mais même si je ne suis pas sûr d'être d'accord avec votre définition, la sémantique du jeu est de nature dénotationnelle. Je pense que je devrais remplacer "jeux" par "sémantique opérationnelle" dans mon commentaire, et inclure la sémantique des jeux comme peut-être une autre forme de recherche sémantique dénotationnelle. cstheory.stackexchange.com/questions/3577/…
Ohad Kammar
1
Je ne suis pas convaincu qu'il y ait un changement. Voir mon premier commentaire, à la lumière du commentaire d'Andrej.
Ohad Kammar
1
Y a-t-il un changement? Une question intéressante. Comment mesurer un changement? Il y a tellement de critères que nous pourrions appliquer, des critères relativement concrets comme le montant des subventions de recherche accordées à différentes approches, aux idées vagues comme la part d'esprit. Compte tenu de notre implication, en tant que chercheurs, en tant qu'employés, en tant que demandeurs de subventions, dans le résultat d'une telle question, il est peu probable que nous nous mettions d'accord sur une réponse.
Martin Berger
20

Voici un échantillon aléatoire de documents disponibles gratuitement en ligne:

  • Winskel, La sémantique formelle des langages de programmation , aperçu de Google Livres . Je ne sais rien de ce livre. C'est sur la liste parce que la question porte spécifiquement sur son contenu, qui est principalement en ligne.
  • Morgan, Programming from Specification , liste des fichiers ps . Le sujet est le raffinement, qui est le processus consistant à commencer par des descriptions de haut niveau non exécutables et à les transformer systématiquement en quelque chose d'exécutable. Bien sûr, chaque étape de raffinement doit préserver la sémantique, donc elle traite également d'un certain type de sémantique (basé principalement sur les transformateurs de prédicat).
  • Harper, Fondements pratiques des langages de programmation , pdf de l'ébauche . Voir le commentaire de Dave Clarke ci-dessous.
  • Remy, Using, Understanding, and Unraveling the OCaml Language , pdf . Voici le livre dont j'ai appris la programmation fonctionnelle (OCaml, plus précisément) et je l' ai aimé beaucoup . Il présente la sémantique des fonctionnalités de base du langage d'une manière très agréable et dans le processus présente le calcul lambda et la théorie des types sur la base des `` besoins de savoir ''.
  • Peyton Jones, L'implémentation des langages de programmation fonctionnelle , djvu . Les premiers chapitres décrivent le calcul lambda (et sa `` sémantique opérationnelle '') et comment les fonctionnalités de langage de niveau supérieur sont intégrées dans le calcul lambda. En ce sens, l'article donne une sémantique opérationnelle pour les langages fonctionnels.
  • Pierce (ed), Rubriques avancées sur les types et les langages de programmation , aperçu de Google Livres .
  • Slonneger, Syntaxe et Sémantique des Langages de Programmation , liste des fichiers pdf . Je l'ai regardé brièvement il y a longtemps et je n'ai pas beaucoup aimé. C'est sur la liste parce que c'est mentionné dans la question.
  • Brookes, A Semantics for Concurrent Separation Logic , pdf . C'est un gros article (80 pages), pas un livre. Je l'ai inclus parce que c'est un développement assez récent que je trouve intéressant.
Radu GRIGore
la source
1
c'est beaucoup de liens :)
Suresh Venkat
3
Cela serait plus utile s'il avait été présenté sous forme de liste. Quoi qu'il en soit, je recommanderais le livre Harper: cliquez sur "pourrait".
Dave Clarke
Je suis d'accord. Radu, pourriez-vous énumérer les livres, afin que nous sachions sur quoi nous cliquons? ce serait une excellente ressource.
Suresh Venkat
C'est une liste maintenant. (La première version a été publiée vers 2h du matin, après avoir dormi environ 5h la nuit précédente.: P)
Radu GRIGore
16

Je diviserais les livres sur la sémantique du langage de programmation en deux classes: ceux qui se concentrent sur la modélisation des concepts du langage de programmation et ceux qui se concentrent sur les aspects fondamentaux de la sémantique. Il n'y a aucune raison qu'un livre ne puisse pas faire les deux. Mais, généralement, il n'y a que peu de choses que vous pouvez mettre dans un livre, et les auteurs ont également leurs propres prédispositions sur ce qui est important.

Le livre de Winskel, déjà mentionné, traite un peu des deux aspects. Et, c'est un bon livre pour débutant. Un livre tout aussi bon, peut-être même meilleur, est celui avec lequel j'ai commencé: la description dénotative de Gordon des langages de programmation . Ce fut mon premier livre sur la sémantique, que j'ai lu peu de temps après avoir terminé mes études de premier cycle. Je dois dire que cela m'a donné une base solide en sémantique et je n'ai jamais eu à me demander en quoi la sémantique dénotationnelle diffère de la sémantique opérationnelle ou de la sémantique axiomatique, etc. Ce livre restera mon préféré de tous les temps sur la sémantique dénotationnelle.

D'autres livres qui se concentrent sur les aspects de modélisation plutôt que sur les aspects fondamentaux sont les suivants:

  • La sémantique des langages de programmation de Tennent , qui est un livre plus ou moins à jour sur la sémantique des langages de programmation impératifs. Ç'est facile a lire. Cependant, il a tendance à être abstrait dans les parties ultérieures du livre et vous pourriez avoir du mal à voir pourquoi les choses sont faites d'une manière particulière.

  • Théories de Reynolds sur les langages de programmation . Toute personne spécialisée en sémantique doit absolument lire ce livre. C'est après tout de Reynolds. (David Schmidt m'a dit un jour: "même si Reynolds vous lit le journal du matin, vous voulez écouter attentivement, car vous pourriez apprendre quelque chose d'important"!). Il a une bonne couverture à la fois des aspects de la modélisation et des aspects fondamentaux.

Les meilleurs livres sur les aspects fondamentaux sont ceux de Gunter (que je considère comme un livre de doctorat) et Mitchell (qui est un bon livre de référence à avoir sur votre étagère car il est assez complet).

Uday Reddy
la source
Je suis ravi de vous avoir ici, Uday!
Radu GRIGore
Je suis content d’être ici aussi. Ceci est une très belle ressource!
Uday Reddy
Que diriez-vous: Transitions et arbres: une introduction à la sémantique structurelle opérationnelle de Hans Hüttel 2010. Semble avoir de bonnes critiques, mais personne ne le mentionne ici.
Arturo Hernandez
1
@Uday: Merci pour la réponse. Que signifient «modélisation des concepts du langage de programmation» et «aspects fondamentaux de la sémantique»? Quelles sont leurs différences et leurs relations?
Tim
1
@Tim: Pour donner la sémantique d'un langage de programmation, vous avez besoin d'une certaine forme de structures mathématiques, par exemple, des ensembles dans le cas le plus simple, mais des structures sophistiquées comme des domaines, des catégories, des coalgebras, etc. pour des problèmes que les ensembles ne peuvent pas gérer. Par «aspects fondamentaux», j'entends la théorie de ces structures plus sophistiquées. Dans le premier cas, l'accent est mis sur les langages de programmation et, dans le second cas, sur les fondements mathématiques.
Uday Reddy
8

J'ai vraiment apprécié lire Winskel lorsque je suivais le cours de premier cycle sur la sémantique. Je ne peux pas dire si c'est daté, car je ne fais pas de recherche dans ce domaine. Un avantage de Winskel est que vous pouvez le trouver traduit dans d'autres langues que l'anglais.

Pour une lecture plus approfondie, plus à un niveau supérieur, je suggère les livres de John Mitchell, Foundations for Programming Languages and Concepts in Programming Languages . Si vous ne lisez que les premiers chapitres, je suppose qu'ils répondent également à votre exigence de concision.

Vous ne trouverez pas de brouillons gratuits de ces livres, donc si vous avez un budget limité, optez pour le «pourrait» dans la réponse de Radu.

Alessandro Cosentino
la source
6

Eh bien, je ne suis pas un expert en la matière, mais je peux donner quelques conseils généraux.

Tout d'abord, il y a des gens qui ont déjà lu le livre et fourni des critiques à ce sujet. Par exemple, pour le livre Winskel The Formal Semantics of Programming Languages (voir [1] et [2] ), j'ai trouvé des critiques sur Amazon.

Une partie d'une critique se lit comme suit:

Ce livre confond la syntaxe et la sémantique depuis le début, comme séparant les littéraux de ses valeurs. Aucune notation spéciale n'a été utilisée pour les différencier. C'est une question cruciale que l'auteur devrait aborder dans un sujet comme celui-ci. De plus, certaines autres notations qu'il a utilisées sont assez déroutantes, comme montrer les prémisses et les conclusions.

L'auteur semble supposer que vous avez TOUTES les conditions préalables nécessaires car il a expliqué très brièvement les documents de base dans les premiers chapitres (c'est-à-dire la théorie des ensembles, la sémantique opérationnelle, les inductions, les définitions inductives). Le style utilisé par l'auteur en introduction est de mettre deux ou trois paragraphes de textes et de mettre quelques formules puis de faire des exercices. Ce qui est pour moi assez frustrant ...

18/20 personnes ont trouvé cet avis utile. Vous pouvez rechercher Amazon (ou d'autres sources) pour voir plus d'avis.

Deuxièmement, Amazon propose des types et des langages de programmation et une théorie des catégories de base pour les informaticiens avec ce livre. Sur un autre sujet, Dave Clarke propose ces livres comme d'excellents sur les «systèmes de types et la sémantique du langage de programmation». Encore une fois, je ne suis pas un expert, mais ceux-ci pourraient vous être utiles.

MS Dousti
la source
TaPL va un peu trop lentement à mon goût. C'est un bon livre, mais je l'ai mentionné parce que la personne qui pose la question semble inquiète pour les livres "de longue haleine".
Radu GRIGore
@Radu: Certes, TAPL est lent, mais c'est une assez bonne introduction. Le livre Harper que vous avez mentionné dans vos liens va beaucoup plus vite et couvre beaucoup plus de terrain, bien qu'il ne soit pas encore terminé.
Dave Clarke
4
Prenez cette critique Amazon du livre de Winskel avec une pincée de sel. Il est souvent utilisé comme texte recommandé dans les cours de sémantique de premier cycle et attire peut-être des étudiants mécontents. J'ai lu le livre et j'ai trouvé les chapitres d'introduction plus que suffisants. Sa notation tout au long semblait également être tout à fait standard.
Dominic Mulligan