Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Events (25 results)

Solver-Aided Programming for All

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

… …

Dijkstra Monads for All

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

… …

Relational Interpreters for Search Problems

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 …

let (rec) insertion without effects, lights or magic

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

Verifying Effectful Haskell Programs in Coq

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 …

Scaling Erlang Distribution

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 …

Tic Tac Types (Functional Pearl)

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 …

Generic Level Polymorphic N-ary Functions

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

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

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

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

Configuration, but without CPP

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

Making a Faster Curry with Extensional Types

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 …

Selective Applicative Functors

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 …

Mixed Linear and Non-linear Recursive Types

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 …

Simple Noninterference from Parametricity

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 …

Higher-order Type-level Programming in Haskell

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 …

Rebuilding Racket on Chez Scheme (Experience Report)

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 …

Sound and robust solid modeling via exact real arithmetic and continuity

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 …

Synthesizing Symmetric Lenses

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

A Reasonably Exceptional Type Theory

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 …

Sequential Programming for Replicated Data Stores

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 …

Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks

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

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types

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 …

Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats

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 …

Programming Language Foundations in Agda

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 …

Approximate Normalization for Gradual Dependent Types

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 …