IFT 6172 -- Sémantique des langages de programmation


Professeur: Stefan Monnier

Deuxième cours: mardi 8 Sep 2020, 12h30-14h30, https://jitsi.iro.umontreal.ca/ift6172

English version

Page Moodle du cours pour A2020.

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 Jitsi
Mardi 12h30-14h30 Jitsi

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.

Travail pratique

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

Voici aussi une présentation plus formelle de Typer, 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

Semaine du Thème
01 sep Tic Tac Types
08 sep STLC
Auxiliary material: Pierce's brick book and Pfenning's "computation and deduction"
14-15 sep STLC and Mini-ML
21-22 sep System F
28-29 sep PTS and Types dépendents
05-06 oct Idris
(Thanksgiving) 13 oct TP/Typer
19-20 oct Semaine de lecture
26-27 oct Présentations
Oct 26: How to make ad-hoc polymorphism less ad hoc, Hanneli Carolina Andreazzi
Oct 26: Slides inspired from Type-Preserving Compilation of Featherweight Java ,
Oct 27: Meta-programming With Built-in Type Equality, Antoine Doucet
Oct 27: Separation logic: A logic for shared mutable data structures, Zhong Sheng Hu
02-03 nov Présentations
Nov 2: Haskell's overlooked object system, Khalid Belharbi
Nov 2: Aspect-oriented programming with classes, Koumba Mamboundou Marie-Joëlle
Nov 3: Fortifying Macros, Samuel Yvon
Nov 3: Continuity analysis of programs, Neil Pereira
09-10 nov Nov 9: Old McDonald's singleton types et ses slides
Nov 10: Theorems for free! and Proofs for free
16-17 nov Présentations
Nov 16: Probabilistic Programming, Khalid Belharbi
Nov 16: Programming and reasoning with guarded recursion for coinductive types, Zhong Sheng Hu
Nov 17: Gradual Typing for Functional Languages, Samuel Yvon
Nov 17: Is sound gradual typing dead?, Koumba Mamboundou Marie-Joëlle
23-24 nov Présentations
Nov 23: Type reconstruction for general refinement types, Antoine Doucet
Nov 23: LiquidHaskell: experience with refinement types in the real world, Neil Pereira
Nov 24: RustBelt: securing the foundations of the rust programming language, Hanneli Carolina Andreazzi
30 nov - 01 dec
07 dec

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.

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.

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.

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.

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.

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 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.

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

Normalisation by Evaluation for Type Theory, in Type Theory, Ambrus Kaposi and Thorsten Altenkirch. LICS'2017.

Co-induction

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