Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 11 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Sun 11 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
08:00 - 09:00 | RegistrationCatering & social at Foyer 2 +120h +48h +96h +72h All speakers speaking in the morning session should arrive early to submit the slides. We recommend that you arrive already at 8:00. | ||
08:00 60mRegistration | Registration Catering & social | ||
09:00 - 10:30 | TyDe 1TyDe at Club CD Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica | ||
09:00 18mFull-paper | A Hoare-Logic Style Refinement Types FormalisationVirtual TyDe Zilin Chen UNSW Sydney Link to publication DOI | ||
09:18 18mFull-paper | Computing with Generic Trees in Agda TyDe | ||
09:36 18mShort-paper | Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (Extended Abstract) TyDe Andreas Nuyts KU Leuven, Belgium Link to publication | ||
09:54 18mShort-paper | Provingly Correct Optimisations on Intrinsically Typed Expressions (Extended Abstract) TyDe Matthias Heinzel Utrecht University Pre-print | ||
10:12 18mFull-paper | Structural Refinement Types TyDe David Binder University of Tübingen, Ingo Skupin University of Tübingen, David Läwen University of Tübingen, Germany, Klaus Ostermann University of Tübingen Pre-print | ||
09:00 - 10:30 | |||
09:00 30mTalk | Welcome HIW | ||
09:30 60mTalk | State of GHC HIW | ||
09:00 - 10:30 | |||
09:00 45mOther | Opening Remarks PLMW @ ICFP Kristopher Micinski Syracuse University | ||
09:45 45mTalk | How to thrive as a PhD student PLMW @ ICFP Sam Westrick Carnegie Mellon University | ||
09:00 - 10:30 | |||
09:00 30mTalk | Lift Inference for Lexical Effect Handlers with Second-Class Functions HOPE Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tübingen | ||
09:30 30mTalk | Higher order programming with probabilistic effects: A model of stochastic memoization and name generation HOPE | ||
10:00 30mTalk | Effect Handlers in Scope, EvidentlyVirtual HOPE File Attached | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Coffee break Catering & social | ||
11:00 - 12:30 | |||
11:00 18mShort-paper | Idris2-Table: evaluating dependently-typed tables with the Brown Benchmark for Table Types (Extended Abstract) TyDe Robert Wright The University of Edinburgh, UK, Michel Steuwer University of Edinburgh, Ohad Kammar University of Edinburgh | ||
11:18 18mShort-paper | Syntax-Generic Operations, Reflectively Reified (Extended Abstract) TyDe Tzu-Chi Lin Institute of Information Science, Academia Sinica, Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica Pre-print | ||
11:36 18mShort-paper | Toward Grammar Inference via Refinement Types (Extended Abstract) TyDe Pre-print Media Attached | ||
11:54 18mShort-paper | Towards Dependently-Typed Control Effects (Extended Abstract)Virtual TyDe File Attached | ||
12:12 18mFull-paper | tylr, a tiny tile-based structure editor TyDe David Moon University of Michigan, Andrew Blinn University of Michigan, Cyrus Omar University of Michigan DOI Pre-print | ||
11:00 - 12:30 | |||
11:00 30mTalk | Compiling Mu with GHC: Halfway Down the Rabbit Hole HIW Gergo Erdi Standard Chartered Bank File Attached | ||
11:30 30mTalk | A Termination Checker for Haskell Rewrite Rules HIW Makoto Hamana Gunma University, Japan | ||
12:00 30mTalk | Annotating Deeply Embedded Languages HIW | ||
11:00 - 12:30 | |||
11:00 45mPanel | Formal Methods: Theory and Practice PLMW @ ICFP Thomas Gilray University of Alabama at Birmingham, Nadia Polikarpova University of California at San Diego, Niki Vazou IMDEA Software Institute, Mike Dodds Galois, Inc., Kristopher Micinski Syracuse University, Daan Leijen Microsoft Research | ||
11:45 45mTalk | Getting the Most Out of ICFP PLMW @ ICFP Paulette Koronkevich University of British Columbia | ||
11:00 - 12:30 | |||
11:00 30mTalk | Relative Monads in CBPV for Stack-based Effects HOPE Max S. New University of Michigan | ||
11:30 30mTalk | Temporal refinements for Call-By-Push-Value with fixpoint HOPE Guilhem Jaber University of Nantes, Kenji Maillard Inria Nantes & University of Chile, Colin Riba LIP - ENS de Lyon File Attached | ||
12:00 30mTalk | On Reinforcement Learning, Effect Handlers, and the State Monad HOPE Ugo Dal Lago University of Bologna; Inria, Alexis Ghyselen University of Bologna, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering & social | ||
14:00 - 15:30 | TyDe 3 / Zena's Birthday 1TyDe at Club CD Chair(s): Gabriel Scherer INRIA Saclay, Marco Gaboardi Boston University | ||
14:00 18mShort-paper | Normalization by Evaluation with Free Extensions (Extended Abstract) TyDe Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Sam Lindley The University of Edinburgh, UK, Nachiappan Valliappan Chalmers University of Technology, Jeremy Yallop University of Cambridge Pre-print | ||
14:18 18mTalk | Zena's birthday introduction TyDe Marco Gaboardi Boston University | ||
14:36 18mTalk | Compiling without continuations TyDe Simon Peyton Jones Epic Games | ||
14:54 18mTalk | On the power of syntactic methods: It is all syntax after all… TyDe Amr Sabry Indiana University | ||
15:12 18mTalk | The impact of delimited control and call-by-need in proof theory TyDe | ||
14:00 - 15:30 | |||
14:00 90mTalk | Teaching functional programming Tutorials Michael Sperber Active Group GmbH | ||
14:00 - 15:30 | Lightning TalksHIW at E3 Lightning talks can be submitted via this form: https://forms.gle/5GG9fkUPB2muw6vt5 | ||
14:00 15mTalk | Lightning Talk Slot #1: Signature Sections HIW Gergo Erdi Standard Chartered Bank File Attached | ||
14:15 15mTalk | Lightning Talk Slot #2: An SSA-based Register Allocator for GHC HIW | ||
14:30 15mTalk | Lightning Talk Slot #3: The Haskell Optimization Handbook HIW Jeffrey Young IOHK | ||
14:45 15mTalk | Lightning Talk Slot #4: Modularizing GHC HIW | ||
15:00 15mTalk | Lightning Talk Slot #5: More recursive equations HIW Joachim Breitner Epic Games | ||
15:15 15mTalk | Lightning Talk Slot #6 HIW | ||
14:00 - 15:30 | |||
14:00 45mTalk | Introduction to Lean PLMW @ ICFP Sebastian Ullrich Karlsruhe Institute of Technology, David Thrane Christiansen The Haskell Foundation | ||
14:45 45mTalk | How Can I Academia When My Brain Can't Even? Mental Health in Grad School and Beyond PLMW @ ICFP | ||
14:00 - 15:30 | |||
14:00 30mTalk | Flexibly graded monads and graded algebras HOPE File Attached | ||
14:30 30mTalk | Monadic Semantics of Bidirectional Effects HOPE Youyou Cong Tokyo Institute of Technology, Shin-ya Katsumata National Institute of Informatics, Kazuki Niimi Axell Corporation, Jonathan Immanuel Brachthäuser University of Tübingen | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Coffee break Catering & social | ||
16:00 - 17:30 | |||
16:00 18mTalk | A Computational Interpretation of Girard's Intuitionistic Proof-Nets TyDe Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France | ||
16:18 18mTalk | Duality of intersection and union types - where and how? TyDe Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA | ||
16:36 18mTalk | Mu tilde (re)cycled TyDe Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt | ||
16:54 18mTalk | OPLSS over twenty years (online) TyDe Robert Harper Carnegie Mellon University | ||
17:12 18mTalk | Happy Birthday, Zena! TyDe | ||
16:00 - 17:30 | |||
16:00 90mTalk | Teaching functional programming Tutorials Michael Sperber Active Group GmbH | ||
16:00 - 17:30 | |||
16:00 30mTalk | A look across the pond: a comparison between GHC and Racket compilation models HIW Alexis King Tweag | ||
16:30 30mTalk | Haskell Playground (WIP) HIW Tom Smeding Utrecht University | ||
17:00 30mTalk | CSI: Haskell: Fault-Localization in Lazy Languages using Runtime Tracing HIW Matthías Páll Gissurarson Chalmers University of Technology, Sweden | ||
16:00 - 17:30 | |||
16:00 90mTalk | How to Write Papers and Give Talks That People Can Follow PLMW @ ICFP Derek Dreyer MPI-SWS | ||
16:00 - 17:30 | |||
16:00 30mTalk | Dependent Temporal Type-and-Effect System with Delimited Continuations HOPE | ||
16:30 30mTalk | Enabling Safe Shared-Memory Interoperability in WebAssemblyVirtual HOPE Michael Fitzgibbons Northeastern University (USA), Zoe Paraskevopoulou Northeastern University, Noble Mushtak Northeastern University, Amal Ahmed Northeastern University, USA | ||
17:00 30mTalk | Verifying non-terminating programs with IO in F* HOPE Cezar-Constantin Andrici MPI-SP, Théo Winterhalter MPI-SP, Cătălin Hriţcu MPI-SP, Exequiel Rivas Tallinn University of Technology Pre-print File Attached | ||
Mon 12 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Mon 12 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
08:00 - 08:50 | RegistrationCatering & social at Foyer 2 If you are a speaker in the first morning session you should submit your slides the day before, or arrive early in the morning to submit, preferrably already at 8:00. | ||
08:00 50mRegistration | Registration Catering & social | ||
08:50 - 09:00 | |||
08:50 10mDay opening | Welcome Catering & social | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Deep Programmability: A New Lens on Networking ICFP Papers and Events Nate Foster Cornell University | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering & social | ||
10:30 - 12:10 | Lambda Calculus and SemanticsICFP Papers and Events at Linhart Chair(s): Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA | ||
10:30 20mTalk | The Theory of Call-by-Value Solvability ICFP Papers and Events DOI | ||
10:50 20mTalk | A Simple and Efficient Implementation of Strong Call by Need by an Abstract Machine ICFP Papers and Events Malgorzata Biernacka University of Wrocław, Witold Charatonik University of Wrocław, Faculty of Mathematics and Computer Science, Tomasz Drab University of Wrocław, Faculty of Mathematics and Computer Science DOI | ||
11:10 20mTalk | On Feller Continuity and Full Abstraction ICFP Papers and Events Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Raphaëlle Crubillé CNRS, Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis DOI | ||
11:30 20mTalk | Multi Types and Reasonable SpaceDistinguished Paper ICFP Papers and Events Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna; Inria, Gabriele Vanoni University of Bologna & INRIA Sophia Antipolis DOI | ||
11:50 20mTalk | Denotational semantics as a foundation for cost recurrence extraction for functional languagesJFP Presentation ICFP Papers and Events | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch Catering & social | ||
13:40 - 15:20 | Analysis and TransformationsICFP Papers and Events at Linhart Chair(s): Malgorzata Biernacka University of Wrocław | ||
13:40 20mTalk | Reference Counting with Frame Limited Reuse ICFP Papers and Events DOI | ||
14:00 20mTalk | Entanglement Detection With Near-Zero CostDistinguished Paper ICFP Papers and Events Sam Westrick Carnegie Mellon University, Jatin Arora Carnegie Mellon University, Umut A. Acar Carnegie Mellon University DOI | ||
14:20 20mTalk | Generating circuits with generators ICFP Papers and Events Marek Materzok University of Wroclaw DOI | ||
14:40 20mTalk | Staged Compilation With Two-Level Type Theory ICFP Papers and Events András Kovács Eötvös Loránd University DOI | ||
15:00 20mTalk | Random Testing of a Higher-Order Blockchain LanguageExperience Report ICFP Papers and Events Tram Hoang National University of Singapore, Anton Trunov Zilliqa Research, Leonidas Lampropoulos University of Maryland, College Park, Ilya Sergey National University of Singapore DOI Pre-print | ||
15:20 - 15:50 | |||
15:20 30mCoffee break | Coffee break Catering & social | ||
15:50 - 16:50 | |||
15:50 20mTalk | Propositional Equality for Gradual Dependently Typed Programming ICFP Papers and Events Joseph Eremondi University of British Columbia, Ronald Garcia University of British Columbia, Éric Tanter University of Chile DOI | ||
16:10 20mTalk | A Reasonably Gradual Type Theory ICFP Papers and Events Kenji Maillard Inria Nantes & University of Chile, Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile DOI | ||
16:30 20mTalk | A completely unique account of enumeration ICFP Papers and Events DOI | ||
16:50 - 17:00 | |||
16:50 10mBreak | Break Catering & social | ||
17:00 - 18:00 | |||
17:00 60mPanel | Fireside Chat with Arvind and Guy Steele ICFP Papers and Events | ||
19:00 - 20:00 | |||
19:00 60mSocial Event | Guided tour of Ljubljana Catering & social | ||
20:00 - 22:00 | |||
20:00 2hSocial Event | Reception & SRC poster presentation Catering & social | ||
Tue 13 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Tue 13 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
08:00 - 09:00 | RegistrationCatering & social at Foyer 2 If you are a speaker in the first morning session you should submit your slides the day before, or arrive early in the morning to submit, preferrably already at 8:00. | ||
08:00 60mRegistration | Registration Catering & social | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Call-by-Push-Value, Quantitatively ICFP Papers and Events Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering & social | ||
10:30 - 12:10 | |||
10:30 20mTalk | Later Credits: Resourceful Reasoning for the Later Modality ICFP Papers and Events Simon Spies MPI-SWS & Saarland University, Lennard Gäher MPI-SWS & Saarland University, Joseph Tassarotti NYU, Ralf Jung MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS DOI | ||
10:50 20mTalk | Introduction and Elimination, Left and Right ICFP Papers and Events Klaus Ostermann University of Tübingen, David Binder University of Tübingen, Ingo Skupin University of Tübingen, Tim Süberkrüb University of Tübingen, Paul Downen University of Massachusetts Lowell DOI Pre-print | ||
11:10 20mTalk | Normalization for Fitch-style Modal CalculiDistinguished Paper ICFP Papers and Events Nachiappan Valliappan Chalmers University of Technology, Fabian Ruch Unaffiliated, Carlos Tomé Cortiñas Chalmers University of Technology DOI Media Attached | ||
11:30 20mTalk | Multiparty GV: Functional Multiparty Session Types With Certified Deadlock Freedom ICFP Papers and Events Jules Jacobs Radboud University, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen DOI | ||
11:50 20mTalk | Back to futuresJFP Presentation ICFP Papers and Events | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch Catering & social | ||
13:40 - 15:20 | Program Verification & SynthesisICFP Papers and Events at Linhart Chair(s): Arthur Azevedo de Amorim Boston University | ||
13:40 20mTalk | Verified Symbolic Execution with Kripke Specification Monads (and no Meta-Programming) ICFP Papers and Events Steven Keuchel Vrije Universiteit Brussel, Sander Huyghebaert Vrije Universiteit Brussel, Georgy Lukyanov Newcastle University, UK, Dominique Devriese KU Leuven DOI | ||
14:00 20mTalk | Safe Couplings: Coupled Refinement Types ICFP Papers and Events Lisa Vasilenko IMDEA Software Institute, Niki Vazou IMDEA Software Institute, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain DOI | ||
14:20 20mTalk | Aeneas: Rust Verification by Functional Translation ICFP Papers and Events DOI | ||
14:40 20mTalk | Searching Entangled Program Spaces ICFP Papers and Events James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego DOI | ||
15:00 20mTalk | Iterating on multiple collections in synchronyJFP Presentation ICFP Papers and Events Stefano Perna , Val Tannen University of Pennsylvania, USA, Limsoon Wong National University of Singapore | ||
15:20 - 15:50 | |||
15:20 30mSocial Event | CARES session Catering & social C: Gabriele Keller Utrecht University, C: Simon Peyton Jones Epic Games , C: Stephanie Weirich University of Pennsylvania | ||
15:20 - 15:50 | |||
15:20 30mCoffee break | Coffee break Catering & social | ||
15:50 - 16:50 | Generic Programming and EducationICFP Papers and Events at Linhart Chair(s): Nicolas Wu Imperial College London | ||
15:50 20mTalk | Datatype-Generic Programming Meets Elaborator Reflection ICFP Papers and Events Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica, Liang-Ting Chen Academia Sinica, Tzu-Chi Lin Institute of Information Science, Academia Sinica Link to publication DOI Media Attached | ||
16:10 20mTalk | Practical generic programming over a universe of datatypes ICFP Papers and Events DOI | ||
16:30 20mTalk | Structural Versus Pipeline Composition of Higher-Order FunctionsVirtualExperience Report ICFP Papers and Events DOI | ||
16:50 - 17:00 | |||
16:50 10mBreak | Break Catering & social | ||
17:00 - 18:00 | |||
17:00 40mOther | Student Research Competition – Finalist Presentations ICFP Papers and Events | ||
17:40 20mOther | Programming Contest Report ICFP Papers and Events Alperen Keles University of Maryland at College Park | ||
18:30 - 21:00 | |||
18:30 2h30mDinner | Women@ICFP Catering & social | ||
Wed 14 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Wed 14 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
08:00 - 09:00 | RegistrationCatering & social at Foyer 2 If you are a speaker in the first morning session you should submit your slides the day before, or arrive early in the morning to submit, preferrably already at 8:00. | ||
08:00 60mRegistration | Registration Catering & social | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Retrofitting Concurrency – Lessons from the Engine Room ICFP Papers and Events KC Sivaramakrishnan IIT Madras and Tarides Media Attached | ||
10:00 - 10:30 | |||
10:00 30mSocial Event | CARES session Catering & social C: Gabriele Keller Utrecht University, C: Simon Peyton Jones Epic Games , C: Stephanie Weirich University of Pennsylvania | ||
10:00 - 10:30 | |||
10:00 30mCoffee break | Coffee break Catering & social | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch Catering & social | ||
13:40 - 15:20 | Programming and Reasoning About EffectsICFP Papers and Events at Linhart Chair(s): William J. Bowman University of British Columbia | ||
13:40 20mTalk | Monadic Compiler CalculationFunctional Pearl ICFP Papers and Events DOI | ||
14:00 20mTalk | Formal Reasoning About Layered Monadic Interpreters ICFP Papers and Events Irene Yoon University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania DOI | ||
14:20 20mTalk | Program Adverbs and Tlön EmbeddingsDistinguished PaperVirtual ICFP Papers and Events DOI Pre-print | ||
14:40 20mTalk | Flexible presentations of graded monads ICFP Papers and Events Shin-ya Katsumata National Institute of Informatics, Dylan McDermott Reykjavik University, Tarmo Uustalu Reykjavik University, Nicolas Wu Imperial College London DOI | ||
15:00 20mTalk | Fusing Industry and Academia at GitHubExperience Report ICFP Papers and Events Patrick Thomson GitHub, Rob Rix GitHub, Inc., Tom Schrijvers KU Leuven, Nicolas Wu Imperial College London DOI | ||
15:20 - 15:50 | |||
15:20 30mCoffee break | Coffee break Catering & social | ||
15:50 - 16:50 | Effects and Type InferenceICFP Papers and Events at Linhart Chair(s): Ben Lippmeier Ghost Locomotion | ||
15:50 20mTalk | Modular Probabilistic Models via Algebraic Effects ICFP Papers and Events Minh Nguyen University of Bristol, Roly Perera Alan Turing Institute, Meng Wang University of Bristol, Nicolas Wu Imperial College London DOI | ||
16:10 20mTalk | Constraint-based type inference for FreezeML ICFP Papers and Events Frank Emrich University of Edinburgh, UK, Jan Stolarek University of Edinburgh, UK, James Cheney University of Edinburgh; Alan Turing Institute, Sam Lindley The University of Edinburgh, UK DOI | ||
16:30 20mTalk | Linearly Qualified Types: Generic inference for capabilities and uniqueness ICFP Papers and Events Arnaud Spiwack Tweag, Csongor Kiss Imperial College London, Jean-Philippe Bernardy University of Gothenburg, Sweden, Nicolas Wu Imperial College London, Richard A. Eisenberg Jane Street Link to publication DOI Pre-print | ||
16:50 - 17:00 | |||
16:50 10mBreak | Break Catering & social | ||
17:00 - 18:00 | |||
17:00 40mAwards | Awards ICFP Papers and Events | ||
17:40 15mOther | Program Committee Chair Report ICFP Papers and Events Zena M. Ariola University of Oregon | ||
17:55 5mDay closing | ICFP 2023 Announcement ICFP Papers and Events | ||
Thu 15 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Thu 15 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
08:00 - 09:00 | |||
08:00 60mRegistration | Registration Catering & social | ||
09:00 - 10:30 | |||
09:00 90mTutorial | OCaml 5 for the working programmer Tutorials | ||
09:00 - 10:30 | |||
09:00 40mTalk | Quantum relational Hoare logic, towards a formalization PLanQC Dominique Unruh University of Tartu | ||
09:40 25mTalk | Type-safe (Variational) Quantum Programming in IdrisVirtual PLanQC Liliane-Joy Dandy EPFL, Ecole Polytechnique, Emmanuel Jeandel LORIA, University of Lorraine, Vladimir Zamdzhiev Inria, LORIA, Université de Lorraine File Attached | ||
10:05 25mTalk | Quantum Programming with Data Structures PLanQC File Attached | ||
09:00 - 10:30 | |||
09:20 10mDay opening | Welcome Haskell Nadia Polikarpova University of California at San Diego | ||
09:30 60mKeynote | Cause and Effect(s): Towards a More Programmable Haskell Haskell Rob Rix GitHub, Inc. | ||
09:00 - 10:30 | |||
09:00 30mTalk | On a Declarative Guideline-Directed UI Layout SynthesisVirtual, Live miniKanren Dmitrii Kosarev Saint Petersburg State University, P: Petr Lozov St. Petersburg State University, St. Petersburg, Russia, Denis Fokin , Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia Pre-print File Attached | ||
09:30 30mTalk | On a Direction-Driven Functional ConversionVirtual, Live miniKanren P: Ekaterina Verbitskaia JetBrains, Daniil Berezun JetBrains Research, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia Pre-print File Attached | ||
10:00 30mTalk | Wildcard Logic VariablesVirtual, Live miniKanren P: Dmitrii Kosarev Saint Petersburg State University, Daniil Berezun JetBrains Research, Petr Lozov St. Petersburg State University, St. Petersburg, Russia Pre-print File Attached | ||
09:00 - 10:30 | |||
09:00 90mMeeting | Introduction and Session 1 FUNARCH | ||
09:00 - 10:30 | |||
09:00 50mKeynote | Keynote: Efficient and Scalable Parallel Functional Programming Through Disentanglement ML Sam Westrick Carnegie Mellon University | ||
09:50 20mTalk | Towards Algebraic Subtyping for Extensible Records ML Rodrigo Marques Universidade do Porto, Mário Florido Universidade do Porto, Pedro Vasconcelos LIACC, Universidade do Porto, Porto, Portugal | ||
10:10 20mTalk | The Ultimate Conditional SyntaxVirtual ML Lionel Parreaux The Hong Kong University of Science and Technology (HKUST) Pre-print File Attached | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Coffee break Catering & social | ||
11:00 - 12:30 | |||
11:00 90mTutorial | OCaml 5 for the working programmer Tutorials | ||
11:00 - 12:30 | |||
11:00 25mTalk | Topological Quantum Programming in TED-KVirtual PLanQC File Attached | ||
11:25 25mTalk | Qrisp: A Framework for Compilable High-Level Programming of Gate-Based Quantum Computers PLanQC Raphael Seidel Fraunhofer Institute for Open Communication Systems, Sebastian Bock Fraunhofer Institute for Open Communication Systems, Nikolay Tcholtchev Fraunhofer Institute for Open Communication Systems, Manfred Hauswirth Fraunhofer Institute for Open Communication Systems, TU Berlin File Attached | ||
11:50 40mTalk | Poster session PLanQC File Attached | ||
11:00 - 12:30 | |||
11:00 30mTalk | Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell Haskell Lykourgos Mastorou National Technical University of Athens, Nikolaos Papaspyrou National Technical University of Athens, Niki Vazou IMDEA Software Institute | ||
11:30 30mTalk | How to Safely Use Extensionality in Liquid Haskell Haskell | ||
12:00 30mTalk | Liquid Proof Macros Haskell Henry Blanchette , Niki Vazou IMDEA Software Institute, Leonidas Lampropoulos University of Maryland, College Park | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Tutorial Reconstruction of miniKanren with constraintsVirtual Tutorial miniKanren Pre-print File Attached | ||
11:30 60mTutorial | Relational Interpreters, Conversion, and SynthesisVirtual Live Tutorial miniKanren File Attached | ||
11:00 - 12:30 | |||
11:00 90mMeeting | Session 2 FUNARCH | ||
11:00 - 12:30 | Implementation of Functional LanguagesML at Štih Chair(s): Matija Pretnar University of Ljubljana, Slovenia | ||
11:00 20mTalk | A New Match Compiler for Standard ML of New Jersey ML David MacQueen University of Chicago (Emeritus) File Attached | ||
11:20 20mTalk | Boxroot, fast movable GC roots for a better FFI ML Pre-print | ||
11:40 20mTalk | Unboxed types for OCaml ML | ||
12:00 20mTalk | What About the Integer Numbers? ML Daan Leijen Microsoft Research Link to publication File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering & social | ||
14:00 - 15:30 | Formalization, verification, and correctnessPLanQC at E3 Chair(s): Ross Duncan Cambridge Quantum Computing | ||
14:00 40mTalk | Invited talk: Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs PLanQC Charles Yuan MIT CSAIL | ||
14:40 25mTalk | Analyzing quantum programs using the power of interaction PLanQC File Attached | ||
15:05 25mTalk | Q*: Implementing Quantum Separation Logic in F* PLanQC Kesha Hietala University of Maryland, Sarah Marshall Microsoft Quantum, Robert Rand University of Chicago, Nikhil Swamy MSR Redmond File Attached | ||
14:00 - 15:30 | |||
14:00 30mTalk | A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures Haskell Gershom Bazerman Arista Networks | ||
14:30 30mTalk | Open Transactional Actions: Interacting with non-transactional resources in STM Haskell Haskell Jonathas Augusto de Oliveira Conceição Universidade Federal de Pelotas, André Rauber Du Bois Universidade Federal de Pelotas, Gerson Cavalheiro Universidade Federal de Pelotas, Samuel Feitosa Universidade Federal da Fronteira Sul, Rodrigo G. Ribeiro Federal University of Ouro Preto | ||
15:00 30mTalk | Staging Regular Expressions with Moore Cayley Fusion Haskell | ||
14:00 - 15:30 | |||
14:00 30mTalk | Demo: New View on Plasma Fractals -- From the High Point of Array Languages FARM Pre-print | ||
14:30 30mTalk | Demo: Counterpoint Analysis and SynthesisVirtual FARM John Leo Halfaya Research Pre-print | ||
14:00 - 15:30 | |||
14:00 30mTalk | Efficient Variational Inference in miniKanren with Weighted Model CountingVirtual, Live miniKanren Pre-print File Attached | ||
14:30 30mTalk | Some criteria for implementations of conjunction and disjunction in microKanrenVirtual, Live miniKanren Pre-print | ||
15:00 30mTalk | Fail Fast and Profile On: Towards a miniKanren ProfilerVirtual, Live miniKanren P: Sloan Chochinov University of Toronto Mississauga, P: Daksh Malhotra University of Toronto Mississauga, Gregory Rosenblatt University of Alabama at Birmingham, Matthew Might University of Alabama at Birmingham | Harvard Medical School, Lisa Zhang University of Toronto Mississauga Pre-print | ||
14:00 - 15:30 | |||
14:00 90mMeeting | Session 3 FUNARCH | ||
14:00 - 15:30 | |||
14:00 20mTalk | Necro ML: Generating OCaml Interpreters ML Pre-print File Attached | ||
14:20 20mTalk | Module Shapes for Modern Tooling ML File Attached | ||
14:40 20mTalk | An OCaml use case for strong call-by-need reduction ML | ||
15:00 20mTalk | Do Mutable Variables Have Reference Types? ML Oleg Kiselyov Tohoku University, Japan Pre-print | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Coffee break Catering & social | ||
16:00 - 18:00 | |||
16:00 2hOther | Technical setup & rehearsal FARM | ||
16:00 - 17:30 | |||
16:00 25mTalk | Optimal synthesis into fixed XX interactions PLanQC File Attached | ||
16:25 25mTalk | Encoding High-level Quantum Programs as SZX-diagrams PLanQC Agustín Borgna Université de Lorraine, CNRS, Inria, LORIA F 54000 Nancy, France and Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91405, Orsay, France, Rafael Romero Universidad de Buenos Aires, Universidad de la República File Attached | ||
16:50 25mTalk | Adventures in Qutrit Compilation PLanQC File Attached | ||
17:15 15mDay closing | Conclusion and Group Photo PLanQC | ||
16:00 - 17:30 | |||
16:00 90mLive Q&A | GHC Proposal Presentations Haskell S: Joachim Breitner Epic Games , Gergo Erdi Standard Chartered Bank, Andreas Klebinger , Matthías Páll Gissurarson Chalmers University of Technology, Sweden File Attached | ||
16:00 - 17:30 | |||
16:00 90mMeeting | Session 4 FUNARCH | ||
16:00 - 17:30 | |||
16:00 20mTalk | Interpreting OCaml GADTs into Coq ML Pre-print Media Attached File Attached | ||
16:20 20mTalk | Extraction to OCaml from Coq: Operational Correctness Verified in Coq ML Yannick Forster Inria, Matthieu Sozeau Inria, Pierre Giraud Inria, Team Gallinette, Pierre-Marie Pédrot INRIA, Nicolas Tabareau Inria File Attached | ||
16:40 20mTalk | Verify, but test: extracting property-based tests from F* specifications ML File Attached | ||
17:30 - 20:00 | |||
17:30 2h30mSocial Event | Industrial reception Catering & social | ||
18:30 - 21:30 | |||
18:30 60mMeeting | Meet the artists FARM A: Rob Canning , A: Enrico Dorigatti University of Portsmouth, A: Francesco Corvi , A: Luka Prinčič , A: Florencia Alonso (Flor de Fuego) None, C: Luka Frelih LJUDMILA Art & Science Laboratory | ||
19:40 20mOther | Fold Yer Loops! FARM | ||
20:00 20mOther | Xeno FARM Enrico Dorigatti University of Portsmouth | ||
20:30 20mOther | Live coding with Adapt FARM | ||
20:50 20mOther | Algoforte FARM | ||
21:10 20mOther | Specific site: remembering is never a faithful copy FARM | ||
Fri 16 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
Fri 16 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
08:00 - 09:00 | |||
08:00 60mRegistration | Registration Catering & social | ||
09:00 - 10:30 | |||
09:00 60mKeynote | Why Functional Programming Matters in CS Education Scheme | ||
10:00 30mFull-paper | Scheme Pearl: Quantum Continuations Scheme Borislav Agapiev YottaAnswers.com, Vikraman Choudhury University of Glasgow, Amr Sabry Indiana University Pre-print | ||
09:00 - 10:30 | |||
09:30 60mKeynote | Industrial Strength Laziness: What's Next? Haskell David Thrane Christiansen The Haskell Foundation | ||
09:00 - 10:30 | |||
09:00 50mKeynote | OCaml 5.0 - Concurrent and Parallel programming for OCaml OCaml KC Sivaramakrishnan IIT Madras and Tarides Media Attached | ||
09:50 20mTalk | Multicoretests - Parallel Testing Libraries for OCaml 5.0 OCaml | ||
10:10 20mTalk | Composing Schedulers using Effect Handlers OCaml Pre-print | ||
09:00 - 10:30 | |||
09:00 15mDay opening | Welcome to the Erlang Workshop Erlang | ||
09:15 75mKeynote | eqWAlizer - Scaling Erlang development at WhatsApp with static typing Erlang | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Coffee break Catering & social | ||
11:00 - 12:30 | |||
11:00 30mFull-paper | Macro-embedding Compiler Intermediate Languages in Racket Scheme William J. Bowman University of British Columbia Pre-print | ||
11:30 30mTalk | Scheme Requests for Implementation Status Report Scheme Arthur Gleckler SRFI Editor | ||
12:00 30mShort-paper | Automating the Design RecipeVirtual Scheme | ||
11:00 - 12:30 | |||
11:00 30mTalk | Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow Haskell Compiler Haskell Celeste Hollenbeck University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh, Michel Steuwer University of Edinburgh | ||
11:30 30mTalk | Partial Type Constructors in Practice Haskell Apoorv Ingle University of Iowa, Alex Hubers The University of Iowa, J. Garrett Morris The University of Iowa | ||
12:00 30mTalk | Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs Haskell Jesper Cockx TU Delft, Lucas Escot TU Delft, Orestis Melkonian University of Edinburgh, James Chapman Input Output, Ulf Norell Gothenburg University Pre-print File Attached | ||
11:00 - 12:30 | |||
11:00 45mTalk | A Reliability Benchmark for Actor-Based Server Languages Erlang | ||
11:45 45mTalk | CAEFL: Composable and Environment Aware Federated Learning Models Erlang Ruomeng (Cocoa) Xu University of Glasgow, Anna Lito Michala University of Glasgow, Phil Trinder University of Glasgow | ||
11:00 - 12:30 | |||
11:00 20mTalk | Efficient “out of heap” pointers for multicore OCaml OCaml Pre-print | ||
11:20 20mTalk | Memo: an incremental computation library that powers Dune OCaml File Attached | ||
11:50 20mTalk | Stack allocation for OCaml OCaml Pre-print | ||
12:10 20mTalk | Continuous Monitoring of OCaml Applications using Runtime EventsVirtual OCaml Pre-print | ||
12:30 - 14:00 | |||
12:30 90mSocial Event | OCaml Industry Lunch Catering & social | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering & social | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Verified Quantum Computing Tutorials | ||
14:00 - 15:30 | |||
14:00 30mIndustry talk | Introducing Visual Scheme for Applications: Modernizing Office Solutions on the CLRVirtual Scheme Bob Calco Apex Data Solutions, LLC | ||
14:30 30mFull-paper | An FFI between Gambit Scheme and CPythonVirtual Scheme Pre-print | ||
15:00 30mShort-paper | R7RS Large Status ReportVirtual Scheme | ||
14:00 - 15:30 | |||
14:00 30mTalk | Embedded Pattern Matching Haskell | ||
14:30 30mDemonstration | Eiger: Auditable, executable, flexible legal regulations Haskell | ||
15:00 30mDay closing | PC Chair Report Haskell Nadia Polikarpova University of California at San Diego | ||
14:00 - 15:30 | |||
14:00 45mTalk | Executable Contracts for Elixir Erlang Sergio Perez Rubio Universitat Politècnica de València, Luis Eduardo Bueso de Barrio Universidad Politécnica de Madrid, Ignacio Ballesteros Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Clara Benac Earle Universidad Politécnica de Madrid, Lars-Åke Fredlund Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid | ||
14:45 45mTalk | Troubleshooting the Performance of a Large Erlang System Erlang | ||
14:00 - 15:30 | |||
14:00 20mTalk | Homogeneous builds with OBuilder and OCaml OCaml Tim McGilchrist Tarides, David Allsopp Tarides, Patrick Ferris Tarides, Antonin Décimo Tarides, Thomas Leonard Tarides UK, Anil Madhavapeddy University of Cambridge, UK, Kate Deplaix Tarides UK Pre-print Media Attached | ||
14:20 20mTalk | Tracing OCaml Programs OCaml Pre-print Media Attached | ||
14:50 20mTalk | Supporting a decade of opam OCaml Media Attached File Attached | ||
15:10 20mTalk | Copying opam switches – it should Just Work™ OCaml David Allsopp Tarides Media Attached File Attached | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Coffee break Catering & social | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Verified Quantum Computing Tutorials | ||
16:00 - 17:30 | |||
16:00 60mTalk | Programming is (should be) fun!Virtual Scheme | ||
16:00 - 17:30 | Demos + DiscussionsHaskell at Kosovel Chair(s): Nadia Polikarpova University of California at San Diego | ||
16:00 90mMeeting | Demos Haskell Matthías Páll Gissurarson Chalmers University of Technology, Sweden, Makoto Hamana Gunma University, Japan, David Thrane Christiansen The Haskell Foundation, Jesper Cockx TU Delft, Lisa Vasilenko IMDEA Software Institute, Orestis Melkonian University of Edinburgh | ||
16:00 - 17:30 | |||
16:00 45mTalk | InfERL: Scalable and Extensible Erlang Static Analysis Erlang Ákos Hajdu Meta, Matteo Marescotti Facebook, Inc., Thibault Suzanne Meta, Ke Mao Meta, Radu Grigore Facebook, Per Gustafsson Meta, Dino Distefano Facebook London | ||
16:45 45mOther | Lightning talks Erlang | ||
19:00 - 21:00 | OCaml & farewell receptionCatering & social at Ljubljana Zoo See event details for information on travel and free zoo entry. | ||
19:00 2hSocial Event | OCaml & farewell reception Catering & social | ||