IFT 6172 -- Sémantique des langages de programmation


Professeur: Stefan Monnier
Premier cours: mercredi 4 septembre 2019, 10h30-12h30, salle Z-205

English version

Page Moodle du cours pour A2019.

Description

Pensé comme une suite du cours IFT-2035, ce cours présente des concepts avancés dans les langages de programmation.

Étude des concepts des langages de programmation modernes. Les sujets au menu incluent:

Buts: Apprendre les concepts avancés qui apparaissent dans les langages de programmation modernes ainsi que les techniques utilisées pour les définir, les implanter, et analyser leur propriétés.
Se familiariser sur l’état de l’art et les pistes ouvertes de recherche en langages de programmation. Développer son habilité à lire des articles de recherche et à les critiquer dans leur contexte. Développer son autonomie de recherche en langage de programmation.

Une importante partie du cours sera structurée autour de présentations d'articles de journaux et de conférences.

Horaire et dates

Jour Heure Lieu
Lundi 10h30-12h30 Y-115
Mercredi 10h30-12h30 Z-205

Voir aussi le formulaire insupportable de Synchro

Évaluation

Chaque étudiant devra faire 1 travail pratique et 2 présentations. La note sera basée pour 50% sur le travail pratique, 40% sur les présentations et 10% sur la participation en classe.

Travaux pratiques

Le TP est disponible, en français et in English.
Le code est dans la branche tp/ift6172-2019 du repository de Typer.

Manuels

Il n'y a pas de manuel pour ce cours, cependant les livres ci-dessous pourraient être de bons compléments au cours:

Types and Programming Languages de Benjamin C. Pierce, MIT Press.

Computation and deduction de Frank Pfenning (aussi en 2-up).

Lambda Calculi with Types de Henk Barendregt (aussi en 2-up).

Certified Programming with Dependent Types de Adam Chlipala.

Semantics of Programming Languages, Structures and Techniques, Carl A. Gunter, MIT Press.

Notes de cours

Planification par semaine

Semaine du Thème
04 sep Tic Tac Toe
09-11 sep STLC and Mini-ML
Auxiliary material: Pierce's brick book and Pfenning's "computation and deduction"
16-18 sep Mini-ML and System F
23-25 sep System-Fω et PTS
30-02 oct Types dépendents
07-09 oct From System-F to Typed Assembly Language
Type-Preserving Compilation of Featherweight Java
(Thanksgiving) 16 oct TP/Typer
21-23 oct Semaine de lecture
28 oct Présentations
Putting type annotations to work, Oumar Marame Ndione
Fortifying macros, Jean-Alexandre Barszcz
30 oct Présentations
Fun with phantom types, Alice De Berny
What Do Reversible Programs Compute?, Alberto Pérez Robledo
04 nov Présentations
Gradual typing for functional languages, Amara Sountoura
Object-oriented multi-methods in Cecil, Arol Maxwell Sènami Gbeto-Fia
06 nov Présentations
Typed memory management in a calculus of capabilities, Deya Mutombo
An Introduction to Probabilistic Programming, Hongji Chen
11 nov Présentations
Refinement types for ML , Steven Thephsourinthone
Assigning Meaning to Programs, Ian Sabourin
13 nov Présentations
Towards Concurrent Type Theory, Akshay Gopalakrishnan
Type classes: an exploration of the design space, Ben Soilihi Boina Soilihi
18 nov Présentations
To Memory Safety through Proofs, Simon Génier
The simple essence of automatic differentiation, Frederic Boileau
20 nov Présentations
Program synthesis from polymorphic refinement types, Nathaniel Bos
Making COLAs with Pepsi and Coke, Ian Sabourin
25 nov Présentations
Type reconstruction for general refinement types, Deya Mutombo
Self: The power of simplicity, Oumar Marame Ndione
Reflection for Statically Typed Languages, Alice De Berny
27 nov Présentations
Efficient differentiable programming in a functional array-processing language, Frederic Boileau
A lambda-calculus foundation for universal probabilistic programming, Hongji Chen
Extensible Effects : An Alternative to Monad Transformers, Jean-Alexandre Barszcz
02 dec Présentations
The ins and outs of gradual type inference, Steven Thephsourinthone
Shared Memory Consistency : A Tutorial, Akshay Gopalakrishnan
Reflection in logic, functional and object-oriented programming: a Short Comparative Study, Alberto Pérez Robledo
04 dec Présentations
A Calculus for Compiling and Linking Classes, Amara Sountoura
A classification of pointcut language constructs, Ben Soilihi Boina Soilihi
RustBelt: securing the foundations of the rust programming language, Simon Génier
09 (fin) dec Présentations
Generic Zero-Cost Reuse for Dependent Types, Nathaniel Bos
Alias types, Arol Maxwell Sènami Gbeto-Fia

