Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 18 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:20 | Interaction and ApplicationsTyDe at Aurora Borealis Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford | ||
09:00 20mTalk | Flexible Structure Editing of Well-Typed Expressions TyDe Pre-print | ||
09:20 20mTalk | Livelits: Filling Typed Holes with Live GUIs TyDe Cyrus Omar University of Chicago, Nick Collins University of Chicago, David Moon , Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago Pre-print | ||
09:40 20mTalk | Formal Investigation of the Extended UTxO Model TyDe Orestis Melkonian Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag I/O & IOHK Pre-print | ||
10:00 20mTalk | An Algebra of Sequential Decision Problems TyDe Pre-print | ||
09:00 - 10:20 | |||
09:00 60mTalk | Morning Keynote Scheme Edwin Brady University of St. Andrews, UK | ||
09:00 - 10:20 | |||
09:00 60mTalk | Keynote FHPNC Trevor L. McDonell Utrecht University | ||
10:00 10mTalk | GSoC Student Report 1 FHPNC | ||
10:10 10mTalk | GSoC Student Report 2 FHPNC Jesse Sigal University of Edinburgh | ||
09:00 - 10:20 | |||
09:00 10mDay opening | Welcome PLMW @ ICFP David Van Horn University of Maryland, USA | ||
09:10 35mTalk | Effect handler oriented programming PLMW @ ICFP Sam Lindley The University of Edinburgh and Imperial College London | ||
09:45 35mTalk | Types and verification PLMW @ ICFP Niki Vazou IMDEA Software Institute | ||
09:00 - 10:20 | |||
09:00 20mDay opening | Opening Erlang | ||
09:20 60mTalk | Introduction to the Erlang Ecosystem Foundation Erlang Peer Stritzinger Peer Stritzinger GmbH | ||
10:50 - 12:10 | Dependently Typed ProgrammingTyDe at Aurora Borealis Chair(s): William J. Bowman University of British Columbia | ||
10:50 20mTalk | Syntax with Shifted Names TyDe Pre-print | ||
11:10 20mTalk | Tic Tac Types (Functional Pearl) TyDe Link to publication | ||
11:30 20mTalk | Monadic typed tactic programming by reflection TyDe Liang-Ting Chen Swansea University Pre-print | ||
11:50 20mTalk | Deferring the Details and Deriving Programs TyDe Liam O'Connor UNSW Link to publication | ||
10:50 - 12:10 | |||
10:30 30mTalk | Syntax Templates In Racket Scheme Ryan Culpepper Czech Technical University | ||
11:00 30mTalk | Visualizing Abstract Abstract Machines Scheme Kyle Headley The University of Alabama at Birmingham | ||
11:30 30mTalk | gLua: A modern Lua transpiler in Scheme Scheme | ||
10:50 - 12:10 | |||
10:50 26mTalk | Generating Efficient FFT GPU Code with Lift FHPNC Link to publication DOI Pre-print File Attached | ||
11:16 26mTalk | Lazy Evaluation in Infinite-Dimensional Function Spaces with Wavelet Basis FHPNC Link to publication Pre-print | ||
11:43 26mTalk | Functional Approach to Acceleration of Monte Carlo Simulation for American Option Pricing (extended abstract) FHPNC Wojciech Michal Pawlak University of Copenhagen, Denmark, Martin Elsman University of Copenhagen, Denmark, Cosmin Oancea University of Copenhagen, Denmark Link to publication | ||
10:50 - 12:10 | |||
10:50 40mTalk | Managing your research, your advisor, your PhD PLMW @ ICFP Amal Ahmed Northeastern University, USA | ||
11:30 40mTalk | Time management, family, and quality of life PLMW @ ICFP Kathleen Fisher Tufts University, USA | ||
10:50 - 12:10 | |||
10:50 40mFull-paper | Gaining Trust by Tracing Security Protocols Erlang Lars-Ake Fredlund , Thomas Arts Quviq, Clara Benac Earle Universidad Politécnica de Madrid, Hans Svensson Quviq AB | ||
11:30 40mFull-paper | Runtime Type Safety for Erlang/OTP Behaviours Erlang Joseph Harrison University of Kent, UK | ||
12:00 - 13:30 | |||
12:00 90mLunch | Lunch Catering | ||
13:40 - 14:50 | Invited Talk and MetatheoryTyDe at Aurora Borealis Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford | ||
13:40 50mTalk | Cubes, Cats, Effects TyDe | ||
14:30 20mTalk | Inductive types deconstructed TyDe Stefan Monnier Université de Montréal Link to publication | ||
13:40 - 14:50 | |||
14:00 20mTalk | Lightning talk: Commanding Emacs from Coq Scheme Joomy Korkut Princeton University, USA | ||
14:20 20mTalk | Reigniting Fuse, an Online Partial Evaluator for Scheme Scheme Paulette Koronkevich University of British Columbia | ||
14:40 20mTalk | SRFI-167, SRFI-168 and the functional store Scheme | ||
13:40 - 14:50 | |||
13:40 23mTalk | Compositional Deep Learning in Futhark FHPNC Duc Minh Tran DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Denmark, Martin Elsman University of Copenhagen, Denmark Link to publication | ||
14:03 23mTalk | Towards Hasktorch 1.0: Automated Generation of C++ Libtorch Bindings (extended abstract) FHPNC | ||
14:26 23mTalk | Hailstorm : A statically typed functional language for systems programming (extended abstract) FHPNC | ||
13:40 - 14:50 | |||
13:40 35mTalk | Functional Programming is Everywhere PLMW @ ICFP Ilya Sergey Yale-NUS College and National University of Singapore | ||
14:15 35mTalk | How to give talks that people can follow PLMW @ ICFP Derek Dreyer MPI-SWS | ||
13:40 - 14:50 | |||
13:40 23mShort-paper | Lux - an expect like test tool written in Erlang Erlang | ||
14:03 23mShort-paper | Towards Online Profiling of Erlang Systems Erlang | ||
14:26 24mShort-paper | Tools supporting green computing in Erlang Erlang Gergely Nagy Eötvös Lóránd University, Áron Attila Mészáros Eötvös Lóránd University, István Bozó Eötvös Loránd University, Melinda Tóth Eötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd. | ||
15:20 - 16:40 | Generic Programming and SynthesisTyDe at Aurora Borealis Chair(s): Edwin Brady University of St. Andrews, UK | ||
15:20 20mTalk | Generic Enumerators TyDe Cas van der Rest Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag I/O & IOHK Pre-print | ||
15:40 20mTalk | Generic Level Polymorphic N-ary Functions TyDe Guillaume Allais University of Strathclyde Link to publication | ||
16:00 20mTalk | Augmenting Type Signatures for Program Synthesis TyDe Pre-print | ||
16:20 20mTalk | Constraint-based Type-directed Program Synthesis TyDe Peter-Michael Osera Grinnell College Link to publication | ||
15:20 - 16:40 | |||
15:30 30mTalk | Scheme Macros for Non-linear Pattern Matching with Backtracking for Non-free Data Types Scheme Satoshi Egi Rakuten Institute of Technology | ||
16:00 30mTalk | Stack-Liberated Abstract Garbage Collection Scheme | ||
15:20 - 16:40 | ArraysFHPNC at Reindeer Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital | ||
15:20 25mTalk | Compiling Generalised Histograms for GPU (extended abstract) FHPNC Sune Hellfritzsch University of Copenhagen, Niels G. W. Serup DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Denmark, Cosmin Oancea University of Copenhagen, Denmark | ||
15:46 26mTalk | Position-Dependent Arrays and Their Applicationfor High Performance Code Generation FHPNC Federico Pizzuti University of Edinburgh, Michel Steuwer University of Glasgow, Christophe Dubach University of Edinburgh Link to publication DOI Pre-print File Attached | ||
16:14 26mTalk | Safety at speed: In-place array algorithms from pure functional programs by safely re-using storage FHPNC Markus Aronsson , Koen Claessen Chalmers University of Technology, Mary Sheeran , Nicholas Smallbone Chalmers University of Technology, Sweden | ||
15:20 - 16:40 | |||
15:20 80mTalk | Social activity PLMW @ ICFP | ||
15:20 - 16:40 | |||
15:20 40mFull-paper | Erlang as an enabling technology for resilient general-purpose applications on edge IoT networks Erlang | ||
16:00 40mFull-paper | Intro to Web Prolog for Erlangers Erlang Torbjörn Lager Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg | ||
17:10 - 18:10 | |||
17:10 20mTalk | Reasoning about Effect Parametricity Using Dependent Types TyDe Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel Pre-print | ||
17:30 20mTalk | How to do proofs? Practically proving properties about effectful programs' results (functional pearl) TyDe Koen Jacobs KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel Link to publication | ||
17:10 - 18:10 | |||
17:10 60mTalk | Afternoon Keynote Scheme Andy Keep Cisco Systems, Inc | ||
17:10 - 18:10 | |||
17:10 60mTalk | Formal Verification of Scientific Computing Programs FHPNC Micaela Mayero LIPN, Université Paris 13 | ||
17:10 - 18:10 | |||
17:10 60mTalk | Panel Discussion: Research in Functional Programming PLMW @ ICFP Simon Peyton Jones Microsoft, UK, Satnam Singh Google Research, Zoe Paraskevopoulou Princeton University, Jeremy Gibbons Department of Computer Science, University of Oxford, Andrey Mokhov Newcastle University, UK, Amal Ahmed Northeastern University, USA | ||
17:10 - 18:10 | |||
17:10 40mFull-paper | Scaling Erlang Distribution Erlang Adam Lindberg Peer Stritzinger GmbH, Sébastien Merle Peer Stritzinger GmbH, Peer Stritzinger Peer Stritzinger GmbH | ||
17:50 20mDay closing | Closing Erlang | ||
18:10 - 19:10 | |||
18:10 60mSocial Event | Happy Hour Catering | ||
Mon 19 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 19 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Blockchains are functional Keynotes and Reports Manuel Chakravarty Tweag I/O & IOHK | ||
10:30 - 12:00 | Compilation & ParallelismResearch Papers at Aurora Borealis Chair(s): Michael D. Adams University of Michigan | ||
10:30 22mTalk | Rebuilding Racket on Chez Scheme (Experience Report) Research Papers Matthew Flatt University of Utah, Caner Derici Indiana University, R. Kent Dybvig Cisco Systems, Inc, Andy Keep Cisco Systems, Inc, Gustavo E. Massaccesi Universidad de Buenos Aires, Sarah Spall Indiana University, Sam Tobin-Hochstadt Indiana University, Jon Zeppieri Link to publication DOI | ||
10:52 22mTalk | Compiling with Continuations, or without? Whatever. Research Papers Youyou Cong Tokyo Institute of Technology, Leo Osvald Purdue University, USA, Gregory Essertel Purdue University, Tiark Rompf Purdue University | ||
11:15 22mTalk | Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning Research Papers Akimasa Morihata University of Tokyo | ||
11:37 22mTalk | Fairness in Responsive Parallelism Research Papers Stefan K. Muller Carnegie Mellon University, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University | ||
12:00 - 13:30 | |||
13:30 - 15:00 | |||
13:30 22mTalk | Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats Research Papers Benjamin Delaware Purdue University, Sorawit Suriyakarn , Clément Pit-Claudel MIT CSAIL, Qianchuan Ye Purdue University, Adam Chlipala Massachusetts Institute of Technology Link to publication DOI Authorizer link | ||
13:52 22mTalk | Closure Conversion is Safe for Space Research Papers | ||
14:15 22mTalk | Linear capabilities for fully abstract compilation of separation-logic-verified code Research Papers Thomas Van Strydonck KULeuven, Frank Piessens KU Leuven, Dominique Devriese Vrije Universiteit Brussel | ||
14:37 22mTalk | The Next 700 Compiler Correctness Theorems. A Functional Pearl. Research Papers | ||
15:20 - 16:30 | |||
15:20 23mTalk | Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq Research Papers | ||
15:43 23mTalk | Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive TypesDistinguished Paper Research Papers Andrea Vezzosi Chalmers University of Technology, Anders Mörtberg Department of Mathematics, Stockholm University, Andreas Abel Gothenburg University | ||
16:06 23mTalk | Approximate Normalization for Gradual Dependent Types Research Papers Joseph Eremondi University of British Columbia, Éric Tanter University of Chile & Inria Paris, Ronald Garcia University of British Columbia Pre-print | ||
16:50 - 18:00 | |||
16:50 23mTalk | Simple Noninterference from Parametricity Research Papers Maximilian Algehed Chalmers University of Technology, Sweden, Jean-Philippe Bernardy University of Gothenburg | ||
17:13 23mTalk | Selective Applicative Functors Research Papers Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Simon Marlow Facebook, Jeremie Dimino Jane Street Europe Link to publication | ||
17:36 23mTalk | Coherence of Type Class Resolution Research Papers Gert-Jan Bottu KU Leuven, Ningning Xie University of Toronto, Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven | ||
18:00 - 20:00 | |||
18:00 2hPoster | SRC Poster Session Student Research Competition | ||
Tue 20 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 20 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Solver-Aided Programming for All Keynotes and Reports Emina Torlak University of Washington | ||
10:30 - 12:00 | Program Analysis & SynthesisResearch Papers at Aurora Borealis Chair(s): Daniel Winograd-Cort Target Corp | ||
10:30 22mTalk | Relational Cost Analysis for Functional-Imperative Programs Research Papers Weihao Qu University at Buffalo, SUNY, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems | ||
10:52 22mTalk | Fuzzi: A Three-Level Logic for Differential Privacy Research Papers Hengchu Zhang University of Pennsylvania, Edo Roth University of Pennsylvania, Andreas Haeberlen University of Pennsylvania, USA, Benjamin C. Pierce University of Pennsylvania, Aaron Roth University of Pennsylvania, USA | ||
11:15 22mTalk | Synthesizing Differentially Private Programs Research Papers | ||
11:37 22mTalk | Synthesizing Symmetric Lenses Research Papers Anders Miltner Princeton University, Solomon Maina University of Pennsylvania, Kathleen Fisher Tufts University, USA, Benjamin C. Pierce University of Pennsylvania, David Walker Princeton University, Steve Zdancewic University of Pennsylvania Pre-print | ||
12:00 - 13:30 | |||
15:20 - 16:30 | Dependent Types in HaskellResearch Papers at Aurora Borealis Chair(s): Joachim Breitner DFINITY Foundation | ||
15:20 23mTalk | Dependently Typed Haskell in Industry (Experience Report) Research Papers David Thrane Christiansen Galois, USA, Iavor Diatchki Galois, Inc., Robert Dockins Galois, Inc., Joe Hendrix Galois, Inc., Tristan Ravitch Galois, Inc. | ||
15:43 23mTalk | A Role for Dependent Types in Haskell Research Papers Stephanie Weirich University of Pennsylvania, USA, Pritam Choudhury University of Pennsylvania, Antoine Voizard University of Pennsylvannia, Richard A. Eisenberg Bryn Mawr College, USA | ||
16:06 23mTalk | Higher-order Type-level Programming in Haskell Research Papers Csongor Kiss Imperial College London, Tony Field Imperial College London, Susan Eisenbach Imperial College London, Simon Peyton Jones Microsoft, UK | ||
16:50 - 18:15 | |||
16:50 40mTalk | SRC Finalist Presentation Student Research Competition | ||
17:30 15mAwards | SIGPLAN Awards Keynotes and Reports | ||
17:45 30mAwards | Programming Contest Report Keynotes and Reports Ilya Sergey Yale-NUS College and National University of Singapore | ||
18:15 - 19:15 | |||
Wed 21 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 21 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Derivations as computations Keynotes and Reports Andrej Bauer University of Ljubljana | ||
10:30 - 12:00 | Program VerificationResearch Papers at Aurora Borealis Chair(s): Adam Chlipala Massachusetts Institute of Technology | ||
10:30 22mTalk | A predicate transformer semantics for effects (Functional Pearl) Research Papers | ||
10:52 22mTalk | Dijkstra Monads for All Research Papers Kenji Maillard Inria Paris and ENS Paris, Danel Ahman University of Ljubljana, Robert Atkey University of Strathclyde, Guido Martínez CIFASIS-CONICET, Argentina, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Éric Tanter University of Chile & Inria Paris Pre-print | ||
11:15 22mTalk | Mechanized Relational Verification of Concurrent Programs with Continuations Research Papers | ||
11:37 22mTalk | Sequential Programming for Replicated Data Stores Research Papers Nicholas V. Lewchenko University of Colorado Boulder, Arjun Radhakrishna Microsoft, Akash Gaonkar , Pavol Cerny University of Colorado Boulder DOI Pre-print | ||
12:00 - 13:30 | |||
13:30 - 15:00 | Modal TypesResearch Papers at Aurora Borealis Chair(s): Dominique Devriese Vrije Universiteit Brussel | ||
13:30 22mTalk | Implementing a Modal Dependent Type TheoryDistinguished Paper Research Papers Daniel Gratzer Aarhus University, Jonathan Sterling Carnegie Mellon University, Lars Birkedal Aarhus University | ||
13:52 22mTalk | A Reasonably Exceptional Type Theory Research Papers Pierre-Marie Pédrot INRIA, Nicolas Tabareau Inria, Hans Fehrmann University of Chile, Éric Tanter University of Chile & Inria Paris | ||
14:15 22mTalk | Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks Research Papers Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen | ||
14:37 22mTalk | Quantitative program reasoning with graded modal types Research Papers Dominic Orchard University of Kent, UK, Vilem-Benjamin Liepelt University of Kent, UK, Harley D. Eades III Augusta University Pre-print | ||
15:20 - 16:30 | |||
15:20 23mTalk | Mixed Linear and Non-linear Recursive Types Research Papers | ||
15:43 23mTalk | A Mechanical Formalization of Higher-Ranked Polymorphic Type InferenceDistinguished Paper Research Papers Zhao Jinxu , Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven | ||
16:06 23mTalk | An Efficient Algorithm for Type-Safe Structural Diffing Research Papers Victor Cacciari Miraldo Utrecht University, Netherlands, Wouter Swierstra Utrecht University, Netherlands | ||
16:50 - 18:00 | Lambda-Calculus & TeachingResearch Papers at Aurora Borealis Chair(s): Jonathan Protzenko Microsoft Research, Redmond | ||
16:50 23mTalk | Call-By-Need is Clairvoyant Call-By-Value Research Papers | ||
17:13 23mTalk | Teaching the Art of Functional Programming Using Automated Grading (Experience Report) Research Papers | ||
17:36 23mTalk | Lambda: the Ultimate Sublanguage (Experience Report) Research Papers DOI Pre-print | ||
18:00 - 18:30 | |||
18:00 10mAwards | SRC Awards Presentation Student Research Competition | ||
18:10 15mTalk | Program Chair's Report Keynotes and Reports François Pottier Inria, France | ||
18:25 5mTalk | ICFP 2020 Announcement Keynotes and Reports | ||
18:30 - 19:30 | |||
Thu 22 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 22 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Gender equality in academia: meeting the challenge Haskell File Attached | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Fine-grained program reasoning using linear and graded modal types Tutorials Harley D. Eades III Augusta University, Dominic Orchard University of Kent, UK, Vilem-Benjamin Liepelt University of Kent, UK | ||
09:00 - 10:00 | |||
09:00 60mTutorial | Tutorial on miniKanren miniKanren William E. Byrd University of Alabama at Birmingham, USA | ||
09:00 - 10:00 | |||
09:00 60mTalk | Keynote: An Introduction to the Imandra Automated Reasoning System ML | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Verifying Imperative Programs with SAW Tutorials | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Functional Software Architecture Tutorials Michael Sperber Active Group GmbH | ||
10:30 - 12:00 | |||
10:30 30mResearch paper | Bidirectional Type Class Instances Haskell Koen Pauwels KU Leuven, Georgios Karachalias KU Leuven, Belgium, Michiel Derhaeg Guardsquare, Tom Schrijvers KU Leuven | ||
11:00 30mResearch paper | Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances Haskell Pre-print File Attached | ||
11:30 30mResearch paper | Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the μVeriFast verifier as a case study Haskell Dominique Devriese Vrije Universiteit Brussel File Attached | ||
10:30 - 12:00 | |||
10:30 45mFull-paper | Relational Interpreters for Search Problems miniKanren Petr Lozov Sain Petersburg State University, SPbGU, Ekaterina Verbitskaia Saint Petersburg State University, Russia, Dmitri Boulytchev Link to publication | ||
11:15 45mFull-paper | Relational Processing for Fun and Diversity: Simulating a CPU relationally with miniKanren miniKanren Link to publication | ||
10:30 - 12:00 | |||
10:30 25mTalk | A right-to-left type system for value recursion ML Pre-print | ||
10:55 25mTalk | let (rec) insertion without effects, lights or magic ML Pre-print | ||
11:20 25mTalk | (TyDe Presentation) FreezeML: Complete and Easy Type Inference for First-Class Polymorphism ML Frank Emrich The University of Edinburgh, Sam Lindley The University of Edinburgh and Imperial College London, Jan Stolarek University of Edinburgh, UK, James Cheney University of Edinburgh, UK | ||
11:20 - 11:45 | |||
11:20 25mTalk | FreezeML: Complete and Easy Type Inference for First-Class Polymorphism TyDe Frank Emrich The University of Edinburgh, Sam Lindley The University of Edinburgh and Imperial College London, Jan Stolarek University of Edinburgh, UK, James Cheney University of Edinburgh, UK Pre-print | ||
12:00 - 13:30 | |||
13:30 - 15:00 | Paper Session 2: VerificationHaskell at Aurora Borealis Chair(s): Ningning Xie University of Toronto | ||
13:30 30mResearch paper | Verifying Effectful Haskell Programs in Coq Haskell Jan Christiansen Flensburg University of Applied Sciences, Germany, Sandra Dylus University of Kiel, Germany, Niels Bunkenburg University of Kiel, Germany | ||
14:00 30mTalk | Solving Haskell equality constraints using Coq Haskell File Attached | ||
14:30 30mExperience report | Formal Verification of Spacecraft Control Programs: An Experience Report Haskell Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Jakob Lechner RUAG Space Austria GmbH | ||
13:30 - 16:30 | |||
13:30 3hTutorial | Make your ETL pipeline with DataHaskell, JSON AutoType and XML TypeLift Tutorials | ||
13:30 - 15:00 | |||
13:30 45mFull-paper | Certified Semantics for miniKanren miniKanren Link to publication | ||
14:15 45mFull-paper | Constructive Negation for miniKanren miniKanren Link to publication | ||
13:30 - 15:00 | |||
13:30 25mTalk | Transparent Synchronous Dataflow ML Steven Cheung University of Birmingham, UK File Attached | ||
13:55 25mTalk | Programming with Rational Coinductive Streams ML Jean-Baptiste Jeannin University of Michigan, USA File Attached | ||
14:20 25mTalk | Efficient Deconstruction with Typed Pointer Reversal ML Pre-print | ||
13:30 - 16:30 | |||
13:30 3hTutorial | Verifying Imperative Programs with SAW Tutorials | ||
13:30 - 16:30 | |||
13:30 3hTutorial | Teaching functional programming Tutorials Michael Sperber Active Group GmbH | ||
15:20 - 16:30 | |||
15:20 30mResearch paper | G2Q: Haskell Constraint Solving Haskell | ||
15:50 30mTalk | Making a Faster Curry with Extensional Types Haskell Paul Downen University of Oregon, USA, Zachary Sullivan , Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK | ||
15:20 - 16:30 | |||
15:20 35mFull-paper | First-order miniKanren representation: Great for tooling and search miniKanren Gregory Rosenblatt , Lisa Zhang University of Toronto, William E. Byrd University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School Link to publication | ||
15:55 35mFull-paper | Towards a miniKanren with fair search strategies miniKanren Link to publication | ||
15:20 - 16:30 | |||
15:20 25mTalk | An Idris Foreign Function Interface to OCaml ML File Attached | ||
15:45 25mTalk | Necro: Animating Skeletons ML File Attached | ||
16:50 - 18:15 | Paper Session 4: MetaprogrammingHaskell at Aurora Borealis Chair(s): Christiaan Baaij QBayLogic B.V. | ||
16:50 30mResearch paper | Multi-Stage Programs in Context Haskell Matthew Pickering University of Bristol, Nicolas Wu Imperial College London, Csongor Kiss Imperial College London | ||
17:20 30mResearch paper | Working with Source Plugins Haskell Matthew Pickering University of Bristol, Nicolas Wu Imperial College London, Boldizsár Németh Eötvös Loránd University | ||
17:50 10mOther | PC Chair Report Haskell Richard A. Eisenberg Bryn Mawr College, USA | ||
16:50 - 18:15 | |||
16:50 85mSocial Event | Q&A with audience miniKanren | ||
16:50 - 18:15 | |||
16:50 25mTalk | Compiling Successor ML Pattern Guards ML Pre-print | ||
17:15 25mTalk | A Key-Value store for OCaml ML Tom Ridge University of Leicester, UK File Attached | ||
17:40 25mTalk | Towards Machine Learning Induction in Poly/ML ML Yutaka Nagashima Data61, Australia File Attached | ||
18:15 - 20:15 | |||
18:15 2hSocial Event | Industrial Reception Catering | ||
Fri 23 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Fri 23 Aug
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Haskell Use and Abuse at Scale Haskell | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Folding/Unfolding with Scala Tutorials | ||
09:00 - 10:00 | |||
09:00 60mTalk | Haskell Use and Abuse at Scale HIW | ||
09:00 - 10:00 | |||
09:00 5mDay opening | Welcome OCaml David Allsopp University of Cambridge | ||
09:05 25mTalk | Invited Talk OCaml Xavier Leroy Collège de France | ||
09:30 30mTalk | The OCaml Platform in 2019 OCaml | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Programming Language Foundations in Agda Tutorials Philip Wadler University of Edinburgh, UK | ||
09:00 - 10:00 | |||
09:10 30mTalk | Csound-expression: Haskell framework for computer music FARM Anton Kholomiov HXR team | ||
09:40 30mTalk | Screaming in the IO monad FARM David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University | ||
09:00 - 12:00 | |||
09:00 3hTutorial | Building C++ project with Shake Tutorials | ||
10:30 - 12:00 | |||
10:30 30mResearch paper | STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism Haskell Sebastian Ertel , Justus Adam Technische Universität Dresden, Norman A. Rink TU Dresden, Germany, Andrés Goens , Jeronimo Castrillon TU Dresden, Germany | ||
11:00 30mResearch paper | Synthesizing Functional Reactive Programs Haskell Bernd Finkbeiner , Felix Klein Saarland University, Ruzica Piskac Yale University, USA, Mark Santolucito Yale University, USA | ||
11:30 30mTalk | The essence of live coding: Change the program, keep the state! Haskell Manuel Bärenz sonnen eServices GmbH File Attached | ||
10:30 - 12:00 | |||
10:30 23mTalk | Configuration, but without CPP HIW | ||
10:53 23mTalk | HIE files in GHC 8.8 HIW | ||
11:16 24mTalk | Tagging Tags: Inferring the presence of pointer tags at compile time. HIW | ||
11:40 20mTalk | Lightning talks Slot #1 HIW | ||
10:30 - 12:00 | |||
10:30 25mTalk | OwlDE: making ODEs first-class Owl citizens OCaml Marcello Seri Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen, Ta-Chu Kao Computational and Biological Learning Lab, Department of Engineering, University of Cambridge | ||
10:55 25mTalk | CausalRPC: traceable distributed computation OCaml Craig Ferguson Tarides | ||
11:20 25mTalk | Executing Owl Computation on GPU and TPU OCaml Jianxin Zhao University of Cambridge | ||
10:30 - 12:00 | Music GenerationFARM at Stockholm Chair(s): David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University | ||
10:30 30mTalk | Music as Language: Putting Probabilistic Temporal Graph Grammars to Good Use FARM Orestis Melkonian Utrecht University | ||
11:00 30mTalk | A Functional Model of Jazz Improvisation FARM | ||
11:30 30mTalk | Demo: Counterpoint by Construction FARM | ||
12:00 - 13:30 | |||
13:30 - 15:00 | |||
13:30 30mResearch paper | Monad Transformers and Modular Algebraic Effects: What Binds Them Together Haskell Tom Schrijvers KU Leuven, Maciej Piróg University of Wrocław, Nicolas Wu Imperial College London, Mauro Jaskelioff CONICET, Argentina | ||
14:00 30mResearch paper | Scoping Monadic Relational Database Queries Haskell Anton Ekblad Chalmers University of Technology | ||
13:30 - 15:00 | |||
13:30 23mTalk | Status Update on the Helium for Haskell compiler HIW Jurriaan Hage Utrecht University, Netherlands | ||
13:53 23mTalk | The Gibbon Compiler: Accelerating a small subset of Haskell HIW Ryan R. Newton Indiana University, Michael Vollmer Indiana University, USA, Chaitanya S. Koparkar Indiana University | ||
14:16 24mTalk | Copilot 3.0: a Haskell runtime verification framework for UAVs HIW Frank Dedden Royal Netherlands Aerospace Center, Alwyn Goodloe NASA Langley Research Center, Ivan Perez NIA / NASA Formal Methods | ||
14:40 20mTalk | Lightning talks Slot #2 HIW | ||
13:30 - 15:00 | |||
13:30 25mTalk | Codept, a whole-project dependency analyzer for OCaml OCaml | ||
13:55 25mTalk | The future of OCaml PPX: towards a unified and more robust ecosystem OCaml Nathan Rebours Tarides, Jeremie Dimino Jane Street Europe, Xavier Clerc ocamljava.org, Carl Eastlund Jane Street Europe | ||
14:20 25mTalk | Benchmarking the OCaml compiler: our experience OCaml Tom Kelly OCaml Labs | ||
13:30 - 16:30 | |||
13:30 3hTutorial | Programming Language Foundations in Agda Tutorials Philip Wadler University of Edinburgh, UK | ||
13:30 - 15:00 | |||
13:30 30mTalk | Fun with Interfaces (SVG Interfaces for Musical Expression) FARM Benedict R. Gaster University of the West of England, Nathan Renney University of West of England, Carinna Parraman University of West of England | ||
14:00 30mTalk | Mobile Game Programming in Haskell FARM | ||
14:30 30mTalk | Demo: Kaleidogen FARM Joachim Breitner DFINITY Foundation | ||
13:30 - 16:30 | |||
13:30 3hTutorial | Write you a mini-GRIN, a unified compiler back-end for lazy and strict FP languages. Tutorials | ||
15:20 - 16:30 | |||
15:20 23mTalk | HoleFitPlugins and the future of interactive development in GHC HIW Matthías Páll Gissurarson Chalmers University of Technology, Sweden | ||
15:43 23mTalk | Explicit Dictionary Applications - From Theory to Practice? HIW Dominique Devriese Vrije Universiteit Brussel File Attached | ||
16:06 23mTalk | Visible dependent quantification HIW Ryan Scott Indiana University at Bloomington, USA File Attached | ||
15:20 - 16:50 | |||
15:20 25mTalk | Lessons from building a succinct blockchain with OCaml OCaml Nathan Holland O(1) Labs | ||
15:45 25mTalk | Makecloud: Simple, Fast, Robust CI/CD for the modern era OCaml | ||
16:10 25mTalk | MirageOS 4: the dawn of practical build systems for exotic targets OCaml Lucas Pluvinage ENS Paris, Romain Calascibetta Tarides, Rudi Grinberg OCaml Labs, Anil Madhavapeddy OCaml Labs | ||
15:20 - 16:30 | |||
15:30 30mDemonstration | Demo: Functors and Music FARM Heinrich Apfelmus independent DOI | ||
16:00 30mTalk | The sound of lambda FARM | ||
16:50 - 18:00 | |||
16:50 2mDay closing | HiW'19 report HIW Niki Vazou IMDEA Software Institute | ||
16:52 23mTalk | GHC status report HIW Simon Peyton Jones Microsoft, UK | ||
17:15 45mOther | Panel Discussion HIW | ||
16:50 - 18:00 | |||
16:50 30mTalk | Analyzing Music with Prefix Trees FARM Yan Han University of Cambridge, Nada Amin Harvard University, Neel Krishnaswami Computer Laboratory, University of Cambridge | ||
17:20 30mTalk | What Constitutes a Musical Pattern? FARM Orestis Melkonian Utrecht University, Iris Yuping Ren Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Anja Volk Utrecht University | ||