WikiLuc

Guest connection: login: Guest, password: anonymous

User Tools

Site Tools


dit:cours:maths2

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

dit:cours:maths2 [2017/04/05 17:06] (current)
Line 1: Line 1:
 +====== Cours de programmation OCaml ======
 +
 +  * Responsable:​ [[Luc.Bouge@ens-rennes.fr|Luc Bougé]], à Ker Lann le mardi (le lundi et le vendredi à l'​IRISA sur le Campus de Beaulieu)
 +
 +======Support technique Ocaml ======
 +
 +  * [[http://​caml.inria.fr/​ocaml/​release.fr.html|Installation]]
 +  * [[http://​caml.inria.fr/​pub/​docs/​manual-ocaml/​|Documentation]] (en anglais)
 +  * [[https://​opam.ocaml.org/​|Installateur OPAM]] et liste des [[https://​opam.ocaml.org/​packages/​|paquets logiciels]] disponibles. ​
 +  * Le mode [[https://​opam.ocaml.org/​packages/​tuareg/​tuareg.2.0.8/​|tuareg]] pour emacs
 +  * La page des [[http://​form-ocaml.forge.ocamlcore.org/​modules/​env.html#​ide|environnements de développement intégrés]] Ocaml (IDE). L'​éditeur [[http://​www.typerex.org/​ocaml-top.html|OCaml-top]] est un éditeur dédié à l'​apprentissage d'​OCaml.
 +
 +<WRAP center round tip 60%>
 +Une bonne manière de commencer: [[http://​try.ocamlpro.com/​]],​ un
 +environnement en ligne utilisable à travers votre navigateur. Rien à
 +installer! Ça suffit largement pour ce premier cours.
 +
 +
 +/​***********************
 +
 +Pour utiliser ocaml en mode terminal, je recommande l'​utilitaire [[http://​freecode.com/​projects/​rlwrap|rlwrap]] qui permet d'​éditer les entrées, à la manière du shell. Il est disponible dans de nombreuses distributions.
 +Utilisation:​ ''​rlwrap | ocaml''​
 +
 +*************************/​
 +</​WRAP>​
 +
 +----
 +
 +====== Programme du cours ======
 +
 +
 +====== Cours 3: Références,​ aspects impératifs,​ tableaux ======
 +
 +{{ http://​courses.cs.vt.edu/​csonline/​DataStructures/​Lessons/​OrderedListImplementationView/​linked_list.gif?​200}}
 +
 +20 janvier 2015
 +
 +  * Notion de référence,​ égalité, identité
 +  * Effets de bord
 +  * Tableaux
 +  * Listes modifiables
 +
 +=== Références ===
 +
 +  * Le type [[dit:​cours:​prog1:​cours04|milist]] des listes d'​entiers modifiables
 +  * L'​article de la semaine: [[http://​dl.acm.org/​citation.cfm?​id=2089138|The four Rs of programming language design]], Dominic Orchard ​
 +
 +<​blockquote>​
 +Language
 +designers are forever searching for the “proper language” for a domain, task, 
 +or class of programs, such that everything – such as correctness,​ optimisations,​ abstractions,​ high-level
 +structures, solutions to a problem, etc. – becomes clearer when the language is used. The
 +four Rs capture the key aspects of programming language’s affect on programs, in its ability to improve
 +reading, writing, running, and reasoning.
 +
 +These are four important areas that we need to consider when
 +designing effective languages. The four Rs
 +are not meant to argue whether a language is “good” or “bad”, or to unilaterally promote
 +one over the other. Instead, the four Rs
 +provide a framework for thinking critically about the effectiveness of languages and language features.
 +Trade-offs between the four Rs have given a broad and beautiful spectrum of programming languages over the last 70 years. I await further languages with excitement and hope that with better
 +languages everything might become clearer.
 +
 +<​cite>​[[http://​dl.acm.org/​citation.cfm?​id=2089138|The four Rs of programming language design]], Dominic Orchard</​cite>​
 +</​blockquote>​
 +
 +----
 +
 +
 +====== Cours 2 (TP): Programmation récursive, listes ======
 +
 +{{  http://​gallium.inria.fr/​~remy/​poly/​ocaml/​ocaml001.gif?​400}}
 +
 +16 janvier 2015
 +
 +  * Programmation récursive
 +  * Listes Ocaml
 +  * Fonctions classiques
 +  * Itérateurs:​ map et reduce
 +
 +=== Références ===
 +
 +  * Le type [[dit:​cours:​prog1:​cours02|ilist]] et quelques fonctions classiques
 +  * Le livre de la semaine: [[http://​www.decitre.fr/​livres/​types-de-donnees-et-algorithmes-9782840740230.html|Types de données et algorithmes]],​ Marie-Claude Gaudel, Michèle Soria, Christine Froidevaux
 +  * Le module de la semaine: [[http://​caml.inria.fr/​pub/​docs/​manual-ocaml/​libref/​List.html|The List Module]]
 +
 +----
 +
 +====== Cours 1: Introduction à Caml ======
 +
 +{{  http://​cacm.acm.org/​system/​assets/​0000/​2966/​052010_CACMpg20_Robin-Milner.large.jpg?​200}}
 +
 +9 janvier 2015
 +
 +  * Historique, grands noms
 +  * Présentation générale: interprète interactif, synthèse de type, évaluation
 +  * Types et opérateurs de base: int, float, char, string, bool, synthèse de type
 +  * Fonctions: définition explicite, lambda-expressions,​ curryfication,​ ordre supérieur
 +  * Constructeurs de types: produit, somme
 +
 +=== Références ===
 +
 +  * La page de la semaine: [[http://​caml.inria.fr/​about/​history.en.html|A History of Caml]]
 +  * Le grand homme de la semaine: [[http://​en.wikipedia.org/​wiki/​Robin_Milner|Robin Milner]], [[http://​cacm.acm.org/​magazines/​2010/​6/​92474-robin-milner-the-elegant-pragmatist/​fulltext|The elegant pragmatist]]
 +
 +----
 +
 +====== Bibliographie ======
 +
 +===== Histoire des mathématiques =====
 +
 +{{  :​dit:​cours:​russell.png?​200}}
 +
 +  * [[http://​fr.wikipedia.org/​wiki/​Bertrand_Russell|Bertrand Russell]]
 +
 +<WRAP center round tip 60%>
 +Allez vite lire [[http://​www.logicomix.com/​fr/​|Logicommix]],​ l'​histoire de Russell en bandes dessinées. Disponible à la bibliothèque de l'ENS ([[http://​bibliopac.ens-rennes.fr/​cgi-bin/​koha/​opac-detail.pl?​biblionumber=14646|F4 1 DOX]])
 +</​WRAP>​
 +
 +  * [[http://​fr.wikipedia.org/​wiki/​Nicolas_Bourbaki|Nicolas Bourbaki]]
 +
 +<​blockquote>​
 +<​cite>​[[http://​fr.wikipedia.org/​wiki/​Nicolas_Bourbaki#​La_mort_de_Bourbaki|Wikipedia]]</​cite>​
 +Les familles Cantor, Hilbert, Noether ; les familles Cartan, Chevalley, Dieudonné, Weil ; les familles Bruhat, Dixmier, Samuel, Schwartz ; les familles Cartier, Grothendieck,​ Malgrange, Serre ; les familles Demazure, Douady, Giraud (de), Verdier ; les familles filtrantes à droite et les épimorphismes strictes, mesdemoiselles Adèle et Idèle ;
 +
 +{{:​dit:​cours:​bourbaki.png?​200 ​ }}
 +
 +ont la douleur de vous faire part du décès de M. Nicolas Bourbaki, leur père, frère, fils, petit-fils arrière-petit-fils et petit-cousin respectivement pieusement décédé le 11 novembre 1968, jour anniversaire de la victoire, en son domicile de Nancago. La crémation aura lieu le samedi 23 novembre 1968 à 15 heures au cimetière des fonctions aléatoires,​ métro Markov et Gödel.
 +
 +On se réunira devant le bar « aux produits directs », carrefour des résolutions projectives,​ anciennement place Koszul.
 +
 +Selon les vœux du défunt, une messe sera célébrée en l'​église Notre-Dame des problèmes universels, par son éminence le Cardinal Aleph 1 en présence des représentants de toutes les classes d'​équivalence et des corps algébriquement clos constitués. Une minute de silence sera observée par les élèves des Écoles normales supérieures et des classes de Chern.
 +
 +Car Dieu est le compactifié d'​Alexandrov de l'​univers,​ Grothendieck IV, 22.
 +</​blockquote>​
 +
 +
 +===== Langages de programmation =====
 +
 +  * [[http://​www.exblog.fr/​public/​divers/​histoire-langages-programmation|History of programming languages]]
 +  * [[http://​www.tiobe.com/​index.php/​content/​paperinfo/​tpci/​|TIOBE Programming Community index]], ​ an indicator of the popularity of programming languages
 + 
 +
 +<​blockquote>​
 +<​cite>​[[http://​en.wikipedia.org/​wiki/​Measuring_programming_language_popularity|Measuring programming language popularity]]</​cite>​
 +It is difficult to determine which programming languages are most widely used, and what usage means varies by context. One language may occupy the greater number of programmer hours, a different one have more lines of code, a third may utilize the most CPU time, and so on. Some languages are very popular for particular kinds of applications. For example, COBOL is still strong in the corporate data center, often on large mainframes; FORTRAN in engineering applications;​ C in embedded applications and operating systems; and other languages are regularly used to write many different kinds of applications.
 +</​blockquote>​
 +
 +
 +
 +===== CAML =====
 +
 +{{  http://​www.pps.univ-paris-diderot.fr/​~cousinea/​Book/​ApprocheBook.gif?​200}}
 +
 +  * //​[[http://​www.pps.univ-paris-diderot.fr/​~cousinea/​Book/​livre.html|Approche fonctionnelle de la programmation]]//,​ Guy Cousineau et Michel Mauny
 +
 +===== Scheme =====
 +
 +  * [[http://​mitpress.mit.edu/​sicp/​|Structure and Interpretation of Computer Programs]], Harold Abelson, Gerald Jay Sussman, Julie Sussman, MIT Press. ​
 +
 +===== Sémantique =====
 +
 +  * Le cours de programmation de l'X: //​[[http://​www.editions.polytechnique.fr/?​afficherfiche=130|Les principe des langages de programmation]]//,​ Gilles Dowek
 +  * Le cours de sémantique de l'X: //​[[http://​www.editions.polytechnique.fr/?​afficherfiche=96|Introduction à la théorie des langages de programmation]]//,​ Gilles Dowek, Jean-Jacques Lévy 
 +
 +
 +===== Lambda-calcul =====
 +
 +  * Une petite introduction:​ //​[[http://​perso.ens-lyon.fr/​pierre.lescanne/​ENSEIGNEMENT/​PROG2/​06-07/​lambda_gen.pdf|Introduction au lambda-calcul]]//,​ Pierre Lescanne, ENS Lyon; voir aussi la suite sur la [[http://​perso.ens-lyon.fr/​pierre.lescanne/​ENSEIGNEMENT/​PROG2/​|page générale du cours]]
 +  * La Bible, approche française: //​[[http://​www.eyrolles.com/​Sciences/​Livre/​lambda-calcul-types-et-modeles-9782225820915|Lambda-calcul,​ types et modèles]]//,​ Jean-Louis Krivine
 +  * La Bible, approche anglo-saxonne:​ //​[[http://​books.google.fr/​books/​about/​The_Lambda_Calculus.html?​hl=fr&​id=ZdydJZVue50C|The Lambda Calculus: Its Syntax and Semantics]]//,​ H.P. Barendregt
 +  * Théorie des types: //​[[http://​www.springer.com/​mathematics/​book/​978-1-4020-2334-7|A Modern Perspective on Type Theory, From its Origins until Today]]//, ​ F.D. Kamareddine,​ T. Laan, Rob Nederpelt
 +
 +
 +
 +===== Théorie des catégories =====
 +
 +  * Une petite introduction:​ //​[[http://​mitpress.mit.edu/​books/​basic-category-theory-computer-scientists|Basic Category Theory for Computer Scientists]]//,​ Benjamin C. Pierce
 +  * Application à ML: //​[[http://​dl.acm.org/​citation.cfm?​id=49340|Computational category theory]]//, David E. Rydeheard, Rod M. Burstall
 +  * Équations récursives aux domaines: //​[[http://​dl.acm.org/​citation.cfm?​id=200952|Mathematical theory of domains]]//,​ Viggo Stoltenberg-Hansen,​ Ingrid Lindström, Edward R. Griffor
 +
 +-----
 +
 +====== Outils, environnements de programmation,​ etc. ======
 +
 +
 +/​***************************
 +
 +===== Geany =====
 +
 +{{  http://​www.geany.org/​images/​geany.png?​100}}
 +Un environnement de développement recommandé pour OCaml: [[http://​www.geany.org/​|Geany]]
 +
 +Geany is known to run under Linux, FreeBSD, NetBSD, OpenBSD, MacOS X, AIX v5.3, Solaris Express and Windows. More generally, it should run on every platform, which is supported by the GTK libraries. Only the Windows port of Geany is missing some features.
 +
 +
 +***************************/​
 +===== OCaml =====
 +
 +  * [[http://​caml.inria.fr/​|Site]] de référence. Nous utilisons la version 4.
 +  * [[http://​caml.inria.fr/​pub/​docs/​manual-ocaml-4.01/​|Documentation]] en ligne
 +  * Mode emacs [[https://​github.com/​ocaml/​tuareg#​tuareg-an-emacs-ocaml-mode|tuareg]]. NB: Ce mode est disponible dans de nombreuses distributions.
 +
 +
 +/​****************
 +
 +
 +====== Cours 4: Références ======
 +
 +{{ http://​courses.cs.vt.edu/​csonline/​DataStructures/​Lessons/​OrderedListImplementationView/​linked_list.gif?​200}}
 +
 +9 octobre 2014
 +
 +  * Notion de référence,​ égalité, identité
 +  * Effets de bord
 +  * Champs modifiables
 +  * Listes modifiables
 +  * Arbres modifiables
 +
 +=== Références ===
 +
 +  * Le type [[dit:​cours:​prog1:​cours04|milist]] des listes d'​entiers modifiables
 +  * L'​article de la semaine: [[http://​dl.acm.org/​citation.cfm?​id=2089138|The four Rs of programming language design]], Dominic Orchard ​
 +
 +<​blockquote>​
 +Language
 +designers are forever searching for the “proper language” for a domain, task, 
 +or class of programs, such that everything – such as correctness,​ optimisations,​ abstractions,​ high-level
 +structures, solutions to a problem, etc. – becomes clearer when the language is used. The
 +four Rs capture the key aspects of programming language’s affect on programs, in its ability to improve
 +reading, writing, running, and reasoning.
 +
 +These are four important areas that we need to consider when
 +designing effective languages. The four Rs
 +are not meant to argue whether a language is “good” or “bad”, or to unilaterally promote
 +one over the other. Instead, the four Rs
 +provide a framework for thinking critically about the effectiveness of languages and language features.
 +Trade-offs between the four Rs have given a broad and beautiful spectrum of programming languages over the last 70 years. I await further languages with excitement and hope that with better
 +languages everything might become clearer.
 +
 +<​cite>​[[http://​dl.acm.org/​citation.cfm?​id=2089138|The four Rs of programming language design]], Dominic Orchard</​cite>​
 +</​blockquote>​
 +
 +----
 +
 +====== Cours 3: Théorie des catégories,​ somme et produit ======
 +
 +{{ http://​www.kent.ac.uk/​secl/​philosophy/​jw/​reasoning/​2013/​category/​pullback.png?​200}}
 +
 +3 octobre 2014
 +
 +  * Théorie des catégories
 +  * Produit et somme catégoriques
 +  * Application aux listes
 +  * Applications aux arbres
 +
 +=== Références ===
 +
 +  * Les types [[dit:​cours:​prog1:​cours03|ilist et itree]] avec une approche catégorique
 +  * Le livre de la semaine: ​ [[http://​mitpress.mit.edu/​books/​basic-category-theory-computer-scientists|Basic Category Theory for Computer Scientists]],​ Benjamin C. Pierce
 +  * Le grand homme de la semaine: [[http://​fr.wikipedia.org/​wiki/​Dana_S._Scott|Dana Scott]]; voir aussi la page Wikipedia sur la [[http://​fr.wikipedia.org/​wiki/​Th%C3%A9orie_des_cat%C3%A9gories|Théorie des catégories]]
 +
 +<​blockquote>​
 +Abstract nonsense, or general abstract nonsense, is a popular term used by mathematicians to describe certain kinds of arguments and concepts in category theory or applications. The term goes back a long way, and even predates the foundation of category theory as a subject itself. Referring to a joint paper with Samuel Eilenberg that introduced the notion of a "​category"​ in 1942, Saunders Mac Lane wrote the subject was 'then called "​general abstract nonsense"'​.
 +
 +The term is believed to have been coined by the mathematician Norman Steenrod, himself one of the developers of the categorical point of view. This term is used by practitioners as an indication of mathematical sophistication or coolness rather than as a derogatory designation.
 +
 +<​cite>"​Logical abstract nonsense is a subfield of general abstract nonsense",​ [[http://​languagelog.ldc.upenn.edu/​nll/?​p=108|Language Log]]</​cite>​
 +</​blockquote>​
 +
 +-----
 +
 +
 +**************/​
 +
  
dit/cours/maths2.txt · Last modified: 2017/04/05 17:06 (external edit)