Articles suggérés

Gestion mémoire manuelle

Typed memory management in a calculus of capabilities, Karl Crary, David Walker, and Greg Morrisett.  POPL'99.

Alias types, Frederick Smith, David Walker, and Greg Morrisett. ESOP'00.

Separation logic: A logic for shared mutable data structures, John Reynolds. LICS'02.

Linear Regions Are All You Need, Matthew Fluet , Greg Morrisett , Amal Ahmed. ESOP'06.

RustBelt: securing the foundations of the rust programming language, Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. POPL'18.

Ownership types: a survey, Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. AiOOP'13.

Typage Graduel

Gradual typing for functional languages, Jeremy Siek and Walid Taha. Scheme'06.

Space-efficient gradual typing, David Herman, Aaron Tomb, and Cormac Flanagan. Higher-Order and Symbolic Computation. 2010.

Is sound gradual typing dead?, Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. POPL'16.

Abstracting gradual typing, Ronald Garcia, Alison M. Clark, and Éric Tanter. POPL'16.

Gradual refinement types, Nico Lehmann and Éric Tanter. POPL'17.

The ins and outs of gradual type inference, .

Programmation étagée et méta-programmation

Self-interpretation and reflection in a statically typed language, Konstantin Läufer and Martin Odersky. OORMA'93.

Multi-stage programming with explicit annotations, Walid Taha and Tim Sheard. PEPM'97.

Tagless staged interpreters for typed languages, Emir Pašalić, Walid Taha, and Tim Sheard. ICFP'02.

Environment classifiers, Walid Taha, Michael Florentin Nielsen. POPL'03.

Typed Tagless Final Interpreters, Oleg Kiselyov. Generic and Indexed Programming, 2012.

The Design and Implementation of BER MetaOCaml, Oleg Kiselyov. FLOPS'14.

Syntaxe extensible

Hygienic macros through explicit renaming, William Clinger. Lisp pointers, 1991.

Taming Macros, Ryan Culpepper and Matthias Felleisen. GPCE'04.

Fortifying macros, Ryan Culpepper and Matthias Felleisen. ICFP'10.

Towards the Essence of Hygiene, Michael D. Adams. POPL'15.

Honu: Syntactic Extension for Algebraic Notation through Enforestation, Jon Rafkind and Matthew Flatt. GPCE'12.

Continuations délimitées

Abstracting control, Olivier Danvy and Andrzej Filinski. LFP'90.

On the Dynamic Extent of Delimited Continuations, Darius Biernacki, Olivier Danvy, and Chung-Chieh Shan. IPL-2005.

Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform, Tiark Rompf, Ingo Maier, and Martin Odersky. ICFP'09.

Inférence de types

Principal type-schemes for functional programs, Luis Damas and Robin Milner, POPL'82.

Putting type annotations to work, Martin Odersky and Konstantin Läufer. POPL'96.

Type Inference with Constrained Types, Martin Odersky, Martin Sulzmann, and Martin Wehr. TAPOS'99.

Discriminative sum types locate the source of type errors, Matthias Neubauer and Peter Thiemann. ICFP'03.

MLF: Raising ML to the Power of System F, Dider Le Botlan and Dider Rémy. ICFP'03.

Type reconstruction for general refinement types, Kenneth Knowles and Cormac Flanagan. ESOP'07.

OutsideIn(X): Modular type inference with local assumptions, Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. JFP'11.

Différentiation automatique

Functional differentiation of computer programs, Jerzy Karczmarczuk. ICFP'98.

Beautiful differentiation, Conal Elliott. ICFP'09.

Continuity analysis of programs, Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. POPL'10.

The simple essence of automatic differentiation, Conal Elliott. ICFP'18.

