projet

Liste provisoire d’articles et réalisations pour le cours TAS
version du 4.10.2015

Articles (30)

conference on Programming Language Design and Implementation ( PLDI 2015) :
- Diagnosing Type Errors with Class,
  Danfeng Zhang (Cornell University), Andrew Myers (Cornell University), Dimitrios Vytiniotis (Microsoft Research Cambridge), Simon Peyton Jones (Microsoft research Cambridge)
  http://research.microsoft.com/en-US/people/dimitris/diagnosing-type-errors-draft.pdf
- KJS: A Complete Formal Semantics of JavaScript,
  Daejun Park, Andrei Stefanescu, Grigore Rosu (University of Illinois at Urbana-Champagne)
  http://fsl.cs.illinois.edu/index.php/KJS:_A_Complete_Formal_Semantics_of_JavaScript
- Type-and-Example-Directed Program Synthesis,
  Peter-Michael Osera, Steve Zdancewic (University of Pensylvania)
  http://www.cs.grinnell.edu/ osera/papers/osera-pldi-2015.pdf
Symposium on Principles of Programming Languages ( POPL 2015) :
- Integrating Linear and Dependent Types,
  Neel Krishnaswami (University of Birmingham), Pierre Pradic (ENS Lyon), Nick Benton (Microsoft Research)
  https://www.mpi-sws.org/ neelk/dlnl-paper.pdf
- Safe and Efficient Gradual Typing for TypeScript ,
  Aseem Rastogi (University of Maryland, College Park), Nikhil Swamy (Microsoft Research) , Cedric Fournet (Microsoft Research), Gavin Bierman (Oracle Labs), Panagiotis Vekris (University of California, San Diego)
  http://goto.ucsd.edu/ pvekris/docs/safets-tr.pdf
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy ,
  Gilles Barthe (IMDEA Software Institute), Marco Gaboardi (University of Dundee) ,Emilio Gallego Arias (University of Pennsylvania) , Justin Hsu (University of Pennsylvania) , Aaron Roth (University of Pennsylvania) , Pierre-Yves Strub (IMDEA Software Institute),
  http://arxiv.org/pdf/1407.6845v2)
- Principal Type Schemes for Gradual Programs,
  Ronald Garcia (University of British Columbia), Matteo Cimini (Indiana University)
  http://www.cs.ubc.ca/ rxg/ptsgp.pdf
- Dependent Information Flow Types,
  Luìsa LourenÃ§o (CITI and NOVA-LINCS / Universidade Nova de Lisboa), Luìs Caires (CITI and NOVA-LINCS / Universidade Nova de Lisboa)
  http://ctp.di.fct.unl.pt/ luisal/resources/TR-DIFT.pdf
- Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant,
  Benjamin Delaware (MIT CSAIL) , ClÃƒÂ©ment Pit-Claudel (MIT CSAIL) , Jason Gross (MIT CSAIL) , Adam Chlipala (MIT CSAIL),
  http://pit-claudel.fr/clement/papers/fiat.pdf
International Conference on Foundations of Software Science and Computation Structures ( FOSSACS 2015):
- Typing weak MSOL properties,
  Sylvain Salvati, Igor Walukiewicz,
  https://hal.archives-ouvertes.fr/hal-01061202v2/document
European Symposium on Programming ( ESOP 2015) :
- Static Analysis of Spreadsheet Applications for Type-Unsafe Operations Detection,
  Tie Cheng, Xavier Rival,
  http://www.di.ens.fr/ rival/papers/esop15-spreadsheet.pdf
- Refinement Types for Incremental Computational Complexity,
  Ezgi ÃƒÂ‡iÃƒÂ§ek, Deepak Garg, Umut Acar,
  http://www.mpi-sws.org/ dg/papers/esop15.pdf
- Automatic Static Cost Analysis for Parallel Programs,
  Jan Hoffmann, Zhong Shao, http://www.cs.cmu.edu/ janh/papers/parallelcost2014.pdf
- Witnessing (Co)datatypes,
  Jasmin Chrstian Blanchette, Andrei Popescu, Dmitriy Traytel,
  http://www21.in.tum.de/ traytel/papers/esop15-witness/wit.pdf http://www21.in.tum.de/~traytel/papers/esop15-witness/wit.pdfm
- Binding Structures as an Abstract Data Type,
  Wilmer Ricciotti,
  http://www.cs.unibo.it/ ricciott/PAPERS/onbinding.pdf
- Composite Replicated Data Types,
  Alexey Gotsman, Hongseok Yang,
  http://software.imdea.org/ gotsman/papers/compos.pdf
- Making Random Judgments, Automatically Generating Well-Typed Terms from the Definition of a Type-System,
  Burke Fetscher, Koen Claessen, MichaÃ…Â‚ PaÃ…Â‚ka, John Hughes, Robby Findler,
  http://www.eecs.northwestern.edu/ robby/pubs/papers/esop2015-fcphf.pdf
