Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 23 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Sun 23 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 60mTalk | A preview of a tutorial on L (polarized μμ̃) HOPE Kenji Maillard Inria Paris and ENS Paris, Étienne Miquey INRIA, Xavier Montillet INRIA, Guillaume Munch-Maccagnoni Inria, Gabriel Scherer INRIA Saclay | ||
09:00 - 10:00 | |||
09:00 5mDay opening | Welcome to HIW HIW Joachim Breitner DFINITY Foundation | ||
09:05 55mTalk | Invited Talk: Let’s Go Mainstream with Eta! HIW Rahul Muttineni TypeLead Media Attached | ||
09:00 - 10:00 | |||
09:00 30mTalk | What an SMT solver can do for you PLMW @ ICFP Nadia Polikarpova University of California, San Diego | ||
09:30 30mTalk | Gradual Types PLMW @ ICFP Ronald Garcia University of British Columbia | ||
10:00 - 10:20 | |||
10:00 20mCoffee break | Sunday coffee break 1 Catering | ||
10:20 - 11:00 | |||
10:20 40mTalk | Finding fixed points faster HOPE Michael Arntzenius University of Birmingham, UK | ||
10:20 - 12:00 | |||
10:20 25mTalk | GHC Update HIW Simon Peyton Jones Microsoft, UK File Attached | ||
10:45 25mTalk | Source Plugins HIW Matthew Pickering University of Bristol Media Attached | ||
11:10 25mTalk | Generalized Abstract GHC.Generics HIW Ryan Scott Indiana University at Bloomington, USA File Attached | ||
11:35 8mTalk | Lightning talk: CodeWorld: Teaching Haskell and mathematics to children HIW Chris Smith Google, USA | ||
11:43 8mTalk | Lightning talk: CoreSpec: Verifying GHC with hs-to-coq HIW File Attached | ||
11:51 9mTalk | Lightning talk: The trick which makes exceptions-0.10.0 possible HIW Samuel Gélineau SimSpace Media Attached | ||
10:20 - 12:00 | |||
10:20 30mTalk | I'm a Young Assistant Professor: AMA. + Heather's Unsolicited Advice About Grad School PLMW @ ICFP Heather Miller Carnegie Mellon University | ||
10:50 70mSocial Event | Interactive Game PLMW @ ICFP | ||
11:00 - 11:20 | |||
11:00 20mCoffee break | Sunday coffee break 2 Catering | ||
11:20 - 12:00 | |||
11:20 40mTalk | A Metalanguage for Guarded Iteration HOPE Sergey Goncharov Friedrich-Alexander-Universität Erlangen-Nürnberg, Christoph Rauch FAU Erlangen-Nürnberg, Lehrstuhl 8, Lutz Schröder FAU Erlangen-Nürnberg, Lehrstuhl 8 | ||
12:00 - 13:30 | |||
12:00 90mLunch | Sunday lunch Catering | ||
13:30 - 14:10 | |||
13:30 40mTalk | Functional programming with MLTS HOPE | ||
13:30 - 15:10 | |||
13:30 25mTalk | Coercion Quantification HIW Link to publication File Attached | ||
13:55 25mTalk | Type-level visible type application HIW My Nguyen Bryn Mawr College File Attached | ||
14:20 25mTalk | Implementing Linear Haskell HIW Media Attached | ||
14:45 8mTalk | Lightning talk: Implementing a VMware Haskell Client with Extensible Records HIW Matthew Russell SimSpace Link to publication File Attached | ||
14:53 8mTalk | Lightning talk: Asterius: Bringing Haskell to WebAssembly HIW Cheng Shao Tweag I/O Media Attached | ||
15:01 9mTalk | Lightning talk: Perfomance impact of control flow optimization HIW | ||
13:30 - 15:10 | |||
13:30 33mTalk | How to write a Great Research Paper PLMW @ ICFP Simon Peyton Jones Microsoft, UK | ||
14:03 33mTalk | Dependent Types PLMW @ ICFP Stephanie Weirich University of Pennsylvania, USA | ||
14:36 34mTalk | An opinionated talk on how to give talks PLMW @ ICFP Ranjit Jhala University of California, San Diego | ||
14:10 - 14:30 | |||
14:10 20mCoffee break | Sunday coffee break 3 Catering | ||
14:30 - 15:10 | |||
14:30 40mTalk | Taming Control Flow through Linear Effect Handlers HOPE | ||
15:10 - 15:30 | |||
15:10 20mCoffee break | Sunday coffee break 4 Catering | ||
15:30 - 16:10 | |||
15:30 40mTalk | A domain theory for statistical probabilistic programming HOPE Ohad Kammar University of Oxford, Matthijs Vákár University of Oxford, Sam Staton University of Oxford File Attached | ||
15:30 - 16:45 | |||
15:30 25mTalk | Pier: yet another Haskell build tool HIW File Attached | ||
15:55 25mTalk | Clash: a practical Haskell to circuit compiler HIW Christiaan Baaij QBayLogic B.V. File Attached | ||
16:20 8mTalk | Lightning talk: More Explicit Foralls in GHC HIW | ||
16:28 17mOther | GHC Community Discussion HIW Simon Peyton Jones Microsoft, UK | ||
15:30 - 16:30 | |||
15:30 60mTalk | Panel Discussion: Research in Functional Programming PLMW @ ICFP Alejandro Russo Chalmers University of Technology, Sweden, Katie Ots Facebook, Leonidas Lampropoulos University of Pennsylvania, David Darais University of Vermont, Ivan Perez National Institute of Aerospace, USA | ||
Mon 24 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Mon 24 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Monday KeynoteKeynotes and Reports at Stifel Theatre Chair(s): Robert Bruce Findler Northwestern University, USA | ||
09:00 60mTalk | Gradual Typing Keynotes and Reports Ronald Garcia University of British Columbia | ||
10:05 - 10:30 | |||
10:05 25mCoffee break | Monday coffee break 1 Catering | ||
10:30 - 12:00 | Environments and ToolsResearch Papers at Stifel Theatre Chair(s): Alejandro Russo Chalmers University of Technology, Sweden | ||
10:30 22mTalk | Build Systems à la CarteDistinguished Paper Research Papers DOI | ||
10:52 22mTalk | Keep Your Laziness in Check Research Papers Kenneth Foner , Hengchu Zhang University of Pennsylvania, Leonidas Lampropoulos University of Pennsylvania DOI | ||
11:15 22mTalk | Merlin: A Language Server for OCaml (Experience Report) Research Papers DOI | ||
11:37 22mTalk | Functional Programming for Compiling and Decompiling Computer-Aided Design Research Papers Chandrakana Nandi University of Washington, USA, James R. Wilcox University of Washington, Taylor Blau University of Washington, Dan Grossman University of Washington, Zachary Tatlock University of Washington, Seattle DOI | ||
12:00 - 13:00 | |||
12:00 60mLunch | Monday lunch Catering | ||
13:00 - 14:30 | Program ConstructionResearch Papers at Stifel Theatre Chair(s): J. Garrett Morris University of Kansas, USA | ||
13:00 22mTalk | Prototyping a Functional Language using Higher-Order Logic Programming: A Functional Pearl on Learning the Ways of λProlog/Makam Research Papers DOI | ||
13:22 22mTalk | A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs Research Papers Guillaume Allais Radboud University Nijmegen, Robert Atkey University of Strathclyde, James Chapman , Conor McBride , James McKinna DOI | ||
13:45 22mTalk | Reasonably Programmable Literal Notation Research Papers Link to publication DOI | ||
14:07 22mTalk | Refunctionalization of Abstract Abstract Machines: Bridging the Gap between Abstract Abstract Machines and Abstract Definitional Interpreters (Functional Pearl) Research Papers DOI | ||
14:30 - 15:00 | |||
14:30 30mCoffee break | Monday coffee break 2 Catering | ||
15:00 - 16:10 | Continuations and EffectsResearch Papers at Stifel Theatre Chair(s): Martin Elsman University of Copenhagen, Denmark | ||
15:00 23mTalk | Capturing the Future by Replaying the Past (Functional Pearl) Research Papers DOI | ||
15:23 23mTalk | Handling Delimited Continuations with Dependent Types Research Papers DOI | ||
15:46 23mTalk | Versatile Event Correlation with Algebraic Effects Research Papers Oliver Bračevac TU Darmstadt, Nada Amin University of Cambridge, Guido Salvaneschi TU Darmstadt, Sebastian Erdweg Delft University of Technology, Netherlands, Patrick Eugster Purdue University, Mira Mezini TU Darmstadt DOI | ||
16:10 - 16:40 | |||
16:10 30mCoffee break | Monday coffee break 3 Catering | ||
16:40 - 18:10 | Probabilistic Programming and LearningResearch Papers at Stifel Theatre Chair(s): Michael Sperber Active Group GmbH | ||
16:40 22mTalk | The Simple Essence of Automatic DifferentiationDistinguished Paper Research Papers Conal Elliott Target, USA DOI | ||
17:02 22mTalk | Functional Programming for Modular Bayesian Inference Research Papers Adam Ścibior University of Cambridge and MPI Tuebingen, Ohad Kammar University of Oxford, Zoubin Ghahramani University of Cambridge DOI | ||
17:25 22mTalk | Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion Research Papers Mitchell Wand Northeastern University, USA, Ryan Culpepper Czech Technical University, Theophilos Giannakopoulos BAE Systems, Inc., Andrew Cobb Northeastern University DOI | ||
17:47 22mTalk | Teaching How to Program using Automated Assessment and Functional Glossy Games (Experience Report) Research Papers José Bacelar Almeira University of Minho & INESC TEC, Alcino Cunha University of Minho and INESC TEC, Portugal, Nuno Macedo University of Minho & INESC TEC, Hugo Pacheco University of Minho, Portugal, José Proença HASLab/INESC TEC & University of Minho DOI | ||
18:30 - 20:30 | |||
18:30 2hSocial Event | SRC Poster Reception Social Events | ||
Tue 25 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Tue 25 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 60mTalk | The Role of Functional Programming and DSLs in Hardware Keynotes and Reports Pat Hanrahan Stanford University, USA | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Tuesday coffee break 1 Catering | ||
10:30 - 12:00 | Compilation and ConcurrencyResearch Papers at Stifel Theatre Chair(s): Heather Miller Carnegie Mellon University | ||
10:30 22mTalk | Competitive Parallelism: Getting Your Priorities Right Research Papers DOI | ||
10:52 22mTalk | Static Interpretation of Higher-Order Modules in Futhark: Functional GPU Programming in the Large Research Papers Martin Elsman University of Copenhagen, Denmark, Troels Henriksen University of Copenhagen, Denmark, Danil Annenkov Department of Computer Science, University of Copenhagen, Cosmin Oancea University of Copenhagen, Denmark Link to publication DOI | ||
11:15 22mTalk | Finitary Polymorphism for Optimizing Type-Directed Compilation Research Papers Atsushi Ohori Tohoku University, Japan, Katsuhiro Ueno Tohoku University, Hisayuki Mima Tohoku University DOI | ||
11:37 22mTalk | Fault Tolerant Functional Reactive Programming (Functional Pearl) Research Papers Ivan Perez National Institute of Aerospace, USA DOI | ||
12:00 - 13:00 | |||
12:00 60mLunch | Tuesday lunch Catering | ||
12:15 - 12:50 | |||
12:15 35mTalk | Report on ICFP and Climate Change Keynotes and Reports | ||
13:00 - 14:30 | Proof Techniques and MechanizationResearch Papers at Stifel Theatre Chair(s): Niki Vazou University of Maryland, USA | ||
13:00 22mTalk | MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic Research Papers Robbert Krebbers Delft University of Technology, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Ralf Jung MPI-SWS, Joseph Tassarotti Carnegie Mellon University, Jan-Oliver Kaiser MPI-SWS, Amin Timany imec-Distrinet KU-Leuven, Arthur Charguéraud Inria, Derek Dreyer MPI-SWS DOI | ||
13:22 22mTalk | Mtac2: Typed Tactics for Backward Reasoning in Coq Research Papers Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET, Robbert Krebbers Delft University of Technology, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek Dreyer MPI-SWS DOI | ||
13:45 22mTalk | Compositional Soundness Proofs of Abstract Interpreters Research Papers Sven Keidel Delft University of Technology, Netherlands, Casper Bach Poulsen Delft University of Technology, Sebastian Erdweg Delft University of Technology, Netherlands DOI | ||
14:07 22mTalk | Equivalences for Free: Univalent Parametricity for Effective TransportDistinguished Paper Research Papers DOI | ||
14:30 - 15:00 | |||
14:30 30mCoffee break | Tuesday coffee break 2 Catering | ||
15:00 - 16:30 | Bidirectional ProgrammingResearch Papers at Stifel Theatre Chair(s): Wouter Swierstra Utrecht University, Netherlands | ||
15:00 22mTalk | What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma (Functional Pearl) Research Papers Guillaume Boisseau University of Oxford, Jeremy Gibbons Department of Computer Science, University of Oxford DOI | ||
15:22 22mTalk | Incremental Relational Lenses Research Papers Rudi Horn University of Edinburgh, Roly Perera University of Glasgow, James Cheney University of Edinburgh, UK DOI | ||
15:45 22mTalk | Synthesizing Quotient Lenses Research Papers Solomon Maina University of Pennsylvania, Anders Miltner Princeton University, Kathleen Fisher Tufts University, USA, Benjamin C. Pierce University of Pennsylvania, Dave Walker Princeton University, Steve Zdancewic University of Pennsylvania DOI | ||
16:07 22mTalk | Generic Deriving of Generic Traversals Research Papers Csongor Kiss Imperial College London, Matthew Pickering University of Bristol, Nicolas Wu University of Bristol, UK DOI | ||
16:30 - 17:00 | |||
16:30 30mCoffee break | Tuesday coffee break 3 Catering | ||
17:00 - 17:40 | |||
17:00 40mTalk | Finalist Presentations Student Research Competition | ||
17:40 - 18:10 | |||
17:40 30mTalk | Contest Report and Results Programming Contest Matthew Fluet Rochester Institute of Technology | ||
Wed 26 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Wed 26 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Wednesday KeynoteKeynotes and Reports at Stifel Theatre Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford | ||
09:00 60mTalk | Conveying the Power of Abstraction Keynotes and Reports | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Wednesday coffee break 1 Catering | ||
10:30 - 12:00 | |||
10:30 22mTalk | Partially-Static Data as Free Extension of Algebras Research Papers Jeremy Yallop University of Cambridge, UK, Tamara von Glehn University of Cambridge, Ohad Kammar University of Oxford Link to publication DOI Pre-print | ||
10:52 22mTalk | Relational Algebra by Way of AdjunctionsDistinguished Paper Research Papers Jeremy Gibbons Department of Computer Science, University of Oxford, Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU), Ralf Hinze Radboud University Nijmegen, Nicolas Wu University of Bristol, UK DOI | ||
11:15 22mTalk | Strict and Lazy Semantics for Effects: Layering Monads and Comonads Research Papers DOI | ||
11:37 22mTalk | What's the Difference? A Functional Pearl on Subtracting Bijections Research Papers DOI | ||
12:00 - 13:00 | |||
12:00 60mLunch | Wednesday lunch Catering | ||
13:00 - 14:30 | Gradual Typing and ProvingResearch Papers at Stifel Theatre Chair(s): Éric Tanter University of Chile & Inria Paris | ||
13:00 22mTalk | A Spectrum of Type Soundness and Performance Research Papers DOI | ||
13:22 22mTalk | Casts and Costs: Harmonizing Safety and Performance in Gradual Typing Research Papers John Peter Campora ULL Lafayette, Sheng Chen University of Louisiana at Lafayette, Eric Walkingshaw Oregon State University DOI | ||
13:45 22mTalk | Graduality from Embedding-Projection Pairs Research Papers DOI | ||
14:07 22mTalk | Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report) Research Papers Joachim Breitner DFINITY Foundation, Antal Spector-Zabusky , Yao Li University of Pennsylvania, Christine Rizkallah University of New South Wales, John Wiegley BAE Systems, Stephanie Weirich University of Pennsylvania, USA DOI | ||
14:30 - 15:00 | |||
14:30 30mCoffee break | Wednesday coffee break 2 Catering | ||
15:00 - 16:10 | Complexity and BoundsResearch Papers at Stifel Theatre Chair(s): Ilya Sergey University College London | ||
15:00 23mTalk | Parallel Complexity Analysis with Temporal Session Types Research Papers Ankush Das Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA DOI | ||
15:23 23mTalk | Parametric Polymorphism and Operational Improvement Research Papers DOI | ||
15:46 23mTalk | Tight Typings and Split Bounds Research Papers Beniamino Accattoli Inria & Ecole Polytechnique, Stéphane Graham-Lengrand CNRS, France, Delia Kesner IRIF, France / University of Paris Diderot, France DOI | ||
16:10 - 16:30 | |||
16:10 20mCoffee break | Wednesday coffee break 3 Catering | ||
16:30 - 17:15 | |||
16:30 22mTalk | Elaborating Dependent (Co)pattern Matching Research Papers DOI | ||
16:52 22mTalk | Generic Zero-Cost Reuse for Dependent Types Research Papers DOI | ||
17:15 - 18:00 | |||
17:15 15mAwards | SIGPLAN Awards Keynotes and Reports Satnam Singh X, the moonshot factory | ||
17:30 10mAwards | Student Research Competition Awards Keynotes and Reports Ravi Chugh University of Chicago | ||
17:40 15mTalk | Program Chair's Report Keynotes and Reports Matthew Flatt University of Utah | ||
17:55 5mTalk | ICFP 2019 Announcement Keynotes and Reports Derek Dreyer MPI-SWS | ||
17:30 - 17:40 | |||
17:30 10mAwards | Student Research Competition Awards Keynotes and Reports Ravi Chugh University of Chicago | ||
18:00 - 19:00 | |||
18:00 60mDinner | Wednesday food trucks Catering | ||
19:00 - 21:30 | |||
19:00 2h30mSocial Event | Strange Loop Party, ride a bus from the venue to the City Museum Social Events | ||
Thu 27 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Thu 27 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
08:45 - 10:00 | |||
08:45 10mTalk | Welcome! TyDe | ||
08:55 20mTalk | Extended Abstract: F# OpenCL Type Provider TyDe Kirill Smirenko Saint Petersburg State University, Semyon Grigorev Saint-Petersburg State University, JetBrains Research File Attached | ||
09:15 20mTalk | Extended Abstract: Comprehending Monoids with Class TyDe Media Attached File Attached | ||
09:35 25mResearch paper | Authenticated Modular Maps in Haskell TyDe Victor Cacciari Miraldo Utrecht University, Netherlands, Harold Carr Oracle Labs, USA, Alex Kogan Oracle Labs, USA, Mark Moir Oracle Labs, New Zealand, Maurice Herlihy Brown University, USA DOI | ||
09:00 - 12:00 | T01: Introduction to Programming and Proving in CedilleTutorials at Burlington Route Chair(s): Aaron Stump The University of Iowa, USA | ||
09:00 3hOther | T01: Introduction to Programming and Proving in Cedille Tutorials | ||
09:00 - 10:00 | |||
09:00 5mDay opening | Introduction OCaml Andrew Kennedy Facebook London | ||
09:05 30mTalk | The OCaml Platform 1.0 OCaml | ||
09:35 10mPoster | The OCaml Software Foundation OCaml | ||
09:45 5mPoster | This PDF is an OCaml bytecode OCaml Gabriel Radanne University of Freiburg, Germany | ||
09:00 - 10:00 | |||
09:00 5mDay opening | Welcome and Chair's Report Haskell Nicolas Wu University of Bristol, UK | ||
09:05 55mTalk | Neither Web nor Assembly (Invited Talk) Haskell Andreas Rossberg Dfinity | ||
09:00 - 10:00 | |||
09:00 60mDay opening | Daisy - a framework for sound accuracy analysis and optimization of numerical programs NPFL Eva Darulova MPI-SWS | ||
10:00 - 10:20 | |||
10:00 20mCoffee break | Thursday coffee break 1 Catering | ||
10:20 - 11:00 | |||
10:20 20mTalk | Abusing Format for fun and profits OCaml | ||
10:40 20mTalk | RFCs, all the way down! OCaml Romain Calascibetta Tarides | ||
10:20 - 12:00 | |||
10:20 25mResearch paper | Typing, Representing, and Abstracting Control: Functional Pearl TyDe Philipp Schuster University of Tübingen, Germany, Jonathan Immanuel Brachthäuser University of Tübingen, Germany DOI | ||
10:45 25mResearch paper | Extensible Type-Directed Editing TyDe DOI | ||
11:10 25mResearch paper | Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming TyDe Victor Cacciari Miraldo Utrecht University, Netherlands, Alejandro Serrano Utrecht University, Netherlands DOI | ||
11:35 25mResearch paper | Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL TyDe DOI | ||
10:20 - 11:20 | |||
10:20 30mTalk | Hasktorch: A Comprehensive Haskell Library for Differentiable Functional Programming NPFL | ||
10:50 30mTalk | APLicative Programming with Naperian Functors NPFL Jeremy Gibbons Department of Computer Science, University of Oxford | ||
10:30 - 12:00 | |||
10:30 30mTalk | AutoBench: Comparing the Time Performance of Haskell Programs Haskell DOI | ||
11:00 30mTalk | Autobahn 2.0: Minimizing Bangs while Maintaining Performance (System Demonstration) Haskell DOI | ||
11:30 30mTalk | Improving Typeclass Relations by Being Open Haskell Guido Martínez CIFASIS-CONICET, Argentina, Mauro Jaskelioff CONICET, Argentina, Guido De Luca Universidad Nacional de Rosario, Argentina DOI | ||
11:00 - 11:20 | |||
11:00 20mCoffee break | Thursday coffee break 2 Catering | ||
11:20 - 12:00 | |||
11:20 20mTalk | The Vecosek Ecosystem OCaml Sebastien Mondet Mount Sinai - Hammer Lab | ||
11:40 20mTalk | OCaml on the ESP32 chip: Well Typed Lightbulbs Await OCaml | ||
11:20 - 12:00 | |||
11:20 40mTalk | Error analysis almost for free NPFL | ||
12:00 - 13:30 | |||
12:00 90mLunch | Thursday lunch Catering | ||
13:00 - 16:00 | T02: Direct Manipulation Programming in Sketch-n-SketchTutorials at Burlington Route Chair(s): Ravi Chugh University of Chicago, Brian Hempel University of Chicago, Justin Lubin , Mikaël Mayer EPFL, Switzerland | ||
13:00 3hOther | T02: Direct Manipulation Programming in Sketch-n-Sketch Tutorials Nick Collins University of Chicago, Brian Hempel University of Chicago, Ravi Chugh University of Chicago, Mikaël Mayer EPFL, Switzerland, Justin Lubin | ||
13:30 - 14:10 | |||
13:30 20mTalk | Wall: rendering vector graphics with OCaml and OpenGL OCaml Frédéric Bour Facebook Paris | ||
13:50 20mTalk | Winning on Windows: porting the OCaml platform OCaml David Allsopp University of Cambridge | ||
13:30 - 15:00 | |||
13:30 30mTalk | Rhine: FRP with Type-Level Clocks Haskell DOI | ||
14:00 30mTalk | A High-Performance Multicore IO Manager Based on libuv (Experience Report) Haskell DOI | ||
14:30 30mTalk | Embedding Invertible Languages with Binders: A Case of the FliPpr Language Haskell DOI | ||
13:30 - 14:20 | |||
13:30 50mTalk | Extrinsic vs Intrinsic Specifications, and Subset Types TyDe K. Rustan M. Leino Amazon | ||
13:30 - 14:30 | Talks IIINPFL at Texas Special Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford | ||
13:30 30mTalk | A Haskell Interface to Sundials via inline-c NPFL Dominic Steinitz Tweag I/O | ||
14:00 30mTalk | On the Calculation of Functions in the Algebra of Physical Space NPFL Nathan Waivio https://github.com/waivio | ||
14:10 - 14:30 | |||
14:10 20mCoffee break | Thursday coffee break 3 Catering | ||
14:20 - 15:10 | Effect Handlers & Abstract MachineTyDe at New York Central Chair(s): Niki Vazou University of Maryland, USA | ||
14:20 25mResearch paper | First Class Dynamic Effect Handlers: or, Polymorphic Heaps with Dynamic Effect Handlers TyDe Daan Leijen Microsoft Research, USA DOI | ||
14:45 25mResearch paper | From Algebra to Abstract Machine: A Verified Generic Construction TyDe Carlos Tomé Cortiñas Utrecht University, Netherlands, Wouter Swierstra Utrecht University, Netherlands DOI | ||
14:30 - 15:10 | |||
14:30 20mTalk | R&B: Towards bringing functional programming to everyday's web programmer OCaml Hongbo Zhang Independent, Cristiano Calcagno Facebook, Jordan Walke Facebook, Cheng Lou Facebook, Ricky Vetter Facebook | ||
14:50 20mTalk | MLExplain OCaml Link to publication | ||
14:30 - 15:10 | |||
14:30 40mTalk | Manifolds as Haskell types NPFL Justus Sagemüller Universität zu Köln, Institut für Geophysik und Meteorologie | ||
15:10 - 15:30 | |||
15:10 20mCoffee break | Thursday coffee break 4 Catering | ||
15:30 - 16:10 | |||
15:30 20mTalk | Relit: Implementing Typed Literal Macros in Reason OCaml | ||
15:30 - 16:00 | |||
15:30 30mTalk | Ghosts of Departed Proofs (Functional Pearl) Haskell Matt Noonan Kataskeue, USA DOI | ||
15:30 - 16:10 | |||
15:30 20mTalk | Extended Abstract: Context Constrained Computing TyDe File Attached | ||
15:50 20mTalk | Extended Abstract: Improving Error Messages for Dependent Types TyDe Joseph Eremondi University of British Columbia, Wouter Swierstra Utrecht University, Netherlands, Jurriaan Hage Utrecht University File Attached | ||
15:30 - 16:10 | |||
15:30 40mTalk | Exact Real Arithmetic for Geometric Operations NPFL Pavel Panchekha University of Washington | ||
16:30 - 17:20 | |||
16:30 50mTalk | Strange Loop Keynote Keynotes and Reports | ||
17:30 - 19:30 | |||
17:30 2hSocial Event | Industrial Reception Social Events | ||
19:00 - 22:00 | |||
19:00 3hSocial Event | Strange Loop Unsessions at Union Station; see Strange Loop website for details Social Events | ||
Fri 28 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Fri 28 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 60mTalk | From Scripting to Proving: Gradual Verification with a Scheme Scheme David Van Horn University of Maryland, USA | ||
09:00 - 10:00 | |||
09:00 60mTalk | Cross-Platform Language Design in Scala.js Scala Sébastien Doeraene EPFL, Switzerland DOI | ||
09:00 - 10:00 | |||
09:00 30mTalk | Deriving Via: or, How to Turn Hand-Written Instances into an Anti-pattern Haskell Baldur Blöndal n.n., n.n., Andres Löh Well-Typed, UK, Ryan Scott Indiana University at Bloomington, USA DOI | ||
09:30 30mTalk | Generic Programming of All Kinds Haskell Alejandro Serrano Utrecht University, Netherlands, Victor Cacciari Miraldo Utrecht University, Netherlands DOI | ||
09:00 - 10:00 | |||
09:00 60mTalk | ELPI: an extension language with binders and unification variables (Invited talk) ML Enrico Tassi INRIA | ||
09:00 - 12:00 | T03: Abstracting Gradual Typing: A Systematic Approach to Designing Gradually Typed LanguagesTutorials at Texas Special Chair(s): Ronald Garcia University of British Columbia, Éric Tanter University of Chile & Inria Paris | ||
09:00 3hOther | T03: Abstracting Gradual Typing: A Systematic Approach to Designing Gradually Typed Languages Tutorials | ||
10:00 - 10:20 | |||
10:00 20mCoffee break | Friday coffee break 1 Catering | ||
10:20 - 11:00 | |||
10:20 20mTalk | Growing Schemes: Twenty Years of Scheme Requests for Implementation Scheme Arthur Gleckler SRFI Editor | ||
10:40 20mTalk | Loop Patterns: Extension of Kleene Star Operator for More Powerful Pattern Matching against Arbitrary Data Structures Scheme Satoshi Egi Rakuten Institute of Technology | ||
10:20 - 11:50 | |||
10:20 22mTalk | Extending Scala with Records: Design, Implementation, and Evaluation Scala DOI | ||
10:42 23mTalk | Initialization Patterns in Dotty Scala DOI | ||
11:05 22mTalk | Path Dependent Types with Path-Equality Scala DOI | ||
11:27 23mTalk | κDOT: Scaling DOT with Mutation and Constructors Scala DOI | ||
10:20 - 12:00 | |||
10:20 25mTalk | Safely Mixing OCaml and Rust ML Stephen Dolan University of Cambridge | ||
10:45 25mTalk | Rust Distilled: An Expressive Tower of Languages ML Aaron Weiss Northeastern University, Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA Link to publication Pre-print | ||
11:10 25mTalk | Generating Mutually Recursive Definitions ML Pre-print | ||
11:35 25mTalk | Experience Report: Type-Safe Multi-Tier Programming with Standard ML Modules ML Martin Elsman University of Copenhagen, Denmark, Philip Munksgaard Intelligent Alpha AG, Switzerland, Ken Friis Larsen DIKU, University of Copenhagen Link to publication | ||
10:30 - 12:00 | |||
10:30 30mTalk | Type Variables in Patterns Haskell Richard A. Eisenberg Bryn Mawr College, USA, Joachim Breitner DFINITY Foundation, Simon Peyton Jones Microsoft, UK DOI | ||
11:00 30mTalk | The Thoralf Plugin: For Your Fancy Type Needs Haskell DOI | ||
11:30 30mTalk | Suggesting Valid Hole Fits for Typed-Holes (Experience Report) Haskell Matthías Páll Gissurarson Chalmers University of Technology, Sweden DOI | ||
11:00 - 11:20 | |||
11:00 20mCoffee break | Friday coffee break 2 Catering | ||
11:20 - 12:00 | |||
11:20 20mTalk | Temporal Logic, μKanren, and a Time-Traveling RDF Database Scheme | ||
11:40 20mTalk | A Surprisingly Competitive Conditional Operator: miniKanrenizing the Inference Rules of Pie Scheme Benjamin Boskin , Weixi Ma , David Thrane Christiansen Galois, USA, Daniel Friedman Indiana University | ||
11:50 - 12:10 | |||
11:50 10mTalk | Julia Subtyping Lessons Scala Could Learn (Student Talk) Scala Artem Pelenitsyn Northeastern University | ||
12:00 10mTalk | Scala with explicit nulls (student talk) Scala | ||
12:00 - 13:30 | |||
12:00 90mLunch | Friday lunch Catering | ||
13:00 - 16:00 | T04: Beluga: Programming Proofs About Formal SystemsTutorials at Texas Special Chair(s): Jacob Thomas Errington McGill University, Aliya Hameer McGill University, Brigitte Pientka McGill University | ||
13:00 3hTalk | T04: Beluga: Programming Proofs About Formal Systems Tutorials Brigitte Pientka McGill University, Jacob Thomas Errington McGill University, Aliya Hameer McGill University | ||
13:10 - 14:40 | |||
13:10 22mTalk | Garnishing Parsec with Parsley Scala DOI | ||
13:32 22mTalk | Interflow: Interprocedural Flow-Sensitive Type Inference and Method Duplication Scala DOI | ||
13:55 22mTalk | Parser Combinators for Context-Free Path Querying Scala Ekaterina Verbitskaia Saint Petersburg State University, Russia, Ilya Kirillov Saint Petersburg State University, Russia, Ilya Nozkin Saint Petersburg State University, Russia, Semyon Grigorev Saint Petersburg State University, Russia DOI | ||
14:17 22mTalk | Truly Abstract Interfaces for Algebraic Data Types: The Extractor Typing Problem Scala Nicolas Stucki EPFL, Switzerland, Paolo G. Giarrusso EPFL, Switzerland, Martin Odersky EPFL, Switzerland DOI | ||
13:30 - 14:10 | |||
13:30 20mTalk | Racets: Faceted Execution in Racket Scheme Kristopher Micinski Haverford College, Zhanpeng Wang Haverford College, USA, Thomas Gilray University of Maryland | ||
13:50 20mTalk | An Efficient Compiler for the Gradually Typed Lambda Calculus Scheme Andre Kuhlenschmidt Indiana University, Deyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA | ||
13:30 - 15:00 | |||
13:30 30mTalk | A Promise Checked Is a Promise Kept: Inspection Testing Haskell Joachim Breitner DFINITY Foundation DOI | ||
14:00 30mTalk | Branching Processes for QuickCheck Generators Haskell Agustín Mista Universidad Nacional de Rosario, Argentina, Alejandro Russo Chalmers University of Technology, Sweden, John Hughes Chalmers University of Technology, Sweden DOI | ||
14:30 30mTalk | Coherent Explicit Dictionary Application for Haskell Haskell DOI File Attached | ||
13:30 - 15:10 | |||
13:30 25mTalk | ML as a Tactic Language, Again ML Guido Martínez CIFASIS-CONICET, Argentina, Danel Ahman University of Ljubljana, Victor Dumitrescu , Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Cătălin Hriţcu Inria Paris, Monal Narasimhamurthy , Zoe Paraskevopoulou Princeton University, Clément Pit-Claudel MIT CSAIL, Jonathan Protzenko Microsoft Research, Redmond, Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research File Attached | ||
13:55 25mTalk | Design and verification of functional proof checkers ML Roberto Blanco Inria | ||
14:20 25mTalk | Disornamentation ML | ||
14:45 25mTalk | Generic Programming with Combinators and Objects ML | ||
14:10 - 14:30 | |||
14:10 20mCoffee break | Friday coffee break 3 Catering | ||
14:30 - 15:10 | |||
14:30 20mTalk | Schism: A Self-Hosting Scheme to WebAssembly Compiler Scheme Eric Holk Google | ||
14:50 20mTalk | Tail Calling Between Code Generated by C and Native Backends Scheme | ||
14:40 - 15:00 | |||
14:40 10mTalk | Adding polymorphic functions to Scala (Student Talk) Scala Guillaume Martres EPFL, Switzerland | ||
14:50 10mTalk | Validating Changes in Typechecking on Codebases with SemanticDB (Student talk) Scala | ||
15:10 - 15:30 | |||
15:10 20mCoffee break | Friday coffee break 4 Catering | ||
15:20 - 16:10 | Session 3: DSLs & Sponsor TalkScala at Frisco Chair(s): Sebastian Erdweg Delft University of Technology, Netherlands | ||
15:20 22mTalk | A Domain-specific Language for Microservices Scala Jacob Donham Twitter, Inc. DOI | ||
15:42 28mIndustry talk | SemanticDB: a common data model for Scala developer tools Scala Eugene Burmako Twitter, Inc. | ||
15:30 - 16:10 | |||
15:30 40mTalk | Rebuilding Racket on Chez Scheme: An Experience Report Scheme Matthew Flatt University of Utah | ||
15:30 - 16:00 | |||
15:30 29mTalk | Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl) Haskell Niki Vazou University of Maryland, USA, Joachim Breitner DFINITY Foundation, Rose Kunkel University of Maryland, USA, David Van Horn University of Maryland, USA, Graham Hutton University of Nottingham, UK DOI | ||
15:59 1mTalk | Closing Statement Haskell Nicolas Wu University of Bristol, UK | ||
15:30 - 16:10 | |||
15:30 40mTalk | Programming with Abstract Algebraic Effects ML Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław | ||
16:30 - 17:20 | |||
16:30 50mTalk | Strange Loop Keynote: Machine learning failures - for art! Keynotes and Reports | ||
Sat 29 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Sat 29 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
08:45 - 10:00 | |||
08:45 15mDay opening | Welcome and Introductions FHPC | ||
09:00 60mTalk | HELIX: A Case Study of a Formal Verification of High Performance Program Generation FHPC A: Vadim Zaliva Carnegie Mellon University, USA, A: Franz Franchetti Carnegie Mellon University, USA DOI | ||
09:00 - 10:00 | |||
09:00 10mDay opening | Day Openning Erlang | ||
09:10 50mTalk | Invited Keynote -- Distributed Erlang: From Datacenter Applications to Planetary Scale Applications Erlang | ||
09:00 - 12:00 | T06: Getting Satisfaction out of Games: Learning to use SAT solvers through puzzles and gamesTutorials at Frisco Chair(s): Jose Calderon Galois, Inc., Eric Mertens Galois, Inc. | ||
09:00 3hOther | T06: Getting Satisfaction out of Games: Learning to use SAT solvers through puzzles and games Tutorials | ||
09:00 - 10:00 | |||
09:00 10mDay opening | Welcome FARM | ||
09:10 25mResearch paper | NNdef: Livecoding Digital Musical Instruments in SuperCollider using Functional Reactive Programming FARM Miguel Negrão Polytechnic Institute of Leiria DOI | ||
09:35 25mDemonstration | La Habra — Livecoding with Clojurescript FARM | ||
09:00 - 12:00 | |||
09:00 3hOther | T07: Writing a chat system in Pony Tutorials | ||
09:00 - 12:00 | T05: Purely functional UIs with ReaclTutorials at Wabash Cannonball Chair(s): Michael Sperber Active Group GmbH | ||
09:00 3hOther | T05: Purely functional UIs with Reacl Tutorials Michael Sperber Active Group GmbH | ||
10:00 - 10:20 | |||
10:00 20mCoffee break | Saturday coffee break 1 Catering | ||
10:20 - 11:00 | |||
10:20 40mProduct announcement | Latest News from the OTP Team Erlang | ||
10:20 - 12:00 | |||
10:20 25mResearch paper | Compositional Computational Constructive Critique: Or, How My Computer Learned to Appreciate Poetry FARM Jennifer Hackett University of Nottingham, UK DOI | ||
10:45 25mDemonstration | Chord Progressions in Haskell FARM Brittni Watkins Southern Methodist University | ||
11:10 25mDemonstration | Pattern-Based Algorithmic Music with Euterpea FARM Donya Quick Stevens Institute of Technology | ||
11:35 25mDemonstration | GAYER: A Graphical Audio plaYER in ReasonML FARM | ||
10:20 - 12:15 | |||
10:20 60mTalk | Modular Acceleration: Tricky Cases of Functional High-Performance Computing FHPC A: Troels Henriksen University of Copenhagen, Denmark, A: Martin Elsman University of Copenhagen, Denmark, A: Cosmin Oancea University of Copenhagen, Denmark DOI | ||
11:20 45mTalk | Preventing Data Races with Refinement Types FHPC | ||
11:00 - 11:20 | |||
11:00 20mCoffee break | Saturday coffee break 2 Catering | ||
11:20 - 12:00 | |||
11:20 25mFull-paper | Understanding Formal Specifications through Good Examples Erlang A: Alex Gerdes University of Gothenburg, Sweden, A: John Hughes Chalmers University of Technology, Sweden, A: Nicholas Smallbone Chalmers University of Technology, Sweden, A: Stefan Hanenberg University of Duisburg-Essen, Germany, A: Sebastian Ivarsson Chalmers University of Technology, Sweden, A: Meng Wang University of Bristol, UK DOI | ||
11:45 15mShort-paper | Towards Secure Erlang Systems Erlang DOI | ||
12:00 - 13:30 | |||
12:00 90mLunch | Saturday lunch Catering | ||
13:00 - 16:00 | T09: Pijul, a purely functional version control systemTutorials at Frisco Chair(s): Pierre-Étienne Meunier | ||
13:00 3hOther | T09: Pijul, a purely functional version control system. Tutorials | ||
13:00 - 16:00 | T10: Hop.js: JavaScript multitier programmingTutorials at Texas Special Chair(s): Manuel Serrano Inria, France | ||
13:00 3hOther | T10: Hop.js: JavaScript multitier programming Tutorials Manuel Serrano Inria, France | ||
13:00 - 16:00 | T08: Implement your own reactive language: the ReactiveML experimentTutorials at Wabash Cannonball Chair(s): Guillaume Baudart IBM Research, Louis Mandel IBM Research, Cédric Pasteur , Marc Pouzet École normale supérieure | ||
13:00 3hOther | T08: Implement your own reactive language: the ReactiveML experiment Tutorials Guillaume Baudart IBM Research, Louis Mandel IBM Research, Cédric Pasteur , Marc Pouzet École normale supérieure | ||
13:30 - 14:30 | |||
13:30 25mFull-paper | iDeA: An Immersive Debugger for Actors Erlang A: Aman Shankar Mathur MPI-SWS, Germany, A: Burcu Kulahcioglu Ozkan MPI-SWS, Germany, A: Rupak Majumdar MPI-SWS, Germany DOI | ||
13:55 25mFull-paper | Automatic Detection of Core Erlang Message Passing Errors Erlang DOI | ||
14:20 10mCoffee break | 10 min Coffee break Erlang | ||
13:30 - 15:10 | |||
13:30 25mResearch paper | Programming-by-Example for Audio: Synthesizing Digital Signal Processing Programs FARM Mark Santolucito Yale University, USA, Kate Rogers Yale University, USA, Aedan Lombardo Yale University, USA, Ruzica Piskac Yale University, USA DOI Pre-print | ||
13:55 25mTalk | Call For Collaboration: The Vecosek Ecosystem FARM Sebastien Mondet Mount Sinai - Hammer Lab | ||
14:20 25mDemonstration | Musical Steganography: Hiding Things in Music FARM Scott Fradkin Flexion | ||
14:45 25mDemonstration | (Ab)using a monadic screen-presentation EDSL as a just-intonation synth pad controller FARM Justus Sagemüller Universität zu Köln, Institut für Geophysik und Meteorologie | ||
13:30 - 15:10 | |||
13:30 45mTalk | An Efficient Compiler for Recursive Functions on Mostly-Serialized Data FHPC A: Michael Vollmer Indiana University, USA, A: Chaitanya S. Koparkar Indiana University, A: Laith Sakka Purdue University, A: Milind Kulkarni Purdue University, A: Ryan R. Newton Indiana University | ||
14:15 45mTalk | Comparing strategies for lightweight threading based on continuations FHPC | ||
14:10 - 14:30 | |||
14:10 20mCoffee break | Saturday coffee break 3 Catering | ||
14:30 - 15:10 | |||
14:30 25mFull-paper | Modelling Distributed Erlang within a Single Node Erlang A: Stavros Aronis Erlang Solutions, Sweden, A: Viktória Fördős Klarna Bank, Sweden, A: Dániel Szoboszlay Klarna Bank, Sweden DOI | ||
14:55 15mShort-paper | Modeling Erlang Processes as Petri Nets Erlang A: Jörgen Brandt Humboldt-Universität zu Berlin, Germany, A: Wolfgang Reisig Humboldt-Universität zu Berlin, Germany DOI | ||
15:10 - 15:30 | |||
15:10 20mCoffee break | Saturday coffee break 4 Catering | ||
15:30 - 16:10 | |||
15:30 25mFull-paper | Typing the Wild in Erlang Erlang A: Nachiappan Valliappan Chalmers University of Technology, Sweden, A: John Hughes Chalmers University of Technology, Sweden DOI | ||
15:55 15mDay closing | Farewell & Closing Erlang | ||
15:30 - 16:10 | |||
15:30 25mResearch paper | Abstract Nonsense FARM April Gonçalves Roskilde University, Denmark DOI | ||
15:55 15mDay closing | Closing FARM | ||
15:30 - 17:00 | |||
15:30 45mTalk | Optimizing Data Parallelism with Linear Programming in Nessie FHPC | ||
16:15 45mDay closing | Optional Discussion FHPC | ||
19:30 - 21:30 | |||
19:30 2hSocial Event | FARM Evening of Algorithmic Arts Social Events | ||