Types dépendants et indexés

Fun with phantom types, Ralf Hinze.

Eliminating array bound checking through dependent types, Hongwei Xi and Frank Pfenning, PLDI'98.

Guarded recursive datatype constructors, Hongwei Xi, Chiyan Chen, and Gang Chen. POPL'03.

Meta-programming with built-in type equality, Tim Sheard and Emir Pašalić. LFMTP'04.

Refinement types

Refinement types for ML, Tim Freeman and Frank Pfenning. PLDI'91.

LiquidHaskell: experience with refinement types in the real world, Niki Vazou, Eric L. Seidel, and Ranjit Jhala. Haskell'14.

Program synthesis from polymorphic refinement types, Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. PLDI'16.

Refinement types for secure implementations, Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. TOPLAS'11.

Objets

Self: The power of simplicity, David Ungar and Randall B. Smith. OOPSLA'87.

How to make ad-hoc polymorphism less ad hoc, P. Wadler and S. Blott. POPL'89.

Object-oriented multi-methods in Cecil, Craig Chambers. ECOOP'92.

Type classes: an exploration of the design space, Simon P. Jones, Mark Jones, Erik Meijer. Haskell'97.

Objective ML: a simple object-oriented extension of ML, Didier Rémy and Jérôme Vouillon. POPL'97.

A Calculus for Compiling and Linking Classes, Kathleen Fisher, John Reppy, and Jon G. Riecke. ESOP'00.

Introspection et reflexion

Computational reflection in class based object-oriented languages, Jacques Ferber. OOPSLA'89.

Reflection in logic, functional and object-oriented programming: a Short Comparative Study, François-Nicola Demers and Jacques Malenfant. IJCAI'95.

Reflection for Statically Typed Languages, José de Oliveira Guimares. ECOOP'98.

Programmation par aspects

A classification of pointcut language constructs, .

A typed monadic embedding of aspects, .

Aspect-oriented programming with type classes, .

Inductively Generated Pointcuts to Support Refactoring to Aspects, .

Système d'effets

A type and effect system for atomicity, Cormac Flanagan and Shaz Qadeer. PLDI'03.

Extensible effects: an alternative to monad transformers, Oleg Kiselyov, Amr Sabry, and Cameron Swords. Haskell'13.

Lightweight polymorphic effects, Lukas Rytz, Martin Odersky, and Philipp Haller. ECOOP'12.

Programmation par contrats

Contracts for higher-order functions, Robert Bruce Findler and Matthias Felleisen. ICFP'02.

Typed contracts for functional programming, Ralf Hinze, Johan Jeuring, and Andres Löh. FLOP'06.

Threesomes, with and without blame, Jeremy G. Siek and Philip Wadler. POPL'10.

Blame for all, Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. POPL'11.

Systèmes de modules

Manifest types, modules, and separate compilation, Xavier Leroy. POPL'94.

A type system for recursive modules, Derek Dreyer. ICFP'07.

Programmation probabiliste

Embedded Probabilistic Programming, Oleg Kiselyov, Chung-Chieh Shan. DSL'09.

Nonstandard interpretations of probabilistic programs for efficient inference, David Wingate, Noah Goodman, Andreas Stuhlmueller, and Jeffrey M. Siskind. NIPS'11.

Probabilistic programming, Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. FOSE'14.

Practical probabilistic programming with monads, Adam Ścibior, Zoubin Ghahramani, and Andrew D. Gordon. Haskell'15.

A lambda-calculus foundation for universal probabilistic programming, Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. ICFP'16.

Calcul réversible

What Do Reversible Programs Compute?, Holger Bock Axelsen and Robert Glück. FOSSACS'11.

Information effects, Roshan P. James and Amr Sabry. POPL'12.

Types session

Language primitives and type discipline for structured communication-based programming, Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. ESOP'98.

Haskell Session Types with (Almost) No Class, Riccardo Pucella and Jesse A. Tov. Haskell'08.

Propositions as Sessions Philip Wadler. ICFP'12.

Towards Concurrent Type Theory, .

Concurrence

CML: A higher concurrent language, John H. Reppy. PLDI'91.

Composable memory transactions, Tim Harris, Simon Marlow, Simon Peyton-Jones, and Maurice Herlihy. PPoPP'05.