International Colloquium on Automata, Languages, and ICALP 2015) :
- Parsimonious Types and Non-uniform Computation,
  Damiano Mazza and Kazushige Terui, Ã‚Â
  https://lipn.univ-paris13.fr/ mazza/papers/Lpoly.pdf
International Conference on Functional Programming ( ICFP 2015) :
- Bounded Refinment types
  Vazou - Bakst - Jhala (San Deigo)
  https://ranjitjhala.github.io/static/bounded_refinement_types.pdf
- XQuery and Static Typing: Tackling the Problem of Backward Axes
  Pierre GenevÃƒÂ¨s, CNRS (France); Nils Gesbert, UniversitÃƒÂ© Grenoble Alpes (France)
  https://hal.inria.fr/hal-01082635v2/document
- 1ML - Core and modules united (F-ing first-class modules),
  Andreas Rossberg (Google),
  https://www.mpi-sws.org/ rossberg/1ml/1ml.pdf
- Functional Pearl: A Smart View on Datatypes,
  OCauro Jaskelioff (CIFASIS - CONICET) and Exequiel Rivas (CIFASIS - CONICET),
  http://www.fceia.unr.edu.ar/ mauro/pubs/smartviews/smartviews.pdf
- GADTs meet their match,
  Georgios Karachalias (Ghent University), Tom Schrijvers (KU Leuven), Dimitrios Vytiniotis (Microsoft Research Cambridge), and Simon Peyton Jones (Microsoft Research Cambridge),
  http://research.microsoft.com/en-us/um/people/simonpj/papers/pattern-matching/gadtpm.pdf
- Which simple types have a unique inhabitant?,
  Gabriel Scherer (INRIA) and Didier RÃƒÂ¨my (INRIA),
  http://gallium.inria.fr/ scherer/drafts/unique_stlc_sums.pdf
- Learning Refinement Types,
  He Zhu (Purdue University), Aditya V. Nori (Microsoft Research), and Suresh Jagannathan (Purdue University),
  http://research.microsoft.com/pubs/245062/icfp_my_version.pdf
Logic in Computer Science ( LICS 2015 :
- Traces for Type Soundness, Tim Disney and Cormac Flanagan,
  (http://disnetdev.com/papers/traces-for-type-soundness.pdf
conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH) ( OOPSLA/SPLASH 2015) :
- A Co-Contextual Formulation of Type Rules and its Application to Incremental Type Checking,
  Sebastian Erdweg, Oliver BraÃ„Âevac, Edlira Kuci, Matthias Krebs, Mira Mezini,
  https://www.student.informatik.tu-darmstadt.de/ xx00seba/publications/cocontextual-type-checking.pdf
- Customizable Gradual Polymorphic Effects for Scala,
  MatÃƒÂas Toro, ÃƒÂ‰ric Tanter,
  http://pleiad.dcc.uchile.cl/papers/2015/toroTanter-oopsla2015.pdf
- Static Analysis of Event-Driven Node.js JavaScript Applications,
  Magnus Madsen, Frank Tip, OndÃ…Â™ej LhotÃƒÂ¡k
  http://plg.uwaterloo.ca/ mmadsen/papers/oopsla15/paper.pdf
- Probability Type Inference for Flexible Approximate Programming,
  Brett Boston, Adrian Sampson, Dan Grossman, Luis Ceze,
  https://homes.cs.washington.edu/ luisceze/publications/decaf-oopsla2015.pdf

Réalisations (6 * 2)

une application Web ou une application d’inférence de types nullables suivant le système de types proposé dans les articles : OCAML Workshop 2014 ou JFLA 2015 résumé étendu
- en utilisant ocaml (js_of_ocaml)
- ou en Haskell ou Scala
une application Web ou une applet/application de vérification dâ€™un type pour un lambda-terme (lambda-calcul simplement typé) avec construction de lâ€™arbre de preuve (avec Let et schémas de types pour le polymorphisme paramÃ©trique).
- en OCaml (avec js_of_ocaml)
- avec Swift ou Haskell
une application Web ou une applet/application d’Ã©valuation de lambda-calcul avec la représentation Alligator Eggs
- en ocaml (js_of_ocaml) ou F#
- en Scala
une extension objet avec sous-typage structurel (pour le typeur) dans un mini-ML : langage libre
- ocaml, F#, Scala, Haskell, Swift
il pourra avoir des variations, mais ce sera globalement pour traiter du sous-typage structurel avec polymorphisme de rangÃ©es
une application de simulation de lâ€™infÃ©rence de types du polymorphisme bornÃ© des gÃ©nÃ©riques pour un mini java (langage libre)
- ocaml, F#, Scala, Haskell, Swift
Si vous voulez proposer dâ€™autres langages fonctionnels pour lâ€™implantation de votre réalisation, comme Haskell, vous pouvez le demander à l’équipe enseignante.

Ce document a été traduit de L^AT_EX par H^EV^EA