Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Events (27 results)

Experience Report on Solving the Problem Set of SICP completely.

Scheme 2020 When: Fri 28 Aug 2020 15:00 - 15:30 People: Vladimir Nikishkin

… as the more challenging, would be to solve all of the problems it gives to the potential students.

We solve all of them, more than 350 in total (as well re-typeset …

Strongly Bounded Termination with Applications to Security and Hardware Synthesis

TyDe 2020 When: Sun 23 Aug 2020 16:00 - 16:30 People: Thomas Reynolds, William Harrison, Rohit Chadha, Gerard Allwein

… Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations …

Higher-order Programming with Effects and Handlers — without First-Class Functions

HOPE 2020 When: Sun 23 Aug 2020 12:00 - 12:45 People: Jonathan Immanuel Brachthäuser, Philipp Schuster

… and treat all functions as second-class. While Effekt supports higher-order …

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

HOPE 2020 When: Sun 23 Aug 2020 10:45 - 11:30 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

A Simple State-Machine Framework for Property-Based Testing in OCaml

OCaml 2020 When: Fri 28 Aug 2020 09:00 - 09:30 People: Jan Midtgaard

… a number concepts common to all such frameworks: state modeling, commands …

A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)

Haskell 2020 When: Fri 28 Aug 2020 11:30 - 12:00 People: Andrej Ivašković, Alan Mycroft

… We present a new type-oriented framework for writing shared memory multithreaded programs that the Haskell type system guarantees are deadlock-free. The implementation wraps all concurrent computation inside a graded monad and assumes …

Staged Sums of Products

Haskell 2020 When: Fri 28 Aug 2020 14:30 - 15:00 People: Matthew Pickering, Andres Löh, Nicolas Wu

… Generic programming libraries have historically traded efficiency in return for
convenience, and the generics-sop library is no exception.
It offers a simple, uniform, representation of all datatypes precisely as a sum
of products …

mediKanren: A System for Bio-medical Reasoning

miniKanren 2020 When: Thu 27 Aug 2020 15:30 - 15:50 People: Michael Patton, Gregory Rosenblatt, William E. Byrd, Matthew Might

… We introduce \emph{mediKanren}, a combination of miniKanren, a database describing relationships between medical concepts, and a graphical user interface (GUI) to simplify data exploration and common queries. All features of the faster …

How Can I Academia When My Brain Can't Even? Mental Health in Grad School and Beyond

PLMW @ ICFP 2020 When: Sun 23 Aug 2020 14:00 - 14:45 People: Kenny Foner

… want all listeners to be empowered to choose (either before or at any point during …

Irmin v2

OCaml 2020 When: Fri 28 Aug 2020 10:00 - 10:30 People: Clément Pascutto, Ioana Cristescu, Craig Ferguson, Thomas Gazagnaire, Romain Liautaud

… Irmin is an OCaml library for building distributed databases with the same design principles as Git. Existing Git users will find many familiar features: branching/merging, immutable causal history for all changes, and the ability …

Relational Lenses as a Library (Demo)

Haskell 2020 When: Thu 27 Aug 2020 15:00 - 15:30 People: Rudi Horn

… existing relational lenses implementation we know of ensures that all

Stan — Haskell Static Analyser

HIW 2020 When: Fri 28 Aug 2020 13:14 - 13:36 People: Dmitrii Kovanikov, Veronika Romashkina

… and detailed information about all identifiers in modules. Usage of the HIE files …

Circuit Notation Source Plugin

HIW 2020 When: Fri 28 Aug 2020 14:22 - 14:44 People: Christopher Chalmers

… . The plugin automates all of the aspects that makes the manual composition of circuits …

Types in amber

OCaml 2020 When: Fri 28 Aug 2020 13:00 - 13:30 People: Paul Steckler, Matthew Ryan

… enforces that all serialized types are marked as versioned, and that serialized types …

Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille

ICFP Program When: Wed 26 Aug 2020 11:30 - 11:45Wed 26 Aug 2020 22:30 - 22:45 People: Aaron Stump, Chris Jenkins, Stephan Spahn, Colin McDonald

… statically confirms termination of the program on all inputs. The approach uses … ensures that all programs written against this interface terminate. Standard polymorphic typing is all that is needed to check the code against the interface …

Certified double sided auction mechanisms

Student Research Competition When: Mon 24 Aug 2020 10:38 - 10:47 People: Suneel sarswat

… We introduce a formal framework for analyzing trades in financial markets. These days, all big exchanges use computer algorithms to match buy and sell … sided auction mechanisms. All the definitions and results presented in this work …

Separation Logic for Sequential Programs (Functional Pearl)

ICFP Program When: Wed 26 Aug 2020 11:15 - 11:30Wed 26 Aug 2020 22:15 - 22:30 People: Arthur Charguéraud

… Software Foundations series, with all the statement and proofs formalized …

Sealing Pointer-Based Optimizations Behind Pure Functions

ICFP Program When: Mon 24 Aug 2020 15:15 - 15:30Tue 25 Aug 2020 03:15 - 03:30 People: Daniel Selsam, Simon Hudon, Leonardo De Moura

… languages all suffer a major limitation in these domains: traversing a term requires … of term-tree sizes has proved to be both common and difficult to prevent. All

Liquid Information Flow Control

ICFP Program When: Mon 24 Aug 2020 16:15 - 16:30Tue 25 Aug 2020 04:15 - 04:30 People: Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama

… if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time. …

Type Hole Inference

Student Research Competition When: Mon 24 Aug 2020 11:04 - 11:12 People: Zhiyi Pan

… to actually fill out all of those explicit annotations, most of which …

Kinds are Calling Conventions

ICFP Program When: Wed 26 Aug 2020 16:00 - 16:15Thu 27 Aug 2020 04:00 - 04:15 People: Paul Downen, Zena M. Ariola, Simon Peyton Jones, Richard A. Eisenberg

… functions, and the evaluation order of arguments—all three of which are useful …

A theory of RPC calculi for client–server model

ICFP Program When: Tue 25 Aug 2020 11:30 - 11:41Tue 25 Aug 2020 22:30 - 22:41 People: Kwanghoon Choi, Byeong-Mo Chang

… only considers a stateless server strategy in which all server states … in the server. It cannot always correctly handle all stateful operations … style. All the existing calculi either provide only the feature of asymmetric …

Designing Hardware Systems and Accelerators with Open-Source Bluespec Haskell

Tutorials When: Sun 23 Aug 2020 14:00 - 17:30 People: Rishiyur Nikhil

… -to-memory array-sorting accelerator (all the materials for this are open-source … will publicize a web site with all the tutorial-specific materials (if you want a link a little earlier, kindly contact the instructor by email). All the materials …

Effect Handlers, Evidently

ICFP Program When: Mon 24 Aug 2020 12:45 - 13:00Mon 24 - Tue 25 Aug 2020 People: Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, Daan Leijen

… one can still express all important effects, while improving local reasoning …

Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris

ICFP Program When: Wed 26 Aug 2020 14:45 - 15:00Thu 27 Aug 2020 02:45 - 03:00 People: Paolo G. Giarrusso, Leo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers

… . The gDOT type system, its semantic model, its soundness proofs, and all

A General Approach to Define Binders Using Matching Logic

ICFP Program When: Wed 26 Aug 2020 12:15 - 12:30Wed 26 Aug 2020 23:15 - 23:30 People: Xiaohong Chen, Grigore Roşu

… matching logic definition of binders also yields models to all binders, which …

Audio, Video & Web Live Coding in Haskell

Tutorials When: Sun 23 Aug 2020 09:00 - 12:30 People: Manuel Bärenz

… have a lightning presentation (one minute each) of all the games you built … make sure that you complete all the steps until there.

Optional reading …