Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 22 AugDisplayed time zone: Seoul change
Sun 22 Aug
Displayed time zone: Seoul change
16:00 - 17:30 | |||
16:00 30mTalk | Representing Monads with Capabilities HOPE | ||
16:30 30mTalk | Higher-order Programming with Effects and Handlers — with First-Class Functions HOPE Jonathan Immanuel Brachthäuser EPFL, Philipp Schuster University of Tübingen, Edward Lee University of Waterloo, Aleksander Boruch-Gruszecki EPFL | ||
17:00 30mTalk | Computational and Contextual Program Differences: Reasoning About Non-equivalent Effectful Programs in an Higher-Order Scenario HOPE Ugo Dal Lago University of Bologna, Italy / Inria, France, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis | ||
18:00 - 19:30 | |||
18:00 15mDay opening | Welcome to FHPNC 2021 FHPNC | ||
18:15 30mTalk | Generating High Performance Code for Irregular Data Structures using Dependent Types FHPNC Federico Pizzuti University of Edinburgh, Michel Steuwer University of Edinburgh, Christophe Dubach McGill University | ||
18:45 30mTalk | Improving GHC Haskell NUMA Profiling FHPNC Ruairidh Macgregor University of Glasgow, Phil Trinder University of Glasgow, Hans-Wolfgang Loidl Heriot-Watt University, UK | ||
18:00 - 19:30 | |||
18:00 30mTalk | The Functional Machine Calculus HOPE Willem Heijltjes University of Bath | ||
18:30 30mTalk | Formalising Algebraic Effects with Non-Recoverable Failure HOPE Pre-print | ||
19:00 30mTalk | Computational calculus: bridging reduction and evaluation HOPE Claudia Faggian Université de Paris & CNRS, Giulio Guerrieri University of Bath, Riccardo Treglia Università di Torino File Attached | ||
18:00 - 19:30 | |||
18:00 90mTutorial | Deductive Verification of OCaml Programs in Cameleer Tutorials Mário Pereira LRI - Université Paris-Sud | ||
20:00 - 21:30 | |||
20:00 22mTalk | Exact Print Annotations in GHC HIW | ||
20:22 22mTalk | Avoiding quadratic GHC core code size HIW | ||
20:44 22mTalk | Improvements to GHC's parallel garbage collector HIW Douglas Wilson Well Typed | ||
20:00 - 21:30 | |||
20:00 30mTalk | Higher-Order Asynchronous Effects HOPE Danel Ahman University of Ljubljana, Matija Pretnar University of Ljubljana, Slovenia, Janez Radešček University of Ljubljana Pre-print File Attached | ||
20:30 30mTalk | Handler calculus HOPE Sam Lindley The University of Edinburgh, UK File Attached | ||
21:00 30mTalk | A Monad for Shared-State Concurrency HOPE File Attached | ||
20:00 - 21:30 | |||
20:00 90mTutorial | Deductive Verification of OCaml Programs in Cameleer Tutorials Mário Pereira LRI - Université Paris-Sud | ||
20:00 - 21:30 | Session ITyDe at TyDe Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica | ||
20:00 30mTalk | Interactive Haskell Type Inference Exploration (Extended Abstract) TyDe File Attached | ||
20:30 30mTalk | Contextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract) TyDe Kazuki Niimi Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology, Jonathan Immanuel Brachthäuser EPFL File Attached | ||
21:00 30mTalk | Translation Certification for Smart Contracts (Extended Abstract) TyDe Jacco Krijnen Utrecht University, Manuel Chakravarty Tweag & IOHK, Gabriele Keller Utrecht University, Wouter Swierstra Utrecht University, Netherlands File Attached | ||
22:00 - 23:00 | |||
22:00 60mTalk | Is Functional HPC the Key to Low Carbon Computing? by Sven-Bodo Scholz FHPNC | ||
22:00 - 23:30 | |||
22:00 60mTalk | Haskell reinterpreted – large-scale real-world experience with the Mu compiler in Financial Markets HIW Marten Agren Standard Chartered Bank File Attached | ||
22:00 - 23:00 | |||
22:00 15mDay opening | Welcome and Opening Remarks PLMW @ ICFP | ||
22:15 45mTalk | How to Write Papers So People Can Read Them PLMW @ ICFP | ||
22:00 - 23:30 | KeynoteTyDe at TyDe Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica | ||
22:00 60mKeynote | Integrating Agda with SMT-LIB – An incomplete list of pits I fell inTyDe Keynote TyDe Wen Kokke University of Edinburgh | ||
23:15 - 01:00 | |||
23:15 60mPanel | "I don't get it!" Panel PLMW @ ICFP M: Ronald Garcia University of British Columbia, P: Patricia Johann Appalachian State University, P: Norman Ramsey Tufts University, P: Steve Zdancewic University of Pennsylvania, P: Andrew D. Gordon Microsoft Research and University of Edinburgh | ||
00:15 45mTalk | Managing Your Research, Your Advisor, Your Ph.D. PLMW @ ICFP | ||
23:30 - 01:00 | |||
23:30 30mTalk | Parallelism-preserving automatic differentiation for second-order array languages FHPNC Adam Paszke Google Research, Matthew J. Johnson Google Research, Roy Frostig Google Research, Dougal Maclaurin Google Research | ||
00:00 30mTalk | Reverse Automatic Differentiation for Accelerate (Extended Abstract) FHPNC Tom Smeding Utrecht University, Matthijs Vákár Utrecht University, Trevor L. McDonell Utrecht University | ||
00:30 30mTalk | Computing Persistent Homology in Futhark FHPNC Erik von Brömssen Chalmers University of Technology | ||
23:30 - 01:00 | |||
23:30 22mTalk | Generalization is hard, but somebody's got to do it HIW Richard A. Eisenberg Tweag | ||
23:52 22mTalk | A new interface for GHC typechecker plugins and type-family rewriting HIW Sam Derbyshire Tweag Media Attached | ||
00:14 22mTalk | The Dynamic Haskell Plugin for GHC HIW Matthías Páll Gissurarson Chalmers University of Technology, Sweden, Agustín Mista Chalmers University of Technology | ||
00:36 22mTalk | GHC Status update HIW Simon Peyton Jones Microsoft, UK File Attached | ||
23:30 - 01:00 | |||
23:30 30mTalk | First-class Names for Effect Handlers HOPE Ningning Xie University of Toronto, Youyou Cong Tokyo Institute of Technology, Daan Leijen Microsoft Research | ||
00:00 30mTalk | Tensor Partial Evaluation HOPE Eli Bingham Broad Institute, Fritz Obermeyer Broad Institute of MIT and Harvard, Yerdos Ordabayev Brandeis University, Du Phan UIUC File Attached | ||
00:30 30mTalk | Dynamic Scope + Laziness = Counterfactuals HOPE James Koppel Massachusetts Institute of Technology, USA, Armando Solar-Lezama Massachusetts Institute of Technology, Zenna Tavares Massachusetts Institute of Technology, Xin Zhang Peking University File Attached | ||
23:30 - 01:00 | |||
23:30 90mTutorial | Teaching Functional Programming Tutorials Michael Sperber Active Group GmbH | ||
23:30 - 01:00 | |||
23:30 30mTalk | Gradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory (Extended Abstract) TyDe Media Attached File Attached | ||
00:00 30mTalk | A Simpler Encoding of Indexed Types TyDe Tesla Zhang The Pennsylvania State University Link to publication DOI Pre-print Media Attached | ||
00:30 30mTalk | Optics for Generic Declarative Server APIs (Extended Abstract) TyDe Andre Videla University Of Strathclyde Media Attached File Attached | ||
Mon 23 AugDisplayed time zone: Seoul change
Mon 23 Aug
Displayed time zone: Seoul change
01:30 - 03:00 | Community update and discussionFHPNC at FHPNC 45 min community update: brief summary (about 5-7 mins) of current work and future plans from
| ||
01:30 - 03:00 | |||
01:30 22mTalk | Testing Haskell with Mocks HIW | ||
01:52 22mTalk | Adventures in GHC compile times HIW | ||
02:14 7mTalk | Lightning Talk: Pinned Warnings HIW | ||
02:21 7mTalk | Lightning Talk: GSOL: A Confluence Checker for Haskell Rewrite Rules HIW File Attached | ||
01:30 - 03:00 | |||
01:30 90mTutorial | Teaching Functional Programming Tutorials Michael Sperber Active Group GmbH | ||
01:30 - 03:00 | |||
01:30 30mTalk | Actions You Can Handle: Dependent Types for AI Plans TyDe Alasdair Hill Heriot-Watt University, Ekaterina Komendantskaya Heriot-Watt University, UK, Matthew L. Daggitt Heriot-Watt University, Ronald P. A. Petrick Heriot-Watt University DOI Pre-print Media Attached | ||
02:00 30mTalk | Co-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract) TyDe File Attached | ||
02:00 - 03:30 | |||
02:00 45mTalk | Introduction to Mechanized Metatheory PLMW @ ICFP | ||
02:45 45mTalk | Emotional Machines PLMW @ ICFP | ||
03:30 - 05:00 | |||
03:30 22mTalk | Securing Web-Applications with A Refinement Typed ORM HIW Nico Lehmann University of California, San Diego, Rose Kunkel University of California, San Diego, Niki Vazou IMDEA Software Institute, Nadia Polikarpova University of California at San Diego, Deian Stefan University of California at San Diego, USA, Ranjit Jhala University of California at San Diego | ||
03:52 22mTalk | Generics for Hardware: Adding Haskell-inspired Generics to Bluespec HIW | ||
04:14 3mTalk | Closing HIW Ningning Xie University of Toronto | ||
04:00 - 06:15 | |||
04:00 90mOther | Small-group Mentoring Meetings PLMW @ ICFP | ||
05:30 45mTalk | Increasing the Impact of PL Research PLMW @ ICFP | ||
16:15 - 17:45 | |||
16:15 15mLive Q&A | Q&A: Client-Server Sessions in Linear LogicMirror Research Papers | ||
16:30 15mLive Q&A | Q&A: An Order-Aware Dataflow Model for Parallel Unix PipelinesBoth Research Papers | ||
16:45 15mLive Q&A | Q&A: CPS Transformation with Affine Types for Call-By-Value Implicit PolymorphismBoth Research Papers | ||
17:00 15mLive Q&A | Q&A: Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingBoth Research Papers | ||
17:15 15mLive Q&A | Q&A: Propositions-as-Types and Shared StateBoth Research Papers | ||
17:30 15mLive Q&A | Q&A: Efficient Tree-Traversals: Reconciling Parallelism and Dense Data RepresentationsBoth Research Papers | ||
19:00 - 20:45 | Session 2Research Papers at ICFP Talks +12h
| ||
19:00 15mTalk | Contextual Modal Types for Algebraic Effects and Handlers Research Papers DOI Media Attached | ||
19:15 15mTalk | Calculating Dependently-Typed Compilers (Functional Pearl) Research Papers DOI Media Attached | ||
19:30 15mTalk | Reasoning about Effect Interaction by Fusion Research Papers DOI Pre-print Media Attached | ||
19:45 15mTalk | Compositional Optimizations for CertiCoq Research Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI Media Attached | ||
20:00 15mTalk | Generalized Evidence Passing for Effect Handlers Research Papers DOI Media Attached | ||
20:15 15mTalk | Deriving Efficient Program Transformations from Rewrite Rules Research Papers DOI Media Attached | ||
20:30 15mTalk | Algebras for Weighted Search Research Papers DOI Media Attached | ||
19:15 - 21:00 | |||
19:15 15mLive Q&A | Q&A: Contextual Modal Types for Algebraic Effects and HandlersBoth Research Papers | ||
19:30 15mLive Q&A | Q&A: Calculating Dependently-Typed Compilers (Functional Pearl)Main Research Papers | ||
19:45 15mLive Q&A | Q&A: Reasoning about Effect Interaction by FusionMain Research Papers | ||
20:00 15mLive Q&A | Q&A: Compositional Optimizations for CertiCoqMain Research Papers | ||
20:15 15mLive Q&A | Q&A: Generalized Evidence Passing for Effect HandlersMirror Research Papers | ||
20:30 15mLive Q&A | Q&A: Deriving Efficient Program Transformations from Rewrite RulesMirror Research Papers | ||
20:45 15mLive Q&A | Q&A: Algebras for Weighted SearchMain Research Papers | ||
21:30 - 22:00 | |||
21:30 30mLive Q&A | Ask Me Anything on Rust with Ralf Jung Social Events Ralf Jung MPI-SWS | ||
22:00 - 23:00 | |||
22:00 60mKeynote | Fun, Funky, Functional: The Pursuit of Better User Interfaces for Programming Research Papers Ravi Chugh University of Chicago Media Attached | ||
Tue 24 AugDisplayed time zone: Seoul change
Tue 24 Aug
Displayed time zone: Seoul change
00:00 - 01:00 | |||
00:00 60mSocial Event | PL Card Game Social Events Media Attached | ||
01:00 - 01:30 | |||
01:00 30mSocial Event | OCaml at Bloomberg Social Events | ||
04:15 - 05:45 | |||
04:15 15mLive Q&A | Q&A: Client-Server Sessions in Linear LogicMirror Research Papers | ||
04:30 15mLive Q&A | Q&A: An Order-Aware Dataflow Model for Parallel Unix PipelinesBoth Research Papers | ||
04:45 15mLive Q&A | Q&A: CPS Transformation with Affine Types for Call-By-Value Implicit PolymorphismBoth Research Papers | ||
05:00 15mLive Q&A | Q&A: Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingBoth Research Papers | ||
05:15 15mLive Q&A | Q&A: Propositions-as-Types and Shared StateBoth Research Papers | ||
05:30 15mLive Q&A | Q&A: Efficient Tree-Traversals: Reconciling Parallelism and Dense Data RepresentationsBoth Research Papers | ||
06:30 - 07:00 | Ask Me AnythingSocial Events at Social Chair(s): Michael Hicks University of Maryland at College Park | ||
06:30 30mLive Q&A | Ask Me Anything on Climate Change with Benjamin Pierce Social Events Benjamin C. Pierce University of Pennsylvania | ||
07:00 - 08:45 | |||
07:00 15mTalk | Contextual Modal Types for Algebraic Effects and Handlers Research Papers DOI Media Attached | ||
07:15 15mTalk | Calculating Dependently-Typed Compilers (Functional Pearl) Research Papers DOI Media Attached | ||
07:30 15mTalk | Reasoning about Effect Interaction by Fusion Research Papers DOI Pre-print Media Attached | ||
07:45 15mTalk | Compositional Optimizations for CertiCoq Research Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI Media Attached | ||
08:00 15mTalk | Generalized Evidence Passing for Effect Handlers Research Papers DOI Media Attached | ||
08:15 15mTalk | Deriving Efficient Program Transformations from Rewrite Rules Research Papers DOI Media Attached | ||
08:30 15mTalk | Algebras for Weighted Search Research Papers DOI Media Attached | ||
07:15 - 09:00 | |||
07:15 15mLive Q&A | Q&A: Contextual Modal Types for Algebraic Effects and HandlersBoth Research Papers | ||
07:30 15mLive Q&A | Q&A: Calculating Dependently-Typed Compilers (Functional Pearl)Main Research Papers | ||
07:45 15mLive Q&A | Q&A: Reasoning about Effect Interaction by FusionMain Research Papers | ||
08:00 15mLive Q&A | Q&A: Compositional Optimizations for CertiCoqMain Research Papers | ||
08:15 15mLive Q&A | Q&A: Generalized Evidence Passing for Effect HandlersMirror Research Papers | ||
08:30 15mLive Q&A | Q&A: Deriving Efficient Program Transformations from Rewrite RulesMirror Research Papers | ||
08:45 15mLive Q&A | Q&A: Algebras for Weighted SearchMain Research Papers | ||
16:15 - 17:45 | |||
16:15 15mLive Q&A | Q&A: Modular, Compositional, and Executable Formal Semantics for LLVM IRBoth Research Papers | ||
16:30 15mLive Q&A | Q&A: Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program LogicsBoth Research Papers | ||
16:45 15mLive Q&A | Q&A: How to Evaluate Blame for Gradual TypesMirror Research Papers | ||
17:00 15mLive Q&A | Q&A: ProbNV: Probabilistic Verification of Network Control PlanesMirror Research Papers | ||
17:15 15mLive Q&A | Q&A: Of JavaScript AOT Compilation PerformanceMain Research Papers | ||
17:30 15mLive Q&A | Q&A: Symbolic and Automatic Differentiation of LanguagesMirror Research Papers | ||
18:30 - 19:00 | |||
18:30 30mMeeting | SIGPLAN CARES Social Events | ||
18:30 - 19:00 | |||
18:30 30mTalk | SRC Finalist Presentation Student Research Competition | ||
19:15 - 21:00 | |||
19:15 15mLive Q&A | Q&A: How to design co-programs (JFP Presentation)Both Research Papers | ||
19:30 15mLive Q&A | Q&A: A Theory of Higher-Order Subtyping with Type IntervalsBoth Research Papers | ||
19:45 15mLive Q&A | Q&A: Typed dataspace actors (JFP Presentation)Both Research Papers | ||
20:00 15mLive Q&A | Q&A: An Existential Crisis Resolved: Type Inference for First-Class Existential TypesBoth Research Papers | ||
20:15 15mLive Q&A | Q&A: Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)Both Research Papers | ||
20:30 15mLive Q&A | Q&A: Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)Both Research Papers | ||
20:45 15mLive Q&A | Q&A: Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)Both Research Papers | ||
21:30 - 22:00 | |||
21:30 30mLive Q&A | Ask Me Anything on Academic Move with José Pedro Magalhães Social Events José Pedro Magalhães Standard Chartered Bank | ||
22:00 - 23:00 | |||
22:00 60mKeynote | Building PL-Powered Systems for Humans Research Papers Elena Glassman Harvard University | ||
23:00 - 00:00 | |||
23:00 60mDinner | Virtual Dinner Social Events | ||
Wed 25 AugDisplayed time zone: Seoul change
Wed 25 Aug
Displayed time zone: Seoul change
03:00 - 04:00 | |||
03:00 60mLunch | Virtual Lunch Social Events | ||
04:15 - 05:45 | |||
04:15 15mLive Q&A | Q&A: Modular, Compositional, and Executable Formal Semantics for LLVM IRBoth Research Papers | ||
04:30 15mLive Q&A | Q&A: Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program LogicsBoth Research Papers | ||
04:45 15mLive Q&A | Q&A: How to Evaluate Blame for Gradual TypesMirror Research Papers | ||
05:00 15mLive Q&A | Q&A: ProbNV: Probabilistic Verification of Network Control PlanesMirror Research Papers | ||
05:15 15mLive Q&A | Q&A: Of JavaScript AOT Compilation PerformanceMain Research Papers | ||
05:30 15mLive Q&A | Q&A: Symbolic and Automatic Differentiation of LanguagesMirror Research Papers | ||
06:30 - 07:00 | |||
06:30 30mMeeting | SIGPLAN CARES Social Events | ||
06:30 - 07:00 | |||
06:30 30mLive Q&A | Ask Me Anything on Coq with Adam Chlipala Social Events Adam Chlipala Massachusetts Institute of Technology | ||
07:15 - 09:00 | |||
07:15 15mLive Q&A | Q&A: How to design co-programs (JFP Presentation)Both Research Papers | ||
07:30 15mLive Q&A | Q&A: A Theory of Higher-Order Subtyping with Type IntervalsBoth Research Papers | ||
07:45 15mLive Q&A | Q&A: Typed dataspace actors (JFP Presentation)Both Research Papers | ||
08:00 15mLive Q&A | Q&A: An Existential Crisis Resolved: Type Inference for First-Class Existential TypesBoth Research Papers | ||
08:15 15mLive Q&A | Q&A: Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)Both Research Papers | ||
08:30 15mLive Q&A | Q&A: Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)Both Research Papers | ||
08:45 15mLive Q&A | Q&A: Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)Both Research Papers | ||
09:30 - 10:30 | |||
09:30 60mSocial Event | PL Trivia Game Social Events | ||
16:15 - 17:45 | |||
16:15 15mLive Q&A | Q&A: On Continuation-Passing Transformations and Expected Cost AnalysisBoth Research Papers | ||
16:30 15mLive Q&A | Q&A: Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation LogicBoth Research Papers | ||
16:45 15mLive Q&A | Q&A: Automatic Amortized Resource Analysis with the Quantum Physicist’s MethodMirror Research Papers | ||
17:00 15mLive Q&A | Q&A: Theorems for Free from Separation Logic SpecificationsBoth Research Papers | ||
17:15 15mLive Q&A | Q&A: Reasoning about the Garden of Forking PathsBoth Research Papers | ||
17:30 15mLive Q&A | Q&A: Formal Verification of a Concurrent Bounded Queue in a Weak Memory ModelBoth Research Papers | ||
18:30 - 19:00 | |||
18:30 30mLive Q&A | Ask Me Anything on V8 JS Engine with Ben Titzer and Toon Verwaest Social Events | ||
19:15 - 21:00 | |||
19:15 15mLive Q&A | Q&A: Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap FragmentsMirror Research Papers | ||
19:30 15mLive Q&A | Q&A: Grafs: Declarative Graph AnalyticsMirror Research Papers | ||
19:45 15mLive Q&A | Q&A: Certifying the Synthesis of Heap-Manipulating ProgramsBoth Research Papers | ||
20:00 15mLive Q&A | Q&A: Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)Both Research Papers | ||
20:15 15mLive Q&A | Q&A: GhostCell: Separating Permissions from Data in RustBoth Research Papers | ||
20:30 15mLive Q&A | Q&A: Catala: A Programming Language for the LawBoth Research Papers | ||
20:45 15mLive Q&A | Q&A: Persistent Software Transactional Memory in HaskellMain Research Papers | ||
21:30 - 23:00 | |||
21:30 45mTalk | Programming Contest Report Research Papers | ||
22:15 45mTalk | Award Presentations & Chair Report Research Papers Sukyoung Ryu KAIST | ||
23:00 - 00:00 | |||
23:00 60mSocial Event | Industrial Reception Social Events | ||
Thu 26 AugDisplayed time zone: Seoul change
Thu 26 Aug
Displayed time zone: Seoul change
00:00 - 01:00 | |||
00:00 60mDinner | Virtual Dinner Social Events | ||
01:30 - 02:00 | |||
01:30 30mSocial Event | Automated Modernization of Fortran Code at Bloomberg Social Events | ||
03:00 - 04:00 | |||
03:00 60mLunch | Virtual Lunch Social Events | ||
04:15 - 05:45 | |||
04:15 15mLive Q&A | Q&A: On Continuation-Passing Transformations and Expected Cost AnalysisBoth Research Papers | ||
04:30 15mLive Q&A | Q&A: Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation LogicBoth Research Papers | ||
04:45 15mLive Q&A | Q&A: Automatic Amortized Resource Analysis with the Quantum Physicist’s MethodMirror Research Papers | ||
05:00 15mLive Q&A | Q&A: Theorems for Free from Separation Logic SpecificationsBoth Research Papers | ||
05:15 15mLive Q&A | Q&A: Reasoning about the Garden of Forking PathsBoth Research Papers | ||
05:30 15mLive Q&A | Q&A: Formal Verification of a Concurrent Bounded Queue in a Weak Memory ModelBoth Research Papers | ||
06:30 - 07:00 | |||
06:30 30mLive Q&A | Ask Me Anything on Mentoring with Talia Ringer Social Events Talia Ringer University of Illinois at Urbana-Champaign | ||
07:15 - 09:00 | |||
07:15 15mLive Q&A | Q&A: Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap FragmentsMirror Research Papers | ||
07:30 15mLive Q&A | Q&A: Grafs: Declarative Graph AnalyticsMirror Research Papers | ||
07:45 15mLive Q&A | Q&A: Certifying the Synthesis of Heap-Manipulating ProgramsBoth Research Papers | ||
08:00 15mLive Q&A | Q&A: Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)Both Research Papers | ||
08:15 15mLive Q&A | Q&A: GhostCell: Separating Permissions from Data in RustBoth Research Papers | ||
08:30 15mLive Q&A | Q&A: Catala: A Programming Language for the LawBoth Research Papers | ||
08:45 15mLive Q&A | Q&A: Persistent Software Transactional Memory in HaskellMain Research Papers | ||
18:00 - 19:30 | |||
18:00 30mTalk | Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming ML Daniel Hillerström The University of Edinburgh Pre-print Media Attached | ||
18:30 30mTalk | Cameleer: a Deductive Verification Tool for OCaml ML Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS File Attached | ||
19:00 30mTalk | Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques ML Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Trinity College Dublin, Nikos Tzevelekos Queen Mary University of London File Attached | ||
20:00 - 21:30 | |||
20:00 10mDay opening | Welcome Erlang | ||
20:10 30mTalk | Graft: General Purpose Raft Consensus in Elixir Erlang Matthew Alan Le Brun University of Malta, Duncan Paul Attard University of Malta, Adrian Francalanza University of Malta DOI | ||
20:40 30mTalk | Makina: A New QuickCheck State Machine Library Erlang Luis Eduardo Bueso de Barrio Universidad Politécnica de Madrid, Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Clara Benac Earle Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid DOI | ||
21:10 10mVision and Emerging Results | Lightning Talk: Expected Application of BeamAsm Erlang Susumu Yamazaki Univ. of Kitakyushu | ||
21:20 10mVision and Emerging Results | Lightning Talk: QuadBlockQuiz – Supply Chain Edition Erlang Duncan Sparrell sFractal Consulting | ||
20:00 - 21:30 | |||
20:00 30mTalk | Chesskell: A Two-Player Game at the Type Level Haskell | ||
20:30 30mTalk | Express: applications of dynamically typed Haskell expressions Haskell Rudy Matela Unaffiliated Link to publication DOI Pre-print | ||
21:00 30mTalk | Haskell⁻¹: Automatic Function Inversion in Haskell Haskell Finn Teegen University of Kiel, Germany, Kai-Oliver Prott University of Kiel, Germany, Niels Bunkenburg University of Kiel, Germany DOI Pre-print | ||
20:00 - 21:30 | |||
20:00 30mTalk | Formalizing OCaml GADT typing in Coq ML Pre-print File Attached | ||
20:30 30mTalk | Demo Paper : Coqlex, an approach to generate verified lexers ML Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole Polytechnique Media Attached File Attached | ||
21:00 30mTalk | Code Extraction from Coq to ML-like languages ML Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus University Link to publication File Attached | ||
20:00 - 21:30 | Session AminiKanren at miniKanren Chair(s): William E. Byrd University of Alabama at Birmingham, USA | ||
20:00 5mDay opening | Opening Remarks miniKanren | ||
20:05 30mPaper | A Complexity Study for Interleaving Search miniKanren Pre-print Media Attached | ||
20:35 30mPaper | metaKanren: Towards a Metacircular Relational Interpreter miniKanren Pre-print Media Attached | ||
21:05 25mPaper | A New Higher-order Unification Algorithm for λKanren miniKanren Pre-print Media Attached | ||
22:00 - 23:30 | |||
22:00 60mKeynote | Fifteen Years of Successfully Dialyzing Erlang and Elixir Code (Keynote) Erlang Konstantinos (Kostis) Sagonas Uppsala University, Sweden | ||
23:00 10mVision and Emerging Results | Lightning Talk: Using Regular Expressions in Erlang Erlang | ||
23:10 10mVision and Emerging Results | Lightning Talk: eigr.io — A Serverless Runtime on the BEAM Erlang Marcel Lanz eigr.io – Member | ||
22:00 - 23:30 | |||
22:00 90mKeynote | Why Functional Programming with Linear Types Matters Haskell | ||
22:00 - 23:30 | |||
22:00 60mKeynote | Keynote: Narratives and Lessons from The Early History of F# ML Don Syme Microsoft | ||
22:00 - 23:30 | |||
22:00 60mKeynote | Adventures in extending miniKanren miniKanren Nada Amin Harvard University Media Attached | ||
23:30 - 01:00 | |||
23:30 30mTalk | Detecting Oxbow Code in Erlang Codebases with the Highest Degree of Certainty Erlang DOI | ||
00:00 30mTalk | Bidirectional Typing for Erlang Erlang Nithin Vadukkumchery Rajendrakumar TU Kaiserslautern, Annette Bieniusa Technische Universität Kaiserslautern DOI | ||
00:30 10mVision and Emerging Results | Lightning Talk: Experience teaching Erlang/Elixir on YouTube Erlang Adolfo Neto Federal University of Technology - Paraná | ||
00:40 10mVision and Emerging Results | Lightning Talk: AtomVM: A flyweight BEAM for microcontrollers Erlang | ||
23:30 - 01:00 | |||
23:30 30mTalk | Design Patterns for Parser Combinators (Functional Pearl) Haskell | ||
00:00 30mTalk | Graded Monads and Type-Level Programming for Dependence Analysis Haskell | ||
00:30 30mTalk | Chair Report Haskell Jurriaan Hage Utrecht University, Netherlands | ||
23:30 - 01:00 | |||
23:30 30mTalk | A metalanguage for multi-phase modularity ML File Attached | ||
00:00 30mTalk | Unfolding ML datatype declarations without loops ML Pre-print Media Attached | ||
00:30 30mTalk | Verifying Multiparty Communication Protocols using ML Type Systems ML Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University File Attached | ||
23:30 - 01:00 | |||
23:30 90mTutorial | Interaction laws of monads and comonads Tutorials Pre-print | ||
23:30 - 01:00 | |||
23:30 30mPaper | Prolog-Style Meta-Programming miniKanren miniKanren Nada Amin Harvard University, William E. Byrd University of Alabama at Birmingham, USA, Tiark Rompf Purdue University Pre-print Media Attached | ||
00:00 30mPaper | Guarded Fresh Goals: Dependency-Directed Introduction of Fresh Logic Variables miniKanren Evan Donahue University of Tokyo Pre-print Media Attached | ||
00:30 30mPaper | Universal Quantification and Implication in miniKanren miniKanren Ende Jin , Gregory Rosenblatt University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School, Lisa Zhang University of Toronto Mississauga Pre-print Media Attached | ||
Fri 27 AugDisplayed time zone: Seoul change
Fri 27 Aug
Displayed time zone: Seoul change
01:30 - 03:00 | |||
01:30 30mTalk | What Are the Critical Security Flaws in My System? Erlang Viktória Fördős Cisco Systems DOI | ||
02:00 30mTalk | The Hera Framework for Fault-Tolerant Sensor Fusion with Erlang and GRiSP on an IoT Network Erlang Sébastien Kalbusch Université Catholique de Louvain, Vincent Verpoten Université Catholique de Louvain, Peter Van Roy Université catholique de Louvain DOI | ||
02:30 10mVision and Emerging Results | Lightning Talk: The debugging tool that comes with Erlang/OTP I just learned exists after many years of using Erlang Erlang Peer Stritzinger Peer Stritzinger GmbH | ||
02:40 10mVision and Emerging Results | More lightning talks Erlang | ||
01:30 - 03:00 | |||
01:30 30mTalk | Frozen inference constraints for type-directed disambiguation ML Pre-print Media Attached | ||
02:00 15mTalk | Experience Report: Domain Modeling with F# (short talk) ML Scott Wlaschin None Media Attached File Attached | ||
02:15 15mTalk | Isomorphisms are back! (short talk) ML File Attached | ||
02:30 15mTalk | Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk) ML Allister Beharry None Media Attached File Attached | ||
02:45 15mTalk | A Data-centered User Study for jsCoq (short talk) ML Hanneli Tavante McGill University File Attached | ||
01:30 - 03:00 | |||
01:30 90mTutorial | Interaction laws of monads and comonads Tutorials Pre-print | ||
01:30 - 03:00 | |||
01:30 90mTutorial | Programming with Effect Handlers and FBIP in Koka Tutorials | ||
01:30 - 03:00 | Afternoon Keynote and Session CminiKanren at miniKanren Chair(s): Gregory Rosenblatt University of Alabama at Birmingham, USA | ||
01:30 60mKeynote | Relational Content Generation miniKanren Chris Martens North Carolina State University Media Attached | ||
02:30 25mPaper | Relational Floating-Point Arithmetic miniKanren Lucas Sandre University of Toronto Mississauga, Malaika Zaidi University of Toronto Mississauga, Lisa Zhang University of Toronto Mississauga Pre-print Media Attached | ||
02:55 5mDay closing | Closing Remarks miniKanren | ||
03:30 - 05:00 | |||
03:30 90mTutorial | Programming with Effect Handlers and FBIP in Koka Tutorials | ||
16:00 - 17:30 | |||
16:00 30mTalk | GopCaml: A Structural Editor for OCaml OCaml Kiran Gopinathan National University of Singapore File Attached | ||
16:30 30mTalk | OCaml and Python: Getting the Best of Both Worlds OCaml Laurent Mazare Jane Street | ||
17:00 30mTalk | Adapting the OCaml ecosystem for Multicore OCaml OCaml Sudha Parimala Segfault Systems, Enguerrand Decorne Tarides, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, KC Sivaramakrishnan IIT Madras File Attached | ||
18:00 - 19:30 | |||
18:00 30mDay opening | Welcome FARM | ||
18:30 30mTalk | mimium: a self-extensible programming language for sound and music FARM Link to publication DOI Pre-print | ||
19:00 30mTalk | MidifilePerformer: a case study for chronologies FARM Juliette Chabassier Inria, Myriam Desainte-Catherine LaBRI, Jean Haury Scrime, Marin Pobel Université de Bordeaux, Bernard Serpette Inria | ||
18:00 - 19:30 | |||
18:00 30mTalk | Deductive Verification of Realistic OCaml Code OCaml Carlos Pinto NOVA LINCS & Universidade da Beira Interior, Portugal, Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, Simão Melo de Sousa NOVA LINCS & Universidade da Beira Interior, Portugal | ||
18:30 20mTalk | Parafuzz: Coverage-guided Property Fuzzing for Multicore OCaml programs OCaml Sumit Padhiyar Indian Institue Of Technology, Madras, Adharsh Kamath National Institute of Technology Karnataka, Surathkal, India, KC Sivaramakrishnan IIT Madras Media Attached File Attached | ||
18:50 20mTalk | Wibbily Wobbly Timey Camly OCaml | ||
19:10 20mTalk | Leveraging Formal Specifications to Generate Fuzzing Suites OCaml Nicolas Osborne Tarides, Clément Pascutto Tarides, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF | ||
20:00 - 21:30 | |||
20:00 30mTalk | Temporal-Scope Grammars for Polyphonic Music Generation FARM | ||
20:30 30mTalk | The W-calculus: A Synchronous Framework for the Verified Modelling of Digital Signal Processing Algorithms FARM Emilio Jesús Gallego Arias INRIA, Pierre Jouvelot MINES ParisTech, PSL University, Sylvain Ribstein Université Paris 7 Diderot, Dorian Desblancs École normale supérieure Paris-Saclay | ||
21:00 30mTalk | Human-in-the-loop Program Synthesis for Live Coding FARM Mark Santolucito Barnard College, Columbia University, USA Pre-print | ||
20:00 - 21:30 | |||
20:00 30mTalk | Practical Normalization by Evaluation for EDSLs Haskell Nachiappan Valliappan Chalmers University of Technology, Sweden, Alejandro Russo Chalmers University of Technology, Sweden, Sam Lindley The University of Edinburgh, UK | ||
20:30 30mTalk | Safe Mutation with Algebraic Effects Haskell | ||
21:00 30mTalk | Seeking Stability by being Lazy and Shallow: Lazy and shallow instantiation is user friendly Haskell | ||
20:00 - 21:30 | |||
20:00 30mTalk | Probabilistic resource limits, or: Programming with interrupts in OCaml OCaml | ||
20:30 20mTalk | Continuous Benchmarking for Ocaml Projects OCaml | ||
20:50 20mTalk | A Multiverse of Glorious Documentation OCaml File Attached | ||
21:10 20mTalk | Digodoc and Docs OCaml Mohamed Hernouf OCamlPro, Fabrice Le Fessant OCamlPro, Thomas Blanc OCamlPro, Louis Gesbert OCamlPro | ||
20:00 - 21:30 | |||
20:00 30mFull-paper | Is Space-Efficient Polymorphic Gradual Typing Possible? Scheme Shota Ozaki , Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan Pre-print | ||
20:30 30mTalk | Design with Blocks, Code in Text (Lightning Talk) Scheme Junya Nose Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology | ||
21:00 30mDemonstration | GRASP: A GRAphical Scheme Programming environment (Lightning Talk) Scheme | ||
22:00 - 23:30 | |||
22:00 20mOther | Performance: Logical Soundness FARM John Leo Halfaya Research | ||
22:20 20mOther | Performance: Can One Hear the Shape of a Marble Drum? FARM | ||
22:40 20mOther | Performance: Homotopy FARM | ||
22:00 - 23:30 | |||
22:00 90mKeynote | Linear Haskell, Today and Tomorrow Haskell | ||
22:00 - 23:30 | |||
22:00 60mKeynote | 25 years of OCaml OCaml Xavier Leroy Collège de France | ||
22:00 - 23:30 | |||
22:00 60mTalk | Scheme as a framework for Deep Learning (Invited Talk) Scheme Jeffrey Mark Siskind Elmore Family School of Electrical and Computer Engineering, Purdue University | ||
22:00 - 23:00 | |||
22:00 60mSocial Event | ShutdownPL Social Events Justin Lubin University of California, Berkeley, Niki Carroll George Mason University, Alan Jeffrey Roblox, David Justo Microsoft | ||
23:30 - 01:00 | |||
23:30 60mKeynote | Keynote FARM | ||
23:30 - 01:00 | |||
23:30 30mTalk | Deadlock-Free Session Types in Linear Haskell Haskell | ||
00:00 30mTalk | Evaluating Linear Functions to Symmetric Monoidal Categories Haskell DOI Pre-print | ||
00:30 30mTalk | This is not really a talk, but should ensure the two talks before it are 30 min. long Haskell | ||
23:30 - 01:00 | |||
23:30 30mTalk | Experiences with Effects OCaml Thomas Leonard OCaml Labs, Craig Ferguson Tarides, Patrick Ferris OCaml Labs, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, KC Sivaramakrishnan IIT Madras, Anil Madhavapeddy University of Cambridge, UK File Attached | ||
00:00 30mTalk | Opam-bin: Binary Packages with Opam OCaml Fabrice Le Fessant OCamlPro File Attached | ||
00:30 30mTalk | Love: a readable language interpreted by a blockchain OCaml | ||
23:30 - 01:00 | |||
23:30 30mTalk | Adding AD to Scheme by Differentiating the Interpreter Scheme Mehrdad Maleki Mastercard Labs, Barak A. Pearlmutter Maynooth University, Jeffrey Mark Siskind Elmore Family School of Electrical and Computer Engineering, Purdue University | ||
00:00 30mTalk | A lightweight approach for accessing Python modules from Gambit Scheme (Lightning Talk) Scheme | ||
00:30 30mTalk | Graphite: A Library for Data Visualization (Lightning Talk) Scheme | ||
23:30 - 01:00 | |||
23:30 90mTutorial | Functional Software Architecture Tutorials Michael Sperber Active Group GmbH | ||
Sat 28 AugDisplayed time zone: Seoul change
Sat 28 Aug
Displayed time zone: Seoul change
01:30 - 03:00 | |||
01:30 30mTalk | From 2n+1 to n OCaml File Attached | ||
02:00 20mTalk | Property-Based Testing for OCaml through Coq OCaml Paaras Bhandari University of Maryland, College Park, Leonidas Lampropoulos University of Maryland, College Park | ||
02:20 20mTalk | Safe Protocol Updates via Propositional Logic OCaml Michael O'Connor Jane Street | ||
01:30 - 03:00 | |||
01:30 30mFull-paper | Scheduling Musical Events in Max/MSP with Scheme For Max Scheme Iain Duncan University of Victoria Pre-print | ||
02:00 30mFull-paper | So You Want To Analyze Scheme Programs With Datalog? Scheme Davis Silverman Syracuse University, USA, Yihao Sun Syracuse University, Kristopher Micinski Syracuse University, Thomas Gilray University of Alabama at Birmingham Pre-print | ||
02:30 30mFull-paper | Prototypes: Object-Orientation, Functionally Scheme François-René Rideau Mutual Knowledge Systems, Inc., Alex Knauth Mutual Knowledge Systems, Inc., Nada Amin Harvard University Pre-print | ||
01:30 - 03:00 | |||
01:30 90mTutorial | Functional Software Architecture Tutorials Michael Sperber Active Group GmbH | ||
03:30 - 05:00 | |||
03:30 30mTalk | Binary Analysis Platform (BAP). Using Universal Algebra and Tagless-Final Style for Developing Representation-Agnostic Frameworks OCaml File Attached | ||
04:00 20mTalk | Semgrep, a fast, lightweight, polyglot, static analysis tool to find bugs OCaml Yoann Padioleau Return to Corp File Attached | ||
03:30 - 05:00 | |||
03:30 30mTalk | Large Scheme: 'Tis Seven Years Since (Invited Talk) Scheme John Cowan R7RS Editor | ||
04:00 60mTalk | Layering: The Architecture of Programs (Invited Talk) Scheme | ||