Keynotes and Reports When: Tue 20 Aug 2019 09:00 - 10:00 People: Emina Torlak

… …

Research Papers When: Wed 21 Aug 2019 10:52 - 11:15 People: Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hriţcu, Exequiel Rivas, Éric Tanter

… …

miniKanren 2019 When: Thu 22 Aug 2019 10:30 - 11:15 People: Petr Lozov, Ekaterina Verbitskaia, Dmitri Boulytchev

… the interpreter returns “true” if the candidate solution satisfies all constraints …

ML 2019 When: Thu 22 Aug 2019 10:55 - 11:20 People: Oleg Kiselyov, Jeremy Yallop

… semantics of let(rec)-insertion, which does not rely on any effects at all. …

Haskell 2019 When: Thu 22 Aug 2019 13:30 - 14:00 People: Jan Christiansen, Sandra Dylus, Niels Bunkenburg

… that hold for all kinds of effects is attractive, not all propositions of interest hold for all kinds of effects. Some propositions fail for certain effects … of effects we can prove propositions for all effects that do not require …

Erlang 2019 When: Sun 18 Aug 2019 17:10 - 17:50 People: Adam Lindberg, Sébastien Merle, Peer Stritzinger

… directions together with prototype implementations that all serve the purpose …

OCaml 2019 When: Fri 23 Aug 2019 13:55 - 14:20 People: Nathan Rebours, Jeremie Dimino, Xavier Clerc, Carl Eastlund

… # The future of OCaml PPX: towards a unified and more robust ecosystem

OCaml 4.02 introduced the PPX language feature to replace Camlp4 with a more uniform way of defining language extensions that would share a syntax understood by all …

TyDe 2019 When: Sun 18 Aug 2019 15:40 - 16:00 People: Guillaume Allais

… for indexed families, all requiring minimal user input. …

TyDe 2019 When: Sun 18 Aug 2019 11:10 - 11:30 People: Sean Innes, Nicolas Wu

… all along; types are great, but in moderation. This lesson is quickly put …

HIW 2019 When: Fri 23 Aug 2019 10:30 - 10:53 People: Matthew Pickering, John Ericson

… and so on. A library consumer chooses one configuration of all these parameters … ideas about not just for the paper cuts, but also to rename and type check all …

Haskell 2019 When: Thu 22 Aug 2019 15:50 - 16:20 People: Paul Downen, Zachary Sullivan, Zena M. Ariola, Simon Peyton Jones

… ad-hoc, and do not work at all in higher-order functions. We show how …

Research Papers When: Mon 19 Aug 2019 17:13 - 17:36 People: Andrey Mokhov, Georgy Lukyanov, Simon Marlow, Jeremie Dimino

… , and all of which are declared statically. Monads extend the applicative interface … by one effect determines all subsequent effects, dynamically.

This paper …* that requires all effects to be declared statically, but provides a way to select which …

Research Papers When: Wed 21 Aug 2019 15:20 - 15:43 People: Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev

… structure of the substructural operations of Intuitionistic Linear Logic at all non … the canonical comonoid structure of all non-linear types. We also show …

Research Papers When: Mon 19 Aug 2019 16:50 - 17:13 People: Maximilian Algehed, Jean-Philippe Bernardy

… proofs of noninterference from parametricity. All our contributions have been …

Research Papers When: Tue 20 Aug 2019 16:06 - 16:30 People: Csongor Kiss, Tony Field, Susan Eisenbach, Simon Peyton Jones

… Type family applications in Haskell must be fully saturated. This means that all type-level functions have to be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension to GHC that removes …

Research Papers When: Mon 19 Aug 2019 10:30 - 10:52 People: Matthew Flatt, Caner Derici, R. Kent Dybvig, Andy Keep, Gustavo E. Massaccesi, Sarah Spall, Sam Tobin-Hochstadt, Jon Zeppieri

… We ported Racket to Chez Scheme, and it works well—as long as we’re allowed a few patches to Chez Scheme. DrRacket runs, the Racket distribution can build itself, and nearly all of the core Racket test suite passes. Maintainability …

Research Papers When: Tue 20 Aug 2019 14:37 - 15:00 People: Benjamin Sherman, Jesse Michel, Michael Carbin

… denote continuous maps, ensuring that all programs are sound and robust.

We also …

Research Papers When: Wed 21 Aug 2019 13:52 - 14:15 People: Pierre-Marie Pédrot, Nicolas Tabareau, Hans Fehrmann, Éric Tanter

… an additional translation that uses parametricity to enforce that all exceptions … is structured in three layers: (a) the exceptional layer, in which all terms can …

Research Papers When: Tue 20 Aug 2019 11:37 - 12:00 People: Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic

… , called simple symmetric lenses, including all bijective lenses, all …

Research Papers When: Wed 21 Aug 2019 11:37 - 12:00 People: Nicholas V. Lewchenko, Arjun Radhakrishna, Akash Gaonkar, Pavol Cerny

… interactions of all pairs of operations when developing or verifying them.

The key …

Research Papers When: Mon 19 Aug 2019 15:43 - 16:06 People: Andrea Vezzosi, Anders Mörtberg, Andreas Abel

… Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning …

Research Papers When: Wed 21 Aug 2019 14:15 - 14:37 People: Patrick Bahr, Christian Uldal Graulund, Rasmus Ejlers Møgelberg

… Functional reactive programming (FRP) is a paradigm for programming with signals and events, allowing the user to describe reactive programs on a high level of abstraction. For this to make sense, an FRP language must ensure that all …

Research Papers When: Mon 19 Aug 2019 13:30 - 13:52 People: Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala

… very natural and nonredundant format specifications, covering all popular network …

Tutorials When: Fri 23 Aug 2019 09:00 - 12:00Fri 23 Aug 2019 13:30 - 16:30 People: Philip Wadler

… download Agda and the textbook in advance of the course. Follow all instructions …

Research Papers When: Mon 19 Aug 2019 16:06 - 16:30 People: Joseph Eremondi, Éric Tanter, Ronald Garcia

… typechecking and satisfies all the expected properties of gradual languages. In particular …