IFT 6172 -- Sémantique des langages de programmation


Professeur: Stefan Monnier

English version

Page Moodle du cours pour A2023.

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. Ces articles seront choisis par les étudiants parmis les articles suggérés ci-dessous (cette liste n'est pas limitative, cependant).

Horaire et dates

Jour Heure Lieu
Lundi 14h30-16h30 B-4280 (3200, J-Brillant)
Mercredi 14h30-16h30 B-4280 (3200, J-Brillant)

Voir aussi le formulaire honteux 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.

Travail pratique

La donnée du TP (available also in English).
Le code est dans la branche tp/ift6172 du repository de Typer.

Voici aussi une présentation plus formelle de Typer Light, y compris le code source.

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

Date Personne Thème
30 oct Maud A Classification of Pointcut Language Constructs
30 oct
01 nov Julien-Charles Object-Oriented Multi-Methods in Cecil
01 nov Jerry Multi-stage programming with explicit annotations
06 nov Mathieu Eliminating Array Bound Checking Through Dependent Types
06 nov Arnaud Alias types
08 nov Cintia Principal type-schemes for functional programs
08 nov Simon Composable memory transactions
13 nov
13 nov
15 nov
15 nov Mathieu Dead Code Elimination through Dependent Types
20 nov Jerry Blame for All
20 nov Maud Is Sound Gradual Typing Dead?
22 nov Cintia Probabilistic programming
22 nov
27 nov Arnaud RustBelt: securing the foundations of the Rust programming language
27 nov Simon Sequential Programming for Replicated Data Stores
29 nov Julien-Charles A Separation Logic for Heap Space under Garbage Collection
29 nov
04 déc
06 déc Présentations/démos de projets

Food for thought

Sometimes all functions are continuous

Articles suggérés

Gestion mémoire

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.

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

A Separation Logic for Heap Space under Garbage Collection Jean-Marie Madiot, François Pottier. POPL'2022.

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.

The ins and outs of gradual type inference, Aseem Rastogi, Avik Chaudhuri, and Basil Hosmer. POPL'12.

Approximate normalization for gradual dependent types, Joseph Eremondi, Éric Tanter, and Ronald Garcia. ICFP'19.

Programmation étagée et méta-programmation

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.

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

Dependent type systems as macros, Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman. POPL'20.

Lightweight modular staging: a pragmatic approach to runtime code generation and compiled DSLs, Tiark Rompf, Martin Odersky. CACM 2012.

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.

Simple Imperative Polymorphism, Andrew K. Wright. Lisp and symbolic computation, 1995.

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.

Efficient differentiable programming in a functional array-processing language, Amir Shaikhha, Andrew W Fitzgibbon, Dimitrios Vytiniotis, Simon Peyton Jones. ICFP'19.

Symbolic and Automatic Differentiation of Languages, Conal Elliott. ICFP'21.

Types dépendants et indexés

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.

Dead Code Elimination through Dependent Types, Hongwei Xi. PADL'99.

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.

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

Objets

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.

Haskell's overlooked object system, Oleg Kyselyov, Ralf Lämmel. 2004.

Java and Scala's type systems are unsound: the existential crisis of null pointers, Nada Amin, Ross Tate. OOPSLA'2016.

Introspection et reflexion

Deriving Via or, How to Turn Hand-Written Instances into an Anti-Pattern, Baldur Blöndal, Andres Löh, Ryan Scott. Haskell 2018.

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 Logique

Logic Functional Language: From Theory to Curry, Michael Hanus, Programming Logics 2013.

Programmation par aspects

A classification of pointcut language constructs, Maximilian Stoerzer, and Stefan Hanenberg. SPLAT'05.

A typed monadic embedding of aspects, Nicolas Tabareau, Ismael Figueroa, and Éric Tanter. AOSD'13.

Aspect-oriented programming with type classes, Martin Sulzmann, and Meng Wang. FOAL'07.

Inductively Generated Pointcuts to Support Refactoring to Aspects, Tom Tourwé, Andy Kellens, Wim Vanderperren, and Frederik Vannieuwenhuyse. AOSD'04.

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.

Programming with algebraic effects and handlers, Andrej Bauer and Matija Pretnar. 2012.

The Arrow Calculus, Sam Lindley, Phil Wadler, and Jeremy Yallop. JFP'2010.

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.

Theorems for free!, Philip Wadler. ICFP'89.

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

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

Session types

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, Luís Caires, Frank Pfenning, and Bernardo Toninho. TLDI'12.

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.

Sequential Programming for Replicated Data Stores, Nicholas V. Lewchenko, Arjun Radhakrishna, Akash Gaonkar, and Pavol Černý. ICFP'19.

Normalisation et Métathéorie

System F in Agda for fun and profit, James Chapman, Roman Kireev, Chad Nester, et Philip Wadler. MPC'19.

Python: the full monty, Joe Gibbs Politz et al. OOPSLA'13.

Co-induction

Programming and reasoning with guarded recursion for coinductive types, Clouston, Ranald, et al. FoSSACS'2015.

Blockchain

Functional Blockchain Contracts, Manuel Chakravarty, et al. Unublished draft apr 2019.

Arguments implicites

On the bright side of type classes: instance arguments in Agda, Dominique Devriese, Frank Piessens. ICFP'2011.

Simplicitly: foundations and applications of implicit function types, Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki. POPL'2018.