Filter Program
Conference Dates
Conference Dates are in time zone (GMT-05:00) Guadalajara, Mexico City, Monterrey, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
Conference DaySun 23 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Sun 23 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | |||
09:00 60mTalk | A preview of a tutorial on L (polarized μμ̃) HOPE Kenji MaillardInria Paris and ENS Paris, Étienne MiqueyINRIA, Xavier MontilletINRIA, Guillaume Munch-MaccagnoniInria, Gabriel SchererINRIA Saclay | ||
09:00 - 10:00 | |||
09:00 5mDay opening | Welcome to HIW HIW Joachim BreitnerDFINITY Foundation | ||
09:05 55mTalk | Invited Talk: Let’s Go Mainstream with Eta! HIW Rahul MuttineniTypeLead Media Attached | ||
09:00 - 10:00 | |||
09:00 30mTalk | What an SMT solver can do for you PLMW @ ICFP Nadia PolikarpovaUniversity of California, San Diego | ||
09:30 30mTalk | Gradual Types PLMW @ ICFP Ronald GarciaUniversity 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 ArntzeniusUniversity of Birmingham, UK | ||
10:20 - 12:00 | |||
10:20 25mTalk | GHC Update HIW Simon Peyton JonesMicrosoft, UK File Attached | ||
10:45 25mTalk | Source Plugins HIW Matthew PickeringUniversity of Bristol Media Attached | ||
11:10 25mTalk | Generalized Abstract GHC.Generics HIW Ryan ScottIndiana University at Bloomington, USA File Attached | ||
11:35 8mTalk | Lightning talk: CodeWorld: Teaching Haskell and mathematics to children HIW Chris SmithGoogle, 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élineauSimSpace 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 MillerCarnegie 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 GoncharovFriedrich-Alexander-Universität Erlangen-Nürnberg, Christoph RauchFAU Erlangen-Nürnberg, Lehrstuhl 8, Lutz SchöderFAU 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 NguyenBryn 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 RussellSimSpace Link to publication File Attached | ||
14:53 8mTalk | Lightning talk: Asterius: Bringing Haskell to WebAssembly HIW Cheng ShaoTweag 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 JonesMicrosoft, UK | ||
14:03 33mTalk | Dependent Types PLMW @ ICFP Stephanie WeirichUniversity of Pennsylvania, USA | ||
14:36 34mTalk | An opinionated talk on how to give talks PLMW @ ICFP Ranjit JhalaUniversity 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 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 BaaijQBayLogic B.V. File Attached | ||
16:20 8mTalk | Lightning talk: More Explicit Foralls in GHC HIW | ||
16:28 17mOther | GHC Community Discussion HIW Simon Peyton JonesMicrosoft, UK | ||
15:30 - 16:30 | |||
15:30 60mTalk | Panel Discussion: Research in Functional Programming PLMW @ ICFP Alejandro RussoChalmers University of Technology, Sweden, Katie OtsFacebook, Leonidas LampropoulosUniversity of Pennsylvania, David DaraisUniversity of Vermont, Ivan PerezNational Institute of Aerospace, USA | ||
Conference DayMon 24 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Mon 24 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Monday KeynoteKeynotes and Reports at Stifel Theatre Chair(s): Robby FindlerNorthwestern University, USA | ||
09:00 60mTalk | Gradual Typing Keynotes and Reports Ronald GarciaUniversity 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 RussoChalmers 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 ZhangUniversity of Pennsylvania, Leonidas LampropoulosUniversity 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 NandiUniversity of Washington, USA, James R. WilcoxUniversity of Washington, Taylor BlauUniversity of Washington, Dan GrossmanUniversity of Washington, Zachary TatlockUniversity 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 MorrisUniversity 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 AllaisRadboud University Nijmegen, Robert AtkeyUniversity 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 ElsmanUniversity 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čevacTU Darmstadt, Nada AminUniversity of Cambridge, Guido SalvaneschiTU Darmstadt, Sebastian ErdwegDelft University of Technology, Netherlands, Patrick EugsterPurdue University, Mira MeziniTU 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 SperberActive Group GmbH | ||
16:40 22mTalk | The Simple Essence of Automatic DifferentiationDistinguished Paper Research Papers Conal ElliottTarget, USA DOI | ||
17:02 22mTalk | Functional Programming for Modular Bayesian Inference Research Papers Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Ohad KammarUniversity of Oxford, Zoubin GhahramaniUniversity of Cambridge DOI | ||
17:25 22mTalk | Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion Research Papers Mitchell WandNortheastern University, USA, Ryan CulpepperCzech Technical University, Theophilos GiannakopoulosBAE Systems, Inc., Andrew CobbNortheastern University DOI | ||
17:47 22mTalk | Teaching How to Program using Automated Assessment and Functional Glossy Games (Experience Report) Research Papers José Bacelar AlmeiraUniversity of Minho & INESC TEC, Alcino CunhaUniversity of Minho and INESC TEC, Portugal, Nuno MacedoUniversity of Minho & INESC TEC, Hugo PachecoUniversity of Minho, Portugal, José ProençaHASLab/INESC TEC & University of Minho DOI | ||
18:30 - 20:30 | |||
18:30 2hSocial Event | SRC Poster Reception Social Events | ||
Conference DayTue 25 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Tue 25 SepDisplayed 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 HanrahanStanford 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 MillerCarnegie 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 ElsmanUniversity of Copenhagen, Denmark, Troels HenriksenUniversity of Copenhagen, Denmark, Danil AnnenkovDepartment of Computer Science, University of Copenhagen, Cosmin OanceaUniversity of Copenhagen, Denmark Link to publication DOI | ||
11:15 22mTalk | Finitary Polymorphism for Optimizing Type-Directed Compilation Research Papers Atsushi OhoriTohoku University, Japan, Katsuhiro UenoTohoku University, Hisayuki MimaTohoku University DOI | ||
11:37 22mTalk | Fault Tolerant Functional Reactive Programming (Functional Pearl) Research Papers Ivan PerezNational 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 VazouUniversity of Maryland, USA | ||
13:00 22mTalk | MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic Research Papers Robbert KrebbersDelft University of Technology, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Ralf JungMPI-SWS, Joseph TassarottiCarnegie Mellon University, Jan-Oliver KaiserMPI-SWS, Amin Timanyimec-Distrinet KU-Leuven, Arthur CharguéraudInria, Derek DreyerMPI-SWS DOI | ||
13:22 22mTalk | Mtac2: Typed Tactics for Backward Reasoning in Coq Research Papers Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET, Robbert KrebbersDelft University of Technology, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Derek DreyerMPI-SWS DOI | ||
13:45 22mTalk | Compositional Soundness Proofs of Abstract Interpreters Research Papers Sven KeidelDelft University of Technology, Netherlands, Casper Bach PoulsenDelft University of Technology, Sebastian ErdwegDelft 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 SwierstraUtrecht University, Netherlands | ||
15:00 22mTalk | What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma (Functional Pearl) Research Papers Guillaume BoisseauUniversity of Oxford, Jeremy GibbonsDepartment of Computer Science, University of Oxford DOI | ||
15:22 22mTalk | Incremental Relational Lenses Research Papers Rudi HornUniversity of Edinburgh, Roly PereraUniversity of Glasgow, James CheneyUniversity of Edinburgh, UK DOI | ||
15:45 22mTalk | Synthesizing Quotient Lenses Research Papers Solomon MainaUniversity of Pennsylvania, Anders MiltnerPrinceton University, Kathleen FisherTufts University, USA, Benjamin C. PierceUniversity of Pennsylvania, Dave WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania DOI | ||
16:07 22mTalk | Generic Deriving of Generic Traversals Research Papers Csongor KissImperial College London, Matthew PickeringUniversity of Bristol, Nicolas WuUniversity 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 FluetRochester Institute of Technology | ||
Conference DayWed 26 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Wed 26 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
09:00 - 10:00 | Wednesday KeynoteKeynotes and Reports at Stifel Theatre Chair(s): Jeremy GibbonsDepartment 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 YallopUniversity of Cambridge, UK, Tamara von GlehnUniversity of Cambridge, Ohad KammarUniversity of Oxford Link to publication DOI Pre-print | ||
10:52 22mTalk | Relational Algebra by Way of AdjunctionsDistinguished Paper Research Papers Jeremy GibbonsDepartment of Computer Science, University of Oxford, Fritz HengleinDepartment of Computer Science, University of Copenhagen (DIKU), Ralf HinzeRadboud University Nijmegen, Nicolas WuUniversity 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 TanterUniversity 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 CamporaULL Lafayette, Sheng ChenUniversity of Louisiana at Lafayette, Eric WalkingshawOregon 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 BreitnerDFINITY Foundation, Antal Spector-Zabusky, Yao LiUniversity of Pennsylvania, Christine RizkallahUniversity of New South Wales, John WiegleyBAE Systems, Stephanie WeirichUniversity 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 SergeyUniversity College London | ||
15:00 23mTalk | Parallel Complexity Analysis with Temporal Session Types Research Papers Ankush DasCarnegie Mellon University, Jan HoffmannCarnegie Mellon University, Frank PfenningCarnegie 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 AccattoliInria & Ecole Polytechnique, Stéphane Graham-LengrandCNRS, France, Delia KesnerIRIF, 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 SinghX, the moonshot factory | ||
17:30 10mAwards | Student Research Competition Awards Keynotes and Reports Ravi ChughUniversity of Chicago | ||
17:40 15mTalk | Program Chair's Report Keynotes and Reports Matthew FlattUniversity of Utah | ||
17:55 5mTalk | ICFP 2019 Announcement Keynotes and Reports Derek DreyerMPI-SWS | ||
17:30 - 17:40 | |||
17:30 10mAwards | Student Research Competition Awards Keynotes and Reports Ravi ChughUniversity 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 | ||
Conference DayThu 27 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Thu 27 SepDisplayed 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 SmirenkoSaint Petersburg State University, Semyon GrigorevSaint-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 MiraldoUtrecht University, Netherlands, Harold CarrOracle Labs, USA, Alex KoganOracle Labs, USA, Mark MoirOracle Labs, New Zealand, Maurice HerlihyBrown University, USA DOI | ||
09:00 - 12:00 | T01: Introduction to Programming and Proving in CedilleTutorials at Burlington Route Chair(s): Aaron StumpThe 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 KennedyFacebook 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 RadanneUniversity of Freiburg, Germany | ||
09:00 - 10:00 | |||
09:00 5mDay opening | Welcome and Chair's Report Haskell Nicolas WuUniversity of Bristol, UK | ||
09:05 55mTalk | Neither Web nor Assembly (Invited Talk) Haskell Andreas RossbergDfinity | ||
09:00 - 10:00 | |||
09:00 60mDay opening | Daisy - a framework for sound accuracy analysis and optimization of numerical programs NPFL Eva DarulovaMPI-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 CalascibettaTarides | ||
10:20 - 12:00 | |||
10:20 25mResearch paper | Typing, Representing, and Abstracting Control: Functional Pearl TyDe Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity 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 MiraldoUtrecht University, Netherlands, Alejandro SerranoUtrecht 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 GibbonsDepartment 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ínezCIFASIS-CONICET, Argentina, Mauro JaskelioffCONICET, Argentina, Guido De LucaUniversidad 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 MondetMount 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): Justin Lubin, Mikaël MayerEPFL, Switzerland, Ravi ChughUniversity of Chicago, Brian HempelUniversity of Chicago | ||
13:00 3hOther | T02: Direct Manipulation Programming in Sketch-n-Sketch Tutorials Nick CollinsUniversity of Chicago, Brian HempelUniversity of Chicago, Ravi ChughUniversity of Chicago, Mikaël MayerEPFL, Switzerland, Justin Lubin | ||
13:30 - 14:10 | |||
13:30 20mTalk | Wall: rendering vector graphics with OCaml and OpenGL OCaml Frédéric BourFacebook Paris | ||
13:50 20mTalk | Winning on Windows: porting the OCaml platform OCaml David AllsoppUniversity 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. LeinoAmazon | ||
13:30 - 14:30 | Talks IIINPFL at Texas Special Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford | ||
13:30 30mTalk | A Haskell Interface to Sundials via inline-c NPFL Dominic SteinitzTweag I/O | ||
14:00 30mTalk | On the Calculation of Functions in the Algebra of Physical Space NPFL Nathan Waiviohttps://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 VazouUniversity of Maryland, USA | ||
14:20 25mResearch paper | First Class Dynamic Effect Handlers: or, Polymorphic Heaps with Dynamic Effect Handlers TyDe Daan LeijenMicrosoft Research, USA DOI | ||
14:45 25mResearch paper | From Algebra to Abstract Machine: A Verified Generic Construction TyDe Carlos Tomé CortiñasUtrecht University, Netherlands, Wouter SwierstraUtrecht University, Netherlands DOI | ||
14:30 - 15:10 | |||
14:30 20mTalk | R&B: Towards bringing functional programming to everyday's web programmer OCaml Hongbo ZhangIndependent, Cristiano CalcagnoFacebook, Jordan WalkeFacebook, Cheng LouFacebook, Ricky VetterFacebook | ||
14:50 20mTalk | MLExplain OCaml Link to publication | ||
14:30 - 15:10 | |||
14:30 40mTalk | Manifolds as Haskell types NPFL Justus SagemüllerUniversitä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 NoonanKataskeue, 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 EremondiUniversity of British Columbia, Wouter SwierstraUtrecht University, Netherlands, Jurriaan HageUtrecht University File Attached | ||
15:30 - 16:10 | |||
15:30 40mTalk | Exact Real Arithmetic for Geometric Operations NPFL Pavel PanchekhaUniversity 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 | ||
Conference DayFri 28 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Fri 28 SepDisplayed 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 HornUniversity of Maryland, USA | ||
09:00 - 10:00 | |||
09:00 60mTalk | Cross-Platform Language Design in Scala.js Scala Sébastien DoeraeneEPFL, 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öndaln.n., n.n., Andres LöhWell-Typed, UK, Ryan ScottIndiana University at Bloomington, USA DOI | ||
09:30 30mTalk | Generic Programming of All Kinds Haskell Alejandro SerranoUtrecht University, Netherlands, Victor Cacciari MiraldoUtrecht University, Netherlands DOI | ||
09:00 - 10:00 | |||
09:00 60mTalk | ELPI: an extension language with binders and unification variables (Invited talk) ML Enrico TassiINRIA | ||
09:00 - 12:00 | T03: Abstracting Gradual Typing: A Systematic Approach to Designing Gradually Typed LanguagesTutorials at Texas Special Chair(s): Ronald GarciaUniversity of British Columbia, Éric TanterUniversity 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 GlecklerSRFI Editor | ||
10:40 20mTalk | Loop Patterns: Extension of Kleene Star Operator for More Powerful Pattern Matching against Arbitrary Data Structures Scheme Satoshi EgiRakuten 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 DolanUniversity of Cambridge | ||
10:45 25mTalk | Rust Distilled: An Expressive Tower of Languages ML Aaron WeissNortheastern University, Daniel PattersonNortheastern University, Amal AhmedNortheastern 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 ElsmanUniversity of Copenhagen, Denmark, Philip MunksgaardIntelligent Alpha AG, Switzerland, Ken Friis LarsenDIKU, University of Copenhagen Link to publication | ||
10:30 - 12:00 | |||
10:30 30mTalk | Type Variables in Patterns Haskell Richard A. EisenbergBryn Mawr College, USA, Joachim BreitnerDFINITY Foundation, Simon Peyton JonesMicrosoft, 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 GissurarsonChalmers 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 | ||
11:50 - 12:10 | |||
11:50 10mTalk | Julia Subtyping Lessons Scala Could Learn (Student Talk) Scala Artem PelenitsynNortheastern 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 ErringtonMcGill University, Aliya HameerMcGill University, Brigitte PientkaMcGill University | ||
13:00 3hTalk | T04: Beluga: Programming Proofs About Formal Systems Tutorials Brigitte PientkaMcGill University, Jacob Thomas ErringtonMcGill University, Aliya HameerMcGill 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 VerbitskaiaSaint Petersburg State University, Russia, Ilya KirillovSaint Petersburg State University, Russia, Ilya NozkinSaint Petersburg State University, Russia, Semyon GrigorevSaint Petersburg State University, Russia DOI | ||
14:17 22mTalk | Truly Abstract Interfaces for Algebraic Data Types: The Extractor Typing Problem Scala Nicolas StuckiEPFL, Switzerland, Paolo G. GiarrussoEPFL, Switzerland, Martin OderskyEPFL, Switzerland DOI | ||
13:30 - 14:10 | |||
13:30 20mTalk | Racets: Faceted Execution in Racket Scheme Kristopher MicinskiHaverford College, Zhanpeng WangHaverford College, USA, Thomas GilrayUniversity of Maryland | ||
13:50 20mTalk | An Efficient Compiler for the Gradually Typed Lambda Calculus Scheme Andre KuhlenschmidtIndiana University, Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA | ||
13:30 - 15:00 | |||
13:30 30mTalk | A Promise Checked Is a Promise Kept: Inspection Testing Haskell Joachim BreitnerDFINITY Foundation DOI | ||
14:00 30mTalk | Branching Processes for QuickCheck Generators Haskell Agustín MistaUniversidad Nacional de Rosario, Argentina, Alejandro RussoChalmers University of Technology, Sweden, John HughesChalmers 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ínezCIFASIS-CONICET, Argentina, Danel AhmanUniversity of Ljubljana, Victor Dumitrescu, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Cătălin HriţcuInria Paris, Monal Narasimhamurthy, Zoe ParaskevopoulouPrinceton University, Clément Pit-ClaudelMIT CSAIL, Jonathan ProtzenkoMicrosoft Research, Redmond, Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research File Attached | ||
13:55 25mTalk | Design and verification of functional proof checkers ML Roberto BlancoInria | ||
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 HolkGoogle | ||
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 MartresEPFL, 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 ErdwegDelft University of Technology, Netherlands | ||
15:20 22mTalk | A Domain-specific Language for Microservices Scala Jacob DonhamTwitter, Inc. DOI | ||
15:42 28mIndustry talk | SemanticDB: a common data model for Scala developer tools Scala Eugene BurmakoTwitter, Inc. | ||
15:30 - 16:10 | |||
15:30 40mTalk | Rebuilding Racket on Chez Scheme: An Experience Report Scheme Matthew FlattUniversity of Utah | ||
15:30 - 16:00 | |||
15:30 29mTalk | Theorem Proving for All: Equational Reasoning in Liquid Haskell (Functional Pearl) Haskell Niki VazouUniversity of Maryland, USA, Joachim BreitnerDFINITY Foundation, Rose KunkelUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA, Graham HuttonUniversity of Nottingham, UK DOI | ||
15:59 1mTalk | Closing Statement Haskell Nicolas WuUniversity of Bristol, UK | ||
15:30 - 16:10 | |||
15:30 40mTalk | Programming with Abstract Algebraic Effects ML Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław | ||
16:30 - 17:20 | |||
16:30 50mTalk | Strange Loop Keynote: Machine learning failures - for art! Keynotes and Reports | ||
Conference DaySat 29 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Conference Day
Sat 29 SepDisplayed 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 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): Eric MertensGalois, Inc., Jose CalderonGalois, 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ãoPolytechnic 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 SperberActive Group GmbH | ||
09:00 3hOther | T05: Purely functional UIs with Reacl Tutorials Michael SperberActive 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 HackettUniversity of Nottingham, UK DOI | ||
10:45 25mDemonstration | Chord Progressions in Haskell FARM Brittni WatkinsSouthern Methodist University | ||
11:10 25mDemonstration | Pattern-Based Algorithmic Music with Euterpea FARM Donya QuickStevens 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 HenriksenUniversity of Copenhagen, Denmark, A: Martin ElsmanUniversity of Copenhagen, Denmark, A: Cosmin OanceaUniversity 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 GerdesUniversity of Gothenburg, Sweden, A: John HughesChalmers University of Technology, Sweden, A: Nicholas SmallboneChalmers University of Technology, Sweden, A: Stefan HanenbergUniversity of Duisburg-Essen, Germany, A: Sebastian IvarssonChalmers University of Technology, Sweden, A: Meng WangUniversity 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 SerranoInria, France | ||
13:00 3hOther | T10: Hop.js: JavaScript multitier programming Tutorials Manuel SerranoInria, France | ||
13:00 - 16:00 | T08: Implement your own reactive language: the ReactiveML experimentTutorials at Wabash Cannonball Chair(s): Louis MandelIBM Research, Marc PouzetÉcole normale supérieure, Cédric Pasteur, Guillaume BaudartIBM Research | ||
13:00 3hOther | T08: Implement your own reactive language: the ReactiveML experiment Tutorials Guillaume BaudartIBM Research, Louis MandelIBM 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 MathurMPI-SWS, Germany, A: Burcu Kulahcioglu OzkanMPI-SWS, Germany, A: Rupak MajumdarMPI-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 SantolucitoYale University, USA, Kate RogersYale University, USA, Aedan LombardoYale University, USA, Ruzica PiskacYale University, USA DOI Pre-print | ||
13:55 25mTalk | Call For Collaboration: The Vecosek Ecosystem FARM Sebastien MondetMount Sinai - Hammer Lab | ||
14:20 25mDemonstration | Musical Steganography: Hiding Things in Music FARM Scott FradkinFlexion | ||
14:45 25mDemonstration | (Ab)using a monadic screen-presentation EDSL as a just-intonation synth pad controller FARM Justus SagemüllerUniversitä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 VollmerIndiana University, USA, A: Chaitanya KoparkarIndiana University, A: Laith SakkaPurdue University, A: Milind KulkarniPurdue University, A: Ryan R. NewtonIndiana 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 AronisErlang Solutions, Sweden, A: Viktória FördősKlarna Bank, Sweden, A: Dániel SzoboszlayKlarna Bank, Sweden DOI | ||
14:55 15mShort-paper | Modeling Erlang Processes as Petri Nets Erlang A: Jörgen BrandtHumboldt-Universität zu Berlin, Germany, A: Wolfgang ReisigHumboldt-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 ValliappanChalmers University of Technology, Sweden, A: John HughesChalmers 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çalvesRoskilde 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 